nickdrozd / reazon

miniKanren for Emacs
GNU General Public License v3.0
112 stars 6 forks source link

Remove unnecessary constraints within reazon--test-sudoku-solve-4x4. #8

Closed ebpa closed 6 years ago

ebpa commented 6 years ago

Super minor; it just needs the eight row and column constraints.

nickdrozd commented 6 years ago

With these changes, (reazon-sudoku-solve-4x4) produces 288 solutions. That's how many solved 4x4 boards there are, so that suggests that these changes are correct. Actually, that's how I convinced myself that the original is correct too, since I can't verify every board individually. I do have some questions though.

The original implementation is basically just the rules of sudoku written down: the nubers of every row must be 1, 2, 3, or 4, and so must the numbers of every column, and the numbers of the subsquares. I guess the idea here is that some of the numbers (especially those of the subsquares) are implied by the arrangement of the others, and so don't need to be specified.

ebpa commented 6 years ago

By subsquares you mean each "quadrant" (top left corner of four squares, top right, etc.)? My thinking was that those constraints are artificial and actually would exclude possible solutions. For example:

|---+---+---+---|
|   | 2 | 3 | 4 |
|---+---+---+---|
| 4 |   |   | 3 |
|---+---+---+---|
|   |   |   | 2 |
|---+---+---+---|
|   |   | 4 |   |
|---+---+---+---|

Came back without a solution. (I notice now that I killed the wrong line in my changes and kept a quadrant constraint. Updated that branch to include a test as well). Without the quadrant constraints:

(reazon--should-equal '((1 2 3 4 4 1 2 3 3 4 1 2 2 3 4 1))
  (reazon-sudoku-solve-4x4 (a1 1) (a2 2) (a3 3) (a4 4) (b1 4) (b4 3) (c4 2) (d3 4)))
|---+---+---+---|
| 1 | 2 | 3 | 4 |
|---+---+---+---|
| 4 | 1 | 2 | 3 |
|---+---+---+---|
| 3 | 4 | 1 | 2 |
|---+---+---+---|
| 2 | 3 | 4 | 1 |
|---+---+---+---|

Mathematically? I'm not sure other than that I think the constraint (I think) is the uniqueness within rows and columns which suggests k * 2 constraints where k is the grid size. They strike me as a minimal set of constraints, but maybe k * 2 - 1 is adequate? I imagine the 9x9 case could be reduced further (from 27 rules to 18), but would take even longer to arrive at a solution.

nickdrozd commented 6 years ago

Ah, I see. The quadrant constraints are indeed important. From Wikipedia:

The objective is to fill a 9×9 grid with digits so that each column, each row, and each of the nine 3×3 subgrids that compose the grid (also called "boxes", "blocks", or "regions") contains all of the digits from 1 to 9.

So your first example should fail:

(reazon--should-equal '()
    (reazon-sudoku-solve-4x4
     (a2 2) (a3 3) (a4 4)
     (b1 4) (b4 3)
     (c4 2)
     (d3 4)))

There should be more test cases to make this clear.

ebpa commented 6 years ago

😳 Lol; you're absolutely right (-: You would think I'd never done a sudoku before!

nickdrozd commented 6 years ago

There's still a lot of room for improvement here. For example, right now the solver is heavily biased towards clues given towards the upper left of the grid. Observe that (reazon-sudoku-solve-4x4 (a2 1) (b1 1)) terminates almost immediately, while (reazon-sudoku-solve-4x4 (c4 1) (d3 1)) takes several seconds. They both return the answer nil, and for the same reason, namely violating a quadrant constraint.

Right now the constraints are arranged as follows:

       (reazon-subseto range `(,a1 ,a2 ,a3 ,a4))
       (reazon-subseto range `(,a1 ,b1 ,c1 ,d1))
       (reazon-subseto range `(,a1 ,a2 ,b1 ,b2))
       (reazon-subseto range `(,b1 ,b2 ,b3 ,b4))
       (reazon-subseto range `(,a2 ,b2 ,c2 ,d2))
       (reazon-subseto range `(,a3 ,b3 ,c3 ,d3))
       (reazon-subseto range `(,a3 ,a4 ,b3 ,b4))
       (reazon-subseto range `(,a4 ,b4 ,c4 ,d4))
       (reazon-subseto range `(,c1 ,c2 ,c3 ,c4))
       (reazon-subseto range `(,c1 ,c2 ,d1 ,d2))
       (reazon-subseto range `(,d1 ,d2 ,d3 ,d4))
       (reazon-subseto range `(,c3 ,c4 ,d3 ,d4))

This means that the coordintates (c4 1) (d3 1) aren't discovered to be invalid until a lot of work has already been done -- lots of candidate solutions are generated and then ruled out, whereas the coordinates (a2 1) (b1 1) are ruled out quickly, and no further work needs to be done.

A smarter macro would rearrange the constraints at compile time according to the inputs. Of course, this is a constraint problem in its own right, so it would make sense to bring in Reazon to solve it. Could that be done quickly? Hmm...