#include #include #include #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; }