From ffa769c48c98bb87ca0f8eafa2d7385064439c69 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 2 Feb 2019 21:22:27 -0600 Subject: [PATCH] doc: add a section and test on the sudoku solver --- README.md | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/README.md b/README.md index e0ef842f..4dc23a6d 100644 --- a/README.md +++ b/README.md @@ -142,3 +142,44 @@ it into clauses using `make_cnf`: - : Sat.res = Sat.Unsat ... ``` +### CDCL(T): a Sudoku solver as an example + +The directory `src/sudoku/` contains a simple Sudoku solver that +uses the interface `Msat.Make_cdcl_t`. +In essence, it implements the logical theory `CDCL(Sudoku)`. +The script `sudoku_solve.sh` compiles and runs the solver. + +It's able to parse sudoku grids denoted as 81 integers +(see `tests/sudoku/sudoku.txt` for example). + +Here is a sample grid and the output from the solver (in roughly .5s): + +```sh +$ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt +$ ./sudoku_solve.sh sudoku.txt +... +######################### +solve grid: + ......... + .....3.85 + ..1.2.... + ...5.7... + ..4...1.. + .9....... + 5......73 + ..2.1.... + ....4...9 + +... + 987654321 + 246173985 + 351928746 + 128537694 + 634892157 + 795461832 + 519286473 + 472319568 + 863745219 + +################### +```