はじめに 前回は地獄のSMT-LIBコピペ祭りを経て、z3で数独を解くことに成功しました。 今回はVBから制約を発行してz3に数独を解かせてみましょう。 .NETバインディング z3には.NETのバインディングが用意されており、P/Invoke祭りやCOM祭りをやらなくともz3…