Sudoku core.logic

sud4-ckanren.clj

(defne all-distinctfd [l]
  ([()])
  ([[h . t]]
     (distinctfd h)
     (all-distinctfd t)))

(run 1 [q]
     (fresh [a1 a2 a3 a4
             b1 b2 b3 b4
             c1 c2 c3 c4
             d1 d2 d3 d4]

            (== q [[a1 a2 a3 a4]
                   [b1 b2 b3 b4]
                   [c1 c2 c3 c4]
                   [d1 d2 d3 d4]])

            (infd a1 a2 a3 a4
                  b1 b2 b3 b4
                  c1 c2 c3 c4
                  d1 d2 d3 d4
                  (interval 1 6))  ;; <- Must be bumped to 6 for it to work?

            (let [row1 [a1 a2 a3 a4]
                  row2 [b1 b2 b3 b4]
                  row3 [c1 c2 c3 c4]
                  row4 [d1 d2 d3 d4]
                  col1 [a1 b1 c1 d1]
                  col2 [a2 b2 c2 d2]
                  col3 [a3 b3 c3 d3]
                  col4 [a4 b4 c4 d4]
                  sq1 [a1 a2 b1 b2]
                  sq2 [a3 a4 b3 b4]
                  sq3 [c1 c2 d1 d2]
                  sq4 [c3 c4 d3 d4]]
              
              (all-distinctfd [row1 row2 row3 row4
                               col1 col2 col3 col4
                               sq1 sq2 sq3 sq4
                               ]))))

sud9-ckanren.clj

  (run 1 [q]
       (fresh [a1 a2 a3 a4 a5 a6 a7 a8 a9
               b1 b2 b3 b4 b5 b6 b7 b8 b9
               c1 c2 c3 c4 c5 c6 c7 c8 c9
               d1 d2 d3 d4 d5 d6 d7 d8 d9
               e1 e2 e3 e4 e5 e6 e7 e8 e9
               f1 f2 f3 f4 f5 f6 f7 f8 f9
               g1 g2 g3 g4 g5 g6 g7 g8 g9
               h1 h2 h3 h4 h5 h6 h7 h8 h9
               i1 i2 i3 i4 i5 i6 i7 i8 i9]

              (== a5 2)
              (== a7 9)
              (== b5 6)
              (== b6 3)
              (== b9 8)
              (== c1 3)
              (== c6 8)
              (== c7 1)
              (== c8 4)
              (== d5 4)
              (== d7 8)
              (== d9 7)
              (== e2 8)
              (== e3 4)
              (== e6 6)
              (== e7 1)

              (== q [[a1 a2 a3 a4 a5 a6 a7 a8 a9]
                     [b1 b2 b3 b4 b5 b6 b7 b8 b9]
                     [c1 c2 c3 c4 c5 c6 c7 c8 c9]
                     [d1 d2 d3 d4 d5 d6 d7 d8 d9]
                     [e1 e2 e3 e4 e5 e6 e7 e8 e9]
                     [f1 f2 f3 f4 f5 f6 f7 f8 f9]
                     [g1 g2 g3 g4 g5 g6 g7 g8 g9]
                     [h1 h2 h3 h4 h5 h6 h7 h8 h9]
                     [i1 i2 i3 i4 i5 i6 i7 i8 i9]])

              (infd a1 a2 a3 a4 a5 a6 a7 a8 a9
                    b1 b2 b3 b4 b5 b6 b7 b8 b9
                    c1 c2 c3 c4 c5 c6 c7 c8 c9
                    d1 d2 d3 d4 d5 d6 d7 d8 d9
                    e1 e2 e3 e4 e5 e6 e7 e8 e9
                    f1 f2 f3 f4 f5 f6 f7 f8 f9
                    g1 g2 g3 g4 g5 g6 g7 g8 g9
                    h1 h2 h3 h4 h5 h6 h7 h8 h9
                    i1 i2 i3 i4 i5 i6 i7 i8 i9
                    (interval 1 14))

              (let [row1 [a1 a2 a3 a4 a5 a6 a7 a8 a9]
                    row2 [b1 b2 b3 b4 b5 b6 b7 b8 b9]
                    row3 [c1 c2 c3 c4 c5 c6 c7 c8 c9]
                    row4 [d1 d2 d3 d4 d5 d6 d7 d8 d9]
                    row5 [e1 e2 e3 e4 e5 e6 e7 e8 e9]
                    row6 [f1 f2 f3 f4 f5 f6 f7 f8 f9]
                    row7 [g1 g2 g3 g4 g5 g6 g7 g8 g9]
                    row8 [h1 h2 h3 h4 h5 h6 h7 h8 h9]
                    row9 [i1 i2 i3 i4 i5 i6 i7 i8 i9]
                    col1 [a1 b1 c1 d1 e1 f1 g1 h1 i1]
                    col2 [a2 b2 c2 d2 e2 f2 g2 h2 i2]
                    col3 [a3 b3 c3 d3 e3 f3 g3 h3 i3]
                    col4 [a4 b4 c4 d4 e4 f4 g4 h4 i4]
                    col5 [a5 b5 c5 d5 e5 f5 g5 h5 i5]
                    col6 [a6 b6 c6 d6 e6 f6 g6 h6 i6]
                    col7 [a7 b7 c7 d7 e7 f7 g7 h7 i7]
                    col8 [a8 b8 c8 d8 e8 f8 g8 h8 i8]
                    col9 [a9 b9 c9 d9 e9 f9 g9 h9 i9]
                    sq1 [a1 a2 a3 b1 b2 b3 c1 c2 c3]
                    sq2 [a4 a5 a6 b4 b5 b6 c4 c5 c6]
                    sq3 [a7 a8 a9 b7 b8 b9 c7 c8 c9]
                    sq4 [d1 d2 d3 e1 e2 e3 f1 f2 f3]
                    sq5 [d4 d5 d6 e4 e5 e6 f4 f5 f6]
                    sq6 [d7 d8 d9 e7 e8 e9 f7 f8 f9]
                    sq7 [g1 g2 g3 h1 h2 h3 i1 i2 i3]
                    sq8 [g4 g5 g6 h4 h5 h6 i4 i5 i6]
                    sq9 [g7 g8 g9 h7 h8 h9 i7 i8 i9]]
                
                (all-distinctfd [row1 row2 row3 row4 row5 row6 row7 row8 row9
                                 col1 col2 col3 col4 col5 col6 col7 col8 col9
                                 sq1 sq2 sq3 sq4 sq5 sq6 sq7 sq8 sq9
                                 ]))))

all-infd could be replace with:

(infd x y z ... (interval 4))

all-distinctfd also unecessary

(distinctfd [x y z ....])

Cheers dude,

care to comment on the question above? Why we have to (interval 1 6) instead of (interval 1 4)???

no idea, can't look into at the moment. But I can use this gist to create a test case when I have time to look into it.

I believe I may have fixed the (interval 4) issue in master. Is the larger sudoku case working for you?

Cool.

I can't get the 9x9 working either. I did double check the rules, they look OK.

You might try by removing the (== a5 2), (== a7 9), ... for a run on a empty board?

(we want the 9x9 working with (interval 1 9) as well)

(interval 9) works as far as I can tell. If I take out the initial board values then I can get a result. Your code does not produce a solution in cKanren Scheme either but again, taking out the initial board values makes it work.

All this said, this cKanren program runs surprisingly slow - Clojure & Scheme both. I think cKanren at the moment is a bit interval centric making it unoptimal from using distinctfd on problems like this one. Can't say at this point what's wrong or if it can be improved - I need to spend some time with the code + YourKit.

Small update. Switching to a type that doesn't use an interval representation, (domain 1 2 3 4 5 6 7 8 9) vs. (interval 1 9) does speed things up. However not by as much as I hoped. Performance still seems about 10X too slow to me. Still investigating ...

There is a typo in the big sudoku example, e7 & c7 are both 1.

If I set e7 to 3 and I use master (just landed a 3X perf boost to distinctfd), I can solve this one in about ~90-100ms

Cheers dude, I was never in doubt! :)

Also, I like your cleaned up version in that other gist.

This is now faster than my hand rolled backtracking solution.