Each program build a theory, which corresponds to a given puzzle.

  1. sudokuLIA.exe demonstrates a straightforward aproach. It builds a theory in Z3 native format. Theory is based on integer numbers and it uses Linear Arithmetic solver.
  2. sudokuBV.exe also builds theory in Z3 native format. It uses Bit Vectors solver. Produced theory is solved in the shortest time.
  3. sudokuSMT.exe build theory in SMT-LIB format, which can be understandable by many other SMT solvers.

Here you can see Z3 worktime on theories generated by this programs:


sudokuLIA.exesudokuBV.exesudokuSMT.exe
1 15.189052 0.246932 112.330890
2 39.969477 0.306012 231.641938
3 1.480314 0.207678 33.269433
4 3.892265 0.199109 13.033685
5 3.990500 0.169286 46.092762
6 5.289847 0.179018 42.128647

Its clear from this table that Bit Vectors are perfect for solving such problem.