The sudoku solver uses Microsoft's Z3 SMT solver. We only use a small part of Z3, namely its SAT solver. The encoding problem is well described on page 35 of the textbook. The implementation exactly follows that. It'll be hard for you to beat Z3 using a special purpose Sudoku solver.