SAT


Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

Boolean satisfaction solvers (SAT) ace every one of these objectives. They have made me a much more capable solver. When faced with a logic puzzle, it is not a question of if I can solve it but how long it will take. Based on my timings for a dozen puzzles or so, it has made me at least 60 times faster. Maybe more, because some of those were puzzles I had written off as unsolvable. Sadly I have not found a thorough introduction to boolean satisfaction. There are lots of research papers along the lines of "We solved the Rubik's Cube with only 100k clauses," but nothing about how they came up with the clauses. There is no analogous text along the lines of "Balancing your Checkbook and Other Everyday Applications of Arithmetic". I've been working on filling this void. You are reading it now, and are unlucky enough be one of the first. Expect rough edges and don't hesitate to ask for clarification.

Name:
Mail: (not shown)

Please type this: