I was wrong about being wrong in my last post. My original predictions were correct after all.
I had skimmed Bram Cohen’s post too quickly, and when I tried following his approach, my branching heuristic was simply to take the clause with the fewest literals.
What happens if we do this? Initially, there are many clauses consisting of 2 negative literals, and a few consisting of 9 positive literals. Thus most of the time we pick a negative clause. We’ll only ever pick a positive clause if only 2 literals are left. By this stage, it’s no different from a negative clause because assigning to true to one of the variables is the same as assigning false to the other.
In other words, apart from unit propagation, each step simply eliminates a particular digit from a particular cell, depending on the the order of the clauses. That is, apart from unit propagation, this is no different to brute force!
I failed to see this when I tried writing a SAT solver, and wound up surprised at the results. It was only later I realized I should have been ignoring negative clauses to make Cohen’s program behave like like Knuth’s: the positive clauses correspond exactly to the columns in the exact cover problem, and the literals within a positive clause correspond to 1s in a column.
The only difference is performance: manipulating lists or arrays to find which negative clauses affect which positive clauses is much slower than manipulating a few links to find which rows affect which columns.
When I returned to Cohen’s post, I realized he had explicitly mentioned skipping negative clauses during branching.
Below is my C translation of Cohen’s program. It is more efficient than the original because of in-place deletion and undeletion of clauses and literals. (I’ve used “dancing arrays” instead of Python lists.) As expected, this solver orders of magnitude slower than my dancing links solver, but handily beats Norvig’s program.
#include <ctype.h>
#include <limits.h>
#include <stdio.h>
#define F(i,n) for(int i = 0; i < n; i++)
int main() {
int a[9][9] = {{0}}, x[4*9*9*(1+9*8/2)][10] = {{0}}, n = 0, m;
// Read a sudoku.
F(i, 9) F(j, 9) do if (EOF == (m = getchar())) return 1; while(
isdigit(m) ? a[i][j] = m - '0', 0 : m != '.');
int enc(int a, int b, int c) {return 9*9*a + 9*b + c + 1;}
void add(int n, int a, int b, int c) {x[n][++*x[n]] = enc(a, b, c);}
F(i, 9) F(j, 9) F(k, 9 || (n += 4, 0)) { // At least one digit per:
add(n , k, i, j); // ...box
add(n+1, i, k, j); // ...column
add(n+2, i, j, k); // ...row
add(n+3, i, j/3*3 + k/3, j%3*3 + k%3); // ...3x3 region.
}
for(int i = n-1; i >= 0; i--) F(j, x[i][0]) F(k, j) {
x[n][1] = -x[i][j+1]; // At most one digit per positive clause.
x[n][2] = -x[i][k+1]; // (Hence the 9 choose 2 factor above.)
x[n++][0] = 2;
}
int y[n], out[9*9*9];
F(i, n) y[i] = i;
int assign(int n, int v) {
F(i, n) {
int k = y[i];
F(j, x[k][0]) {
if (x[k][j+1] == v) { // Satisfied clause:
y[i--] = y[--n]; // Swap with last one
y[n] = k; // and decrement array count.
break;
} else if (x[k][j+1] == -v) { // False literal:
x[k][j+1] = x[k][x[k][0]]; // Swap with last one
x[k][x[k][0]--] = -v; // and decrement clause size.
break; // Assume literals are unique in a clause.
}
}
}
return n;
}
void solve(int n) {
int s = INT_MAX, t = 0;
if (!n) { // Print solution.
F(i, m) if ((t = out[i] - 1) >= 0) a[t/9%9][t%9] = t/9/9 + 1;
F(r, 9) F(c, 9 || 0*puts("")) putchar('0'+a[r][c]);
return;
}
F(i, n) if (x[y[i]][0] < s) { // Find smallest positive clause.
if (x[y[i]][0] > 1 && x[y[i]][1] < 0) continue;
if (!(s = x[y[i]][0])) return; // Empty clause: no solution.
t = y[i];
}
void try(int v) {
solve(assign(n, out[m++] = v));
F(i, n) { // Undo any clause deletions.
int k = y[i];
if (x[k][0] < 9 && x[k][x[k][0]+1] == -v) x[k][0]++;
}
m--;
}
try(x[t][1]);
if (s > 1) try(-x[t][1]);
}
// Fill in the given digits, and go!
F(r, 9) F(c, 9) if (a[r][c]) n = assign(n, enc(a[r][c]-1, r, c));
m = 0, solve(n); // Reuse m as count of 'out' array.
return 0;
}
