Sudoku Solver

This applet lets you solve your sudoku. The position is entered by clicking on the different squares of the sudoku. For example, 5 is put on an empty square by clicking five times on it. Once the position is entered, click on the "Solve" button to solve it. If you want to start from scratch, click on the "Clear" button.

This code has been proved correct in the Coq system. A paper that explains the algorithm that is used can be found here. We have been using the OcamlJava to include Ocaml code inside an applet.