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:

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