The puzzle size can be 4x4, 9x9 (the default) or 16x16.
The solutions are found by converting the puzzle into a satisfiability problem, and this is
displayed using the competition format. This is solved using the sat4j package and the
solution model is also displayed. It is possible to copy the satisfiability problem and paste it into a text
editor to be solved by your own satisfiability solver, and if the solution is pasted into the tool
it can be interpreted as a solution to the SuDoku puzzle - see the "cnf" tab.
A Java application is available
here. Note that your browser my rename this sudoku.jar file to sudoku.zip. It permits larger puzzles, but be warned that the 36x36 puzzles
may take some time to create and solve. To use larger puzzles increase the amount of heap space by using the command

java -Xmx300m -jar sudoku.jar

The Java appliction can also write cnf files and read the corresponding
models and copy and paste puzzles directly.

The source code is also available from sat4j.

When you think that you have finished, clicking "Check" will check your solution. If you get stuck you can ask the program to complete the puzzle for you by clicking "Solve". This
will not change any entered values, protected or not. It may be that it is not possible to continue
with what you have entered, in which case you will be informed. The puzzles created automatically
can always be solved.

123 indicates that row 1, column 2 contains 3.

-456 indicates that row 4, column 5 does not contain 6.

The first line of the problem is of the form "p cnf num-of-variables num-of-clauses".

111 112 113 114 115 116 117 118 119 0

indicates that it contains a least one such value (the 0 is a terminator). To show that it contains only one value needs a series of clauses of the form

-111 -112 0 (can't be both 1 and 2)

-111 -113 0 (can't be both 1 and 3)

These have to be repeated for each of the 81 cells.

111 121 131 141 151 161 171 181 191 0

and to show that it contains a 2 we need

112 122 132 142 152 162 172 182 192 0

This is repeated for values 3 to 9. Then, to show that it does not contain more than one 1, we need

-111 -121 0 (first two squares aren't both 1)

-111 -131 0 (first and third aren't both 1)

This is repeated for the values in the range 2 to 9.

111 211 311 411 5111 611 7111 8111 911 0

and to show that it contains a 2 we need

112 212 312 412 512 612 712 812 912 0

This is repeated for values 3 to 9. Then, to show that it does not contain more than one 1, we need

-111 -211 0 (first two squares aren't both 1)

-111 -311 0 (first and third aren't both 1)

This is repeated for the values in the range 2 to 9.

111 121 131 211 221 231 311 321 331 0

234 0

It should be noted that the clauses described above contain considerable redundancy. For example, if it is guaranteed that row 1 (with 9 cells) contains all the values in the range 1 to 9, then it is not necessary to specify in addition that the same value cannot appear twice. Taking this into account results in a very much smaller, but logically equivalent, cnf problem which can be created using the "Simpler cnf" button. However, the solver used in this program is very much slower when applied to the simpler cnf problem, and so it is only made available for you to try on your own solver.

The encoding for the variables is not the most efficient possible, but is used for the 4x4 and 9x9 cases because it makes the clauses more understandable. The encoding breaks down for the 16x16 problem because r, c and v can all exceed 9. It would be possible to use 10000*r + 100*c + v, but that is so very inefficient that the default heap space for the java virtual machine is not sufficient for the solver. Instead, the encoding used is 17*17*r + 17*c + v.