|
| 1 | +# Sudoku |
| 2 | +In this example, we consider a smaller 6x6 version of the sudoku. |
| 3 | +The aim is to fill in the grid with numbers from 1 to 6 such that no row, column or box contains the same number twice. |
| 4 | +Boxes are 2 rows tall x 3 columns wide. |
| 5 | +Sudoku is a popular puzzle involving a 9x9 grid. |
| 6 | +Some of the numbers will be filled in as part of the puzzle. |
| 7 | + |
| 8 | + |
| 9 | +## Usage |
| 10 | +### Setup |
| 11 | +If you're using bazel, it will take care of the dependencies for you. |
| 12 | +If not, you'll have to install the dependencies using: |
| 13 | + |
| 14 | +`python -m pip requirements.txt` |
| 15 | + |
| 16 | +### Running the solver |
| 17 | +Through bazel: |
| 18 | + |
| 19 | + `bazel run //sudoku:driver -- (<sudoku-path|setup>)` |
| 20 | +Directly: |
| 21 | + |
| 22 | + `python driver.py (<sudoku-path>|setup)` |
| 23 | + |
| 24 | +Running with |
| 25 | +* `setup` will (re)create the database and load the required schema & data. |
| 26 | +* `<sudoku-path>` will solve the sudoku in the specified file. It will also run setup if required. |
| 27 | + - When running through bazel, use the path to the samples is: `sudoku/sample/sudoku*.txt`. |
| 28 | + |
| 29 | +### Running tests |
| 30 | +`bazel test //sudoku:test` or `python test.py` |
| 31 | + |
| 32 | +## Defining the sudoku file |
| 33 | +The file specified through the `sudoku-path` argument must contain a space |
| 34 | +delimited list of cells. Empty cells should be filled with `0`. |
| 35 | + |
| 36 | +Example, for the sudoku: |
| 37 | + |
| 38 | +| | | 3 | 6 | | | |
| 39 | +|---|---|---|---|---|---| |
| 40 | +| | 2 | | | | 4 | |
| 41 | +| 5 | | | | 6 | | |
| 42 | +| | 3 | | | | 5 | |
| 43 | +| 3 | | | | 1 | | |
| 44 | +| | | 1 | 4 | | | |
| 45 | + |
| 46 | +The file would contain: |
| 47 | +``` |
| 48 | +0 0 3 6 0 0 |
| 49 | +0 2 0 0 0 4 |
| 50 | +5 0 0 0 6 0 |
| 51 | +0 3 0 0 0 5 |
| 52 | +3 0 0 0 1 0 |
| 53 | +0 0 1 4 0 0 |
| 54 | +``` |
| 55 | + |
| 56 | +## Approach |
| 57 | +We declare a variable corresponding to each position in the sudoku |
| 58 | + |
| 59 | +| - | a | b | c | d | e | f | |
| 60 | +|---|---|---|---|---|---|---| |
| 61 | +| 1 |$a1|$b1|$c1|$d1|$e1|$f1| |
| 62 | +| 2 |$a2|$b2|$c2|$d2|$e2|$f2| |
| 63 | +| 3 |$a3|$b3|$c3|$d3|$e3|$f3| |
| 64 | +| 4 |$a4|$b4|$c4|$d4|$e4|$f4| |
| 65 | +| 5 |$a5|$b5|$c5|$d5|$e5|$f5| |
| 66 | +| 6 |$a6|$b6|$c6|$d6|$e6|$f6| |
| 67 | + |
| 68 | +The work is done in the `solution-rule`. |
| 69 | +Each row, column and box is constrained to be a permutation of the numbers 1 to 6. |
| 70 | + |
| 71 | +```typeql |
| 72 | +# Each row must be a valid permutation |
| 73 | +(mem: $a1, mem: $b1, mem: $c1, mem: $d1, mem: $e1, mem: $f1) isa permutation; |
| 74 | +(mem: $a2, mem: $b2, mem: $c2, mem: $d2, mem: $e2, mem: $f2) isa permutation; |
| 75 | +(mem: $a3, mem: $b3, mem: $c3, mem: $d3, mem: $e3, mem: $f3) isa permutation; |
| 76 | +(mem: $a4, mem: $b4, mem: $c4, mem: $d4, mem: $e4, mem: $f4) isa permutation; |
| 77 | +(mem: $a5, mem: $b5, mem: $c5, mem: $d5, mem: $e5, mem: $f5) isa permutation; |
| 78 | +(mem: $a6, mem: $b6, mem: $c6, mem: $d6, mem: $e6, mem: $f6) isa permutation; |
| 79 | +
|
| 80 | +# Each column must be a valid permutation |
| 81 | +(mem: $a1, mem: $a2, mem: $a3, mem: $a4, mem: $a5, mem: $a6) isa permutation; |
| 82 | +(mem: $b1, mem: $b2, mem: $b3, mem: $b4, mem: $b5, mem: $b6) isa permutation; |
| 83 | +(mem: $c1, mem: $c2, mem: $c3, mem: $c4, mem: $c5, mem: $c6) isa permutation; |
| 84 | +(mem: $d1, mem: $d2, mem: $d3, mem: $d4, mem: $d5, mem: $d6) isa permutation; |
| 85 | +(mem: $e1, mem: $e2, mem: $e3, mem: $e4, mem: $e5, mem: $e6) isa permutation; |
| 86 | +(mem: $f1, mem: $f2, mem: $f3, mem: $f4, mem: $f5, mem: $f6) isa permutation; |
| 87 | +
|
| 88 | +# Each box must be a valid permutation |
| 89 | +(mem: $a1, mem: $b1, mem: $c1, mem: $a2, mem: $b2, mem: $c2) isa permutation; |
| 90 | +(mem: $a3, mem: $b3, mem: $c3, mem: $a4, mem: $b4, mem: $c4) isa permutation; |
| 91 | +(mem: $a5, mem: $b5, mem: $c5, mem: $a6, mem: $b6, mem: $c6) isa permutation; |
| 92 | +(mem: $d1, mem: $e1, mem: $f1, mem: $d2, mem: $e2, mem: $f2) isa permutation; |
| 93 | +(mem: $d3, mem: $e3, mem: $f3, mem: $d4, mem: $e4, mem: $f4) isa permutation; |
| 94 | +(mem: $d5, mem: $e5, mem: $f5, mem: $d6, mem: $e6, mem: $f6) isa permutation; |
| 95 | +``` |
| 96 | + |
| 97 | +In our database, we have a single permutation instance inserted as follows: |
| 98 | +```typeql |
| 99 | +$v1 = 1 isa number; |
| 100 | +$v2 = 2 isa number; |
| 101 | +$v3 = 3 isa number; |
| 102 | +$v4 = 4 isa number; |
| 103 | +$v5 = 5 isa number; |
| 104 | +$v6 = 6 isa number; |
| 105 | +(mem: $v1, mem: $v2, mem: $v3, mem: $v4, mem: $v5, mem: $v6) isa permutation; |
| 106 | +``` |
0 commit comments