Comments are moderated. It may take a few minutes before your comment appears.

Markdown is supported in your comments.

Some of the limitations should be immediately obvious. For example, all variables are boolean and in most puzzles integers would be useful. But this is not too bad; it can be compensated for by using extra variable terms. A bigger problem is the number of clauses required. For example, sudoku needs 11600 clauses just to establish the physics of the grid. (While plugging in the initial board state only takes one clause per cell.) With some clever logic the required clauses can be cut down to 3 thousand, but there is no benefit to do so besides mathematical pedantry. In fact, highly minimal expressions can often take longer to solve because more backtracking is needed. |