/*
 * ex3_nqueens.c -- N-Queens via alldifferent.
 *
 * The classical CP encoding of N-Queens: one variable per row, the
 * value being the column the queen sits in. Three alldifferent
 * constraints cover the three families of attack lines:
 *
 *     alldifferent(col_0, col_1, ..., col_{N-1})        -- columns
 *     alldifferent(col_0 + 0, col_1 + 1, ...)           -- "/" diagonals
 *     alldifferent(col_0 - 0, col_1 - 1, ...)           -- "\" diagonals
 *
 * To use the second and third we need auxiliary integer variables
 * d1_i and d2_i with the linear constraints d1_i == col_i + i and
 * d2_i == col_i - i. The LCG core only supports linear inequalities,
 * so we encode equality as two inequalities (le and ge).
 *
 * Compare with the SAT-only encoding in the SAT annex (ex2_queens.c):
 * that one needs O(N^3) pairwise exclusion clauses. Here we need three
 * alldifferent constraints, regardless of N. The propagator does the
 * work that the SAT-only encoding pushed into the clause database.
 *
 * Defaults to N = 6 (small enough to be instant; large enough to
 * exercise the Hall-set logic). Run with `./ex3_nqueens 8` to try
 * other sizes.
 */
#include "lcg.h"

#include <stdio.h>
#include <stdlib.h>

static IntVar make_offset_var(LcgCtx *ctx, IntVar src, int offset,
                              int dom_lo, int dom_hi, const char *name)
{
    /* aux == src + offset, encoded as:
     *     aux - src <=  offset
     *    -aux + src <= -offset
     */
    IntVar aux = lcg_new_int_var(ctx, dom_lo, dom_hi, name);
    int     c1[2] = {  1, -1 }; IntVar v[2] = { aux, src };
    int     c2[2] = { -1,  1 };
    lcg_post_linear_le(ctx, c1, v, 2,  offset);
    lcg_post_linear_le(ctx, c2, v, 2, -offset);
    return aux;
}

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

    LcgCtx *ctx = lcg_new();

    /* col[i] in [0..N-1] */
    IntVar *col = malloc((size_t)N * sizeof(IntVar));
    char name[16];
    for (int i = 0; i < N; i++) {
        snprintf(name, sizeof name, "col%d", i);
        col[i] = lcg_new_int_var(ctx, 0, N - 1, name);
    }

    /* d1[i] = col[i] + i  in [i..N-1+i] */
    /* d2[i] = col[i] - i  in [-i..N-1-i] */
    IntVar *d1 = malloc((size_t)N * sizeof(IntVar));
    IntVar *d2 = malloc((size_t)N * sizeof(IntVar));
    for (int i = 0; i < N; i++) {
        snprintf(name, sizeof name, "d1_%d", i);
        d1[i] = make_offset_var(ctx, col[i],  i, i,         N - 1 + i, name);
        snprintf(name, sizeof name, "d2_%d", i);
        d2[i] = make_offset_var(ctx, col[i], -i, -i,        N - 1 - i, name);
    }

    lcg_post_alldifferent(ctx, col, N);
    lcg_post_alldifferent(ctx, d1,  N);
    lcg_post_alldifferent(ctx, d2,  N);

    int r = lcg_solve(ctx);

    printf("=== Phase 3: %d-Queens via alldifferent ===\n\n", N);
    printf("  status         = %s\n",
        r == LCG_SAT   ? "SAT" :
        r == LCG_UNSAT ? "UNSAT  (expected only for N = 2 or 3)" : "unknown");
    if (r == LCG_SAT) {
        printf("\n");
        for (int i = 0; i < N; i++) {
            int c = lcg_value(ctx, col[i]);
            printf("    ");
            for (int j = 0; j < N; j++) putchar(j == c ? 'Q' : '.');
            putchar('\n');
        }
        printf("\n");
    }
    printf("  decisions      = %ld\n", lcg_decisions   (ctx));
    printf("  conflicts      = %ld\n", lcg_conflicts   (ctx));
    printf("  propagations   = %ld\n", lcg_propagations(ctx));
    printf("  explanations   = %ld\n", lcg_explanations(ctx));

    free(col); free(d1); free(d2);
    lcg_free(ctx);
    return r == LCG_SAT ? 0 : ((N == 2 || N == 3) ? 0 : 1);
}
