This is based on the excellent work of Claire Alvis, Will Byrd & Dan Friedman who continue to improve their Scheme miniKanren system. miniKanren embeds Prolog semantics into Scheme. core.logic implements and extends that work in Clojure. This code highlights the new cKanren extensions Claire et. al. have developed which enables Constraint Logic Programming in miniKanren - http://en.wikipedia.org/wiki/Constraint_logic_programming.
One neat bit about this is that this is surprisingly efficient given the generality and how new this work is. The HN crowd will be familiar with Norvig's fantastic sudoku solver in Python - http://norvig.com/sudoku.html. This core.logic solver can solve easy sudoku problems ~6-7ms. Norvig's hard one that takes 188 seconds in Python takes ~60ms. More benchmarking needs to be done, but this is promising especially since this is a generic all-different FD constraint over small domains as well as intervals - so it's not specific to sudoku.
Feel free to ask any questions.
UPDATE: to be extra clear this is not just about sudoku. The following is also now possible to express under the same framework -
(run* [q]
(fresh [x y z]
(infd x y z (interval 1 3))
(+fd x y z)
(== q [x y z])))
;; => ([1 1 2] [2 1 3] [1 2 3])
This program shows all possibilities where x, y & z range over 1, 2, 3 where x & y add up to z.
Have you found any multiple-order-of-magnitude spike of processing time for any other "hard" ones? Or, more generally, any quantization of time as a function of difficulty?
Yes I had time to check that one of the hardest ones listed on Wikipedia takes ~570ms on my machine, so that's nearly 100X slower. I haven't had time yet to do any real comprehensive benchmarking or quantization a la Norvig. Hopefully soon.
I've been anxiously waiting for you to make this available for some time. All other personal coding projects are now secondary to this. I can't wait to play!
It's a mix of Claire et al's ideas and my own. A distinctfd constraint takes a list of vars and creates the real distinctfd constraint for each var, these are put into the constraint store. They do not run unless the var reaches a single possible value. At which point they run once and are purged from the constraint store. Each constraint has a list of the vars involved plus the list of known single values for the other vars. When it runs if the constrained vars' value exists in the single values set it fails. If it doesn't, the constraint removes the value from any other var that has a domain of values.
It's actually pretty simple. Most of the performance is from Clojure, the purely functional design which gives us backtracking "for free", and the random access nature of the constraint store.
People thinking "Oh god, not another x in y lines of z" (I first thought this as well), be open minded and try to read the code. It might not be in a language you know, but try and see if you can understand the last part:
Which, for me, reads "Take one solution and return q, where q is equal to vars, and every var is either 1, 2, 3, 4, 5, 6, 7, 8 or 9. Then initialize the variables with the already placed elements we've been given, and ensure that every row, column and square has only distinct elements."
Now, I don't know about you, but this sounds actually like the rules of Sudoku for me, not some algorithm on how to solve it. That's amazing, and should really get you to think about trying out logic programming if you haven't already. There's a lot of power in it, and using it in production code might not be as far away as it seems.
Coding in Prolog feels very much the same, 'though the syntax is frustrating. My solver came out somewhat more declarative but a little more verbose, 'though.
Just FYI, "though" is an English word, synonymous with "although." It doesn't require an apostrophe, and in fact "although" is incorrect when used at the end of a sentence.
Its very nicely coded and credit to the author, but I think people might infer from your description something more than its actually doing, which is basically 'brute force' - trying every combination and crossing them off when they fail (hence your quoted code above).
The alternative approach would be to work like humans do, looking for the next 'right' square (rather than this, which looks for the next 'wrong' combination). This would be much more difficult but would solve the hard problems much faster and computationally elegantly (though its only a matter of seconds anyway!).
[EDIT] I created an derivative version in ruby for anyone who is interested (42 lines of code - probably could be shorter) - http://pastebin.com/ecjQzzU6
I don't understand much clojure but looking at it it would seem to me the solution is actually found in a smart way, iteratively restricting the domains for a single variable and then propagating the changes (which I think is the standard constraint programming approach).
What happens if you input a puzzle that's unsolvable? Does the program run forever trying to seek a solution, or can it realize the puzzle is unsolvable?
This is an optimization model of an assignment problem. Certain problems should be approached not only with the right language, but also with the right tool. Optimization solvers are not always the best tool for feasibility problems, but this solver (of the branch-and-bound type) can also solve difficult sudoku instances.
That was absolutely horrifying. It's like a train wreck. I can look away. I read the entire thing.
I'm sure that my thought process while developing code is ugly and messy and scattered too. However, this level of TDD just strikes me as a mechanism to generate legacy code to maintain. It's as if, upon embarking on a new project, these people so miss their giant codebases, with slow builds, and spaghetti grep results, that they have concocted a way to maximize the rate of legacy code generation, so they can feel at home again. The result is that you do a lot of what feels like work. You're constantly moving code around, changing names, tweaking stuff. You tell yourself that you're "Refactoring" and that's how it's supposed to work.
To clarify this code snippet is not just about solving sudoku. This demonstrates brevity, generality, and it's zippy to boot! It's an extensible CLP framework, see my other comment.
Maybe this might help some helpless other Clojure newbees like me: I just compiled clojure and core.logic from the github repos, and it seems that the author just changed "everyo" to "everyg" very recently:
More details about this code here http://dosync.posterous.com/sudoku and here http://dosync.posterous.com/friendlier-shorter
This is based on the excellent work of Claire Alvis, Will Byrd & Dan Friedman who continue to improve their Scheme miniKanren system. miniKanren embeds Prolog semantics into Scheme. core.logic implements and extends that work in Clojure. This code highlights the new cKanren extensions Claire et. al. have developed which enables Constraint Logic Programming in miniKanren - http://en.wikipedia.org/wiki/Constraint_logic_programming.
One neat bit about this is that this is surprisingly efficient given the generality and how new this work is. The HN crowd will be familiar with Norvig's fantastic sudoku solver in Python - http://norvig.com/sudoku.html. This core.logic solver can solve easy sudoku problems ~6-7ms. Norvig's hard one that takes 188 seconds in Python takes ~60ms. More benchmarking needs to be done, but this is promising especially since this is a generic all-different FD constraint over small domains as well as intervals - so it's not specific to sudoku.
Feel free to ask any questions.
UPDATE: to be extra clear this is not just about sudoku. The following is also now possible to express under the same framework -
This program shows all possibilities where x, y & z range over 1, 2, 3 where x & y add up to z.