/*
 * ex3_coloring.c -- graph k-coloring as SAT
 *
 *   The classical NP-complete decision problem: given a graph and an
 *   integer k, can every vertex be assigned one of k colours such that no
 *   edge has both endpoints the same colour?
 *
 *   We demonstrate on the Petersen graph: 10 vertices, 15 edges, famous
 *   in graph theory as a small counterexample to many naive conjectures.
 *   Its chromatic number is 3.
 *
 * Encoding:
 *
 *   Variable x[v][c] (1-indexed) means "vertex v has colour c".
 *
 *   - For each vertex v: at least one colour: (x[v][1] v ... v x[v][k]).
 *   - For each vertex v and pair c1 < c2: not both colours: (~x[v][c1] v ~x[v][c2]).
 *   - For each edge (u, v) and colour c: not same colour: (~x[u][c] v ~x[v][c]).
 *
 * What the SAT solver buys you:
 *
 *   Graph k-colouring is the textbook example where local domain
 *   propagation (the CSP/arc-consistency approach in the main book)
 *   struggles for dense graphs. CDCL has no special knowledge of
 *   graphs, but the learned clauses act as compiled-in "this combination
 *   of colour choices in this region is forbidden" memos -- exactly the
 *   global pruning that pure local propagation can't generate.
 *
 *   Compare the two outputs in this example: the solver proves
 *   3-colorability by finding an assignment, and proves 2-colorability
 *   is impossible by exhausting the search and refuting it via learned
 *   clauses.
 */
#include "sat.h"
#include <stdio.h>
#include <stdlib.h>

/* Petersen graph: 10 vertices labelled 0..9. */
static const int PETERSEN_N    = 10;
static const int PETERSEN_E[][2] = {
    /* outer 5-cycle */
    {0,1},{1,2},{2,3},{3,4},{4,0},
    /* inner pentagram */
    {5,7},{7,9},{9,6},{6,8},{8,5},
    /* spokes */
    {0,5},{1,6},{2,7},{3,8},{4,9},
};
static const int PETERSEN_EN  = 15;

static int solve_coloring(int n_verts, int n_edges,
                          const int edges[][2], int k,
                          long *out_conflicts) {
    int n_vars = n_verts * k;
    Sat *s = sat_new(n_vars);

    #define X(v, c) ((v) * k + (c) + 1)

    int *cl = malloc((size_t)k * sizeof(int));

    /* Each vertex gets at least one colour. */
    for (int v = 0; v < n_verts; v++) {
        for (int c = 0; c < k; c++) cl[c] = X(v, c);
        sat_add_clause(s, cl, k);
    }
    free(cl);

    /* At most one colour per vertex. */
    int pair[2];
    for (int v = 0; v < n_verts; v++)
        for (int c1 = 0; c1 < k; c1++)
            for (int c2 = c1 + 1; c2 < k; c2++) {
                pair[0] = -X(v, c1); pair[1] = -X(v, c2);
                sat_add_clause(s, pair, 2);
            }

    /* Endpoints of each edge differ in colour. */
    for (int e = 0; e < n_edges; e++)
        for (int c = 0; c < k; c++) {
            pair[0] = -X(edges[e][0], c); pair[1] = -X(edges[e][1], c);
            sat_add_clause(s, pair, 2);
        }

    int r = sat_solve(s);

    if (r == SAT_SATISFIABLE) {
        printf("    k=%d  SAT.  Colour assignment:\n      ", k);
        for (int v = 0; v < n_verts; v++) {
            int c_v = -1;
            for (int c = 0; c < k; c++)
                if (sat_value(s, X(v, c)) == SAT_TRUE) { c_v = c; break; }
            printf("v%d=%d ", v, c_v);
        }
        printf("\n");
    } else if (r == SAT_UNSATISFIABLE) {
        printf("    k=%d  UNSAT  (chromatic number > %d)\n", k, k);
    }
    *out_conflicts = sat_conflicts(s);
    long stats_dec  = sat_decisions(s);
    long stats_prop = sat_propagations(s);
    long stats_learn = sat_learned_clauses(s);
    sat_free(s);
    printf("      decisions=%ld  conflicts=%ld  propagations=%ld  learned=%ld\n\n",
           stats_dec, *out_conflicts, stats_prop, stats_learn);
    return r;
    #undef X
}

int main(void) {
    printf("=== Petersen graph k-colouring ===\n");
    printf("  vertices=%d  edges=%d\n\n", PETERSEN_N, PETERSEN_EN);

    long c2, c3;
    int r2 = solve_coloring(PETERSEN_N, PETERSEN_EN, PETERSEN_E, 2, &c2);
    int r3 = solve_coloring(PETERSEN_N, PETERSEN_EN, PETERSEN_E, 3, &c3);

    int ok = (r2 == SAT_UNSATISFIABLE) && (r3 == SAT_SATISFIABLE);
    printf("Petersen chromatic number = 3   %s\n", ok ? "(confirmed)" : "(MISMATCH)");
    return ok ? 0 : 1;
}
