/*
 * ex4_sudoku.c -- 9x9 sudoku as SAT
 *
 * Encoding (the canonical "minimal" sudoku-to-SAT, 729 variables):
 *
 *   Variable x[r][c][d] (1-indexed) means "the digit at row r, column c
 *   is d". Indices: r, c, d in 0..8.
 *
 *   Constraints:
 *     - Each cell has at least one digit.
 *     - Each cell has at most one digit  (pairwise).
 *     - Each row contains each digit at least once.
 *     - Each column contains each digit at least once.
 *     - Each 3x3 box contains each digit at least once.
 *     - "At most one" versions follow from the "at least one" plus
 *       counting (9 cells, 9 digits), and are implied by the cell-uniqueness
 *       clauses, so we can omit the per-row/col/box "at most" clauses
 *       without changing the solution set. We include them anyway because
 *       they give unit propagation more to chew on and make the solver
 *       much faster in practice.
 *     - Each clue is an additional unit clause.
 *
 *   Total clauses for an empty board: 11745 (with the redundant "at most
 *   one" for row/col/box added) or 8829 (just the cell uniqueness).
 *
 * What the SAT solver buys you:
 *
 *   Sudoku is the canonical demo of "give me a real puzzle, get a real
 *   answer". Hand-encode the rules once, throw any puzzle at it, get an
 *   answer back. The encoding is naive -- no clever propagation rules,
 *   no constraint-specific reasoning -- and CDCL still solves human-hard
 *   sudoku in milliseconds. The redundant clauses are an interesting
 *   pedagogical point: adding more constraints (provably the same
 *   formula) makes the solver dramatically faster, because unit
 *   propagation now sees more deductions for free.
 *
 *   The puzzle below is "AI Escargot", widely cited as one of the
 *   hardest sudokus published. It was specifically designed to be
 *   adversarial to standard human and computer solvers.
 */
#include "sat.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

/* "AI Escargot" -- a famously hard sudoku. (Arto Inkala, 2006.) */
static const char *PUZZLE =
    "1....7.9."
    ".3..2...8"
    "..96..5.."
    "..53..9.."
    ".1..8...2"
    "6....4..."
    "3......1."
    ".4......7"
    "..7...3..";

static int X(int r, int c, int d) { return r * 81 + c * 9 + d + 1; }

int main(void) {
    Sat *s = sat_new(9 * 9 * 9);
    int n_cl = 0;
    int cl[9];

    /* Per cell: at least one digit, at most one digit. */
    for (int r = 0; r < 9; r++)
        for (int c = 0; c < 9; c++) {
            for (int d = 0; d < 9; d++) cl[d] = X(r, c, d);
            sat_add_clause(s, cl, 9); n_cl++;
            for (int d1 = 0; d1 < 9; d1++)
                for (int d2 = d1 + 1; d2 < 9; d2++) {
                    int pair[2] = { -X(r, c, d1), -X(r, c, d2) };
                    sat_add_clause(s, pair, 2); n_cl++;
                }
        }

    /* Each row contains each digit (at least once). */
    for (int r = 0; r < 9; r++)
        for (int d = 0; d < 9; d++) {
            for (int c = 0; c < 9; c++) cl[c] = X(r, c, d);
            sat_add_clause(s, cl, 9); n_cl++;
        }

    /* Each column contains each digit. */
    for (int c = 0; c < 9; c++)
        for (int d = 0; d < 9; d++) {
            for (int r = 0; r < 9; r++) cl[r] = X(r, c, d);
            sat_add_clause(s, cl, 9); n_cl++;
        }

    /* Each 3x3 box contains each digit. */
    for (int br = 0; br < 3; br++)
        for (int bc = 0; bc < 3; bc++)
            for (int d = 0; d < 9; d++) {
                int k = 0;
                for (int dr = 0; dr < 3; dr++)
                    for (int dc = 0; dc < 3; dc++)
                        cl[k++] = X(br * 3 + dr, bc * 3 + dc, d);
                sat_add_clause(s, cl, 9); n_cl++;
            }

    /* Redundant "at most one per row/col/box" clauses (speed). */
    for (int r = 0; r < 9; r++)
        for (int d = 0; d < 9; d++)
            for (int c1 = 0; c1 < 9; c1++)
                for (int c2 = c1 + 1; c2 < 9; c2++) {
                    int pair[2] = { -X(r, c1, d), -X(r, c2, d) };
                    sat_add_clause(s, pair, 2); n_cl++;
                }
    for (int c = 0; c < 9; c++)
        for (int d = 0; d < 9; d++)
            for (int r1 = 0; r1 < 9; r1++)
                for (int r2 = r1 + 1; r2 < 9; r2++) {
                    int pair[2] = { -X(r1, c, d), -X(r2, c, d) };
                    sat_add_clause(s, pair, 2); n_cl++;
                }
    for (int br = 0; br < 3; br++)
        for (int bc = 0; bc < 3; bc++)
            for (int d = 0; d < 9; d++) {
                int sqs[9], k = 0;
                for (int dr = 0; dr < 3; dr++)
                    for (int dc = 0; dc < 3; dc++)
                        sqs[k++] = X(br * 3 + dr, bc * 3 + dc, d);
                for (int a = 0; a < 9; a++)
                    for (int b = a + 1; b < 9; b++) {
                        int pair[2] = { -sqs[a], -sqs[b] };
                        sat_add_clause(s, pair, 2); n_cl++;
                    }
            }

    /* Clues as unit clauses. */
    int n_clues = 0;
    for (int r = 0; r < 9; r++)
        for (int c = 0; c < 9; c++) {
            char ch = PUZZLE[r * 9 + c];
            if (ch >= '1' && ch <= '9') {
                int d = ch - '1';
                int unit = X(r, c, d);
                sat_add_clause(s, &unit, 1);
                n_cl++; n_clues++;
            }
        }

    printf("=== Sudoku (AI Escargot) ===\n");
    printf("\nPuzzle:\n");
    for (int r = 0; r < 9; r++) {
        printf("  ");
        for (int c = 0; c < 9; c++) {
            char ch = PUZZLE[r * 9 + c];
            putchar(ch == '.' ? '.' : ch);
            putchar(c % 3 == 2 && c < 8 ? '|' : ' ');
        }
        putchar('\n');
        if (r % 3 == 2 && r < 8) printf("  ---------+---------+---------\n");
    }

    printf("\n  variables : %d\n", 9 * 9 * 9);
    printf("  clauses   : %d  (incl. %d clues)\n\n", n_cl, n_clues);

    int r = sat_solve(s);
    if (r != SAT_SATISFIABLE) {
        printf("  result: %s\n", r == SAT_UNSATISFIABLE ? "UNSAT" : "unknown");
        sat_free(s);
        return 1;
    }

    printf("Solution:\n");
    for (int r = 0; r < 9; r++) {
        printf("  ");
        for (int c = 0; c < 9; c++) {
            int found = 0;
            for (int d = 0; d < 9; d++) {
                if (sat_value(s, X(r, c, d)) == SAT_TRUE) {
                    putchar('1' + d); found = 1; break;
                }
            }
            if (!found) putchar('?');
            putchar(c % 3 == 2 && c < 8 ? '|' : ' ');
        }
        putchar('\n');
        if (r % 3 == 2 && r < 8) printf("  ---------+---------+---------\n");
    }

    printf("\n  decisions   = %ld\n", sat_decisions(s));
    printf("  conflicts   = %ld\n", sat_conflicts(s));
    printf("  propagations= %ld\n", sat_propagations(s));
    printf("  restarts    = %ld\n", sat_restarts(s));
    printf("  learned cls = %ld\n", sat_learned_clauses(s));

    sat_free(s);
    return 0;
}
