/*
 * ex2_queens.c -- N-Queens as SAT
 *
 *   Place N queens on an N x N board so no two attack each other (no shared
 *   row, column, or diagonal). The same problem appears in the main book as
 *   a CSP / sparse-set demo; encoding it as SAT shows what changes when the
 *   underlying inference engine is generic clause-learning instead of
 *   problem-specific domain narrowing.
 *
 * Encoding:
 *
 *   Variable x[i][j] (1-indexed) means "there is a queen on square (i, j)".
 *   N x N variables in total.
 *
 *   - Each row has at least one queen.
 *   - At most one queen per row, column, and diagonal -- pairwise clauses.
 *
 * What the SAT solver buys you:
 *
 *   The CSP solver from the main book carries an explicit notion of variable
 *   domains and uses arc consistency to prune them. The SAT solver here
 *   knows nothing about queens or rows or diagonals; the only information
 *   it has is the list of clauses. The CDCL inner loop -- two-watched-literal
 *   propagation plus first-UIP analysis -- discovers, conflict by conflict,
 *   exactly the same kinds of inferences the dedicated CSP solver makes by
 *   construction. This is the price and the payoff of a generic solver:
 *   you encode any problem in a single uniform language, and a single
 *   uniform algorithm pulls structure out of it.
 *
 *   For N = 8 this is essentially instant. The interesting numbers to watch
 *   are propagations per conflict (how much "free" inference each branch
 *   triggers) and the ratio of decisions to conflicts.
 */
#include "sat.h"
#include <stdio.h>
#include <stdlib.h>

int main(int argc, char **argv) {
    int N = (argc > 1) ? atoi(argv[1]) : 8;
    if (N < 1 || N > 32) { fprintf(stderr, "N out of range\n"); return 1; }

    int n_vars = N * N;
    Sat *s = sat_new(n_vars);

    #define X(i, j) ((i) * N + (j) + 1)

    int n_cl = 0;
    int *row_cl = malloc((size_t)N * sizeof(int));

    /* At least one queen per row. (N rows, N-literal clauses.) */
    for (int i = 0; i < N; i++) {
        for (int j = 0; j < N; j++) row_cl[j] = X(i, j);
        sat_add_clause(s, row_cl, N);
        n_cl++;
    }
    free(row_cl);

    /* Pairwise "at most one" clauses for each attack line. */
    int pair[2];

    /* Rows. */
    for (int i = 0; i < N; i++)
        for (int j1 = 0; j1 < N; j1++)
            for (int j2 = j1 + 1; j2 < N; j2++) {
                pair[0] = -X(i, j1); pair[1] = -X(i, j2);
                sat_add_clause(s, pair, 2); n_cl++;
            }

    /* Columns. */
    for (int j = 0; j < N; j++)
        for (int i1 = 0; i1 < N; i1++)
            for (int i2 = i1 + 1; i2 < N; i2++) {
                pair[0] = -X(i1, j); pair[1] = -X(i2, j);
                sat_add_clause(s, pair, 2); n_cl++;
            }

    /* Diagonals  (i - j = const). */
    for (int d = -(N - 1); d <= N - 1; d++) {
        int sqs[64], k = 0;
        for (int i = 0; i < N; i++) {
            int j = i - d;
            if (j >= 0 && j < N) sqs[k++] = X(i, j);
        }
        for (int a = 0; a < k; a++)
            for (int b = a + 1; b < k; b++) {
                pair[0] = -sqs[a]; pair[1] = -sqs[b];
                sat_add_clause(s, pair, 2); n_cl++;
            }
    }

    /* Anti-diagonals  (i + j = const). */
    for (int d = 0; d < 2 * N - 1; d++) {
        int sqs[64], k = 0;
        for (int i = 0; i < N; i++) {
            int j = d - i;
            if (j >= 0 && j < N) sqs[k++] = X(i, j);
        }
        for (int a = 0; a < k; a++)
            for (int b = a + 1; b < k; b++) {
                pair[0] = -sqs[a]; pair[1] = -sqs[b];
                sat_add_clause(s, pair, 2); n_cl++;
            }
    }

    printf("=== %d-Queens ===\n", N);
    printf("  variables : %d\n", n_vars);
    printf("  clauses   : %d\n\n", n_cl);

    int r = sat_solve(s);

    if (r == SAT_SATISFIABLE) {
        printf("  result    : SAT\n\n");
        for (int i = 0; i < N; i++) {
            printf("    ");
            for (int j = 0; j < N; j++)
                putchar(sat_value(s, X(i, j)) == SAT_TRUE ? 'Q' : '.');
            putchar('\n');
        }
        printf("\n");
    } else if (r == SAT_UNSATISFIABLE) {
        printf("  result    : UNSAT  (only happens for N=2, 3)\n");
    }

    printf("  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 r == SAT_SATISFIABLE ? 0 : (N == 2 || N == 3) ? 0 : 1;
}
