/*
 * ex1_overconstrained_wta.c -- Phase 1 demonstration.
 *
 * Six inbound threats, three available weapons. Each weapon has a
 * compatibility window with the threat set (it can only engage
 * threats inside its sensor envelope and within its kinematic
 * envelope). We want to engage as many threats as possible.
 *
 *
 *   SCENARIO
 *
 *   threats:    T0   T1   T2   T3   T4   T5
 *   ---------------------------------------
 *   w0:         X    X    X    .    .    .
 *   w1:         .    X    X    X    X    .
 *   w2:         .    .    X    X    X    X
 *
 *   X = weapon w_i is compatible with threat t_j.
 *
 *
 *   MODEL
 *
 *   x_{i,j}     boolean: weapon i engages threat j.
 *   hard:       for each weapon, at most one engagement at this time slot.
 *   hard:       for each threat, at most one weapon engages it.
 *   soft:       for each threat, at least one weapon engages it
 *               (cost 1 per unengaged threat; Phase 3 will weight by
 *               threat value).
 *
 *   With 3 weapons and 6 threats, the trivial upper bound is to engage
 *   3 threats. The MaxSAT solver finds an assignment that meets this
 *   bound; the cost is 6 - 3 = 3 (unengaged threats). The compatibility
 *   graph happens to allow many such assignments; the solver picks one.
 */
#include "maxsat.h"

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

int main(void) {
    int n_w = 3, n_t = 6;
    int compat[3][6] = {
        { 1, 1, 1, 0, 0, 0 },
        { 0, 1, 1, 1, 1, 0 },
        { 0, 0, 1, 1, 1, 1 },
    };

    MaxSatCtx *m = maxsat_new();

    /* Allocate x[w][t] for compatible pairs only. */
    int x[3][6];
    for (int w = 0; w < n_w; w++)
        for (int t = 0; t < n_t; t++)
            x[w][t] = compat[w][t] ? maxsat_new_var(m) : -1;

    /* Hard: at-most-one engagement per weapon. */
    for (int w = 0; w < n_w; w++) {
        int row[6], n = 0;
        for (int t = 0; t < n_t; t++) if (x[w][t] > 0) row[n++] = x[w][t];
        maxsat_add_at_most_one(m, row, n);
    }
    /* Hard: at-most-one weapon per threat. */
    for (int t = 0; t < n_t; t++) {
        int col[3], n = 0;
        for (int w = 0; w < n_w; w++) if (x[w][t] > 0) col[n++] = x[w][t];
        if (n > 0) maxsat_add_at_most_one(m, col, n);
    }
    /* Soft: each threat is engaged. */
    for (int t = 0; t < n_t; t++) {
        int col[3], n = 0;
        for (int w = 0; w < n_w; w++) if (x[w][t] > 0) col[n++] = x[w][t];
        if (n > 0) maxsat_add_soft_clause(m, col, n);
    }

    long cost = maxsat_solve(m);

    printf("=== Phase 1: over-constrained WTA ===\n\n");
    printf("  compatibility matrix:\n");
    printf("       T0 T1 T2 T3 T4 T5\n");
    for (int w = 0; w < n_w; w++) {
        printf("    w%d  ", w);
        for (int t = 0; t < n_t; t++) printf(" %c ", compat[w][t] ? 'X' : '.');
        putchar('\n');
    }

    if (cost == MAXSAT_HARD_UNSAT) {
        printf("\n  status         = HARD UNSAT\n");
    } else {
        printf("\n  status         = SAT  (optimal)\n");
        printf("  unengaged       = %ld threats\n", cost);
        printf("  engaged         = %ld threats\n", (long)n_t - cost);
        printf("\n  assignment:\n");
        printf("       T0 T1 T2 T3 T4 T5\n");
        for (int w = 0; w < n_w; w++) {
            printf("    w%d  ", w);
            for (int t = 0; t < n_t; t++) {
                if (x[w][t] > 0 && maxsat_value(m, x[w][t]))     printf(" * ");
                else if (compat[w][t])                            printf(" . ");
                else                                              printf("   ");
            }
            putchar('\n');
        }
        printf("\n    threats engaged: ");
        for (int t = 0; t < n_t; t++) {
            int hit = 0;
            for (int w = 0; w < n_w; w++)
                if (x[w][t] > 0 && maxsat_value(m, x[w][t])) hit = 1;
            if (hit) printf("T%d ", t);
        }
        printf("\n    threats unengaged: ");
        for (int t = 0; t < n_t; t++) {
            int hit = 0;
            for (int w = 0; w < n_w; w++)
                if (x[w][t] > 0 && maxsat_value(m, x[w][t])) hit = 1;
            if (!hit) printf("T%d ", t);
        }
        printf("\n");
    }

    printf("\n  iterations     = %ld\n", maxsat_iterations(m));
    printf("  SAT decisions  = %ld\n",   maxsat_total_decisions(m));

    maxsat_free(m);
    return (cost == MAXSAT_HARD_UNSAT) ? 1 : 0;
}
