/*
 * ex1_pigeonhole.c -- the pigeonhole principle
 *
 *   m+1 pigeons, m holes; each pigeon in some hole; no two pigeons in the
 *   same hole. Trivially impossible -- you cannot put 7 pigeons in 6 holes
 *   without two pigeons sharing.
 *
 * What the SAT solver buys you:
 *
 *   PHP is a famous testing ground for combinatorial inference. The
 *   shortest *resolution* refutation of PHP(m+1, m) has size exponential
 *   in m -- Haken's classical result from 1985. Naive DPLL inherits the
 *   same exponential lower bound; it cannot prove PHP(7, 6) without an
 *   astronomical search.
 *
 *   Modern CDCL still has the same theoretical lower bound (clause learning
 *   does not break the resolution barrier) but in practice the conflict
 *   analysis machinery is dramatically more efficient than blind DPLL.
 *   Small instances solve in tens or hundreds of conflicts; the learned
 *   clauses encode the "I already tried this kind of failure" knowledge
 *   that DPLL has to re-derive from scratch every time.
 *
 *   This example shows the kind of UNSAT proof a CDCL solver constructs
 *   for free, and lets you crank m up to see when it starts to hurt.
 *
 * Variables: x[i][j] = "pigeon i is in hole j"  (i in 0..M, j in 0..M-1).
 */
#include "sat.h"
#include <stdio.h>
#include <stdlib.h>

int main(int argc, char **argv) {
    int M = (argc > 1) ? atoi(argv[1]) : 6;     /* default: 7 pigeons, 6 holes */
    if (M < 2 || M > 30) { fprintf(stderr, "M out of range\n"); return 1; }

    int n_pigeons = M + 1;
    int n_holes   = M;
    int n_vars    = n_pigeons * n_holes;

    Sat *s = sat_new(n_vars);

    /* Variable id: x[i][j] = i * n_holes + j + 1  (1-indexed). */
    #define X(i, j) ((i) * n_holes + (j) + 1)

    /* (1) Each pigeon is in at least one hole. */
    int n_clauses = 0;
    int *cl = malloc((size_t)n_holes * sizeof(int));
    for (int i = 0; i < n_pigeons; i++) {
        for (int j = 0; j < n_holes; j++) cl[j] = X(i, j);
        sat_add_clause(s, cl, n_holes);
        n_clauses++;
    }
    free(cl);

    /* (2) No two pigeons share a hole. */
    for (int j = 0; j < n_holes; j++) {
        for (int i1 = 0; i1 < n_pigeons; i1++) {
            for (int i2 = i1 + 1; i2 < n_pigeons; i2++) {
                int pair[2] = { -X(i1, j), -X(i2, j) };
                sat_add_clause(s, pair, 2);
                n_clauses++;
            }
        }
    }

    printf("=== PHP(%d, %d) ===\n", n_pigeons, n_holes);
    printf("  variables : %d\n", n_vars);
    printf("  clauses   : %d\n\n", n_clauses);

    int r = sat_solve(s);

    printf("  result    : %s\n", r == SAT_UNSATISFIABLE ? "UNSAT (as expected)" :
                                  r == SAT_SATISFIABLE  ? "SAT (BUG!)" : "unknown");
    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_UNSATISFIABLE ? 0 : 1;
}
