/*
 * ex3_dwta_weighted.c -- Phase 3: weighted DWTA over a saturated
 *                        threat picture.
 *
 *
 *   SCENARIO
 *
 *   A naval combatant has three fire-control channels and is tracking
 *   six inbound threats. The threat picture is over-saturated: not
 *   every threat can be engaged with the channels available. Each
 *   threat has a value (expected damage if it leaks through), and we
 *   want to minimize the total expected damage from unengaged threats.
 *
 *   Each weapon has a compatibility set --- threats it can prosecute
 *   given its sensor pointing, kinematic envelope, and engagement
 *   geometry. The same threats LCG handled in its DWTA example, plus
 *   a couple more to oversaturate the defence:
 *
 *     threat   value  | compatible weapons
 *     ---------------+---------------------
 *     T0  cruise-msl   10  | w0
 *     T1  drone-A       5  | w0, w1
 *     T2  cruise-msl    8  | w0, w1, w2
 *     T3  anti-ship     3  | w1, w2
 *     T4  drone-B       7  | w1, w2
 *     T5  drone-C       2  | w2
 *
 *
 *   MODEL
 *
 *   x_{w,t}   boolean: weapon w engages threat t.
 *   hard:     at-most-one engagement per weapon (capacity 1).
 *   hard:     at-most-one weapon per threat (no over-engagement).
 *   soft:     for each threat t, "engage t" (disjunction over compatible
 *             weapons) with weight = threat value.
 *
 *   Unengaging threat t costs (threat value). The solver minimizes
 *   total expected leakage.
 *
 *
 *   OPTIMUM
 *
 *   With 3 weapons we engage at most 3 threats. The best choice is the
 *   highest-value subset of 3 threats achievable under compatibility:
 *
 *     w0 -> T0 (value 10)
 *     w1 -> T4 (value  7)    [or T2; tie-broken by the solver]
 *     w2 -> T2 (value  8)
 *
 *   Engaged total = 10 + 7 + 8 = 25.
 *   Unengaged: T1 (5) + T3 (3) + T5 (2) = 10. So the optimum cost is 10.
 *
 *
 *   COMPARISON WITH PHASE 1
 *
 *   Phase 1's unweighted DWTA example treated every threat as equally
 *   important, so the solver minimized the number of unengaged
 *   threats and ended up leaking T0 (value 10) and T1 (value 5) while
 *   engaging T5 (value 2) --- a tactically disastrous schedule. The
 *   weighted formulation gets it right: T0 and T2 are now engaged
 *   ahead of T5 and T3.
 */
#include "maxsat.h"

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

int main(void) {
    int n_w = 3, n_t = 6;
    const char *id  [6] = { "T0", "T1", "T2", "T3", "T4", "T5" };
    const char *kind[6] = { "cruise-msl", "drone-A", "cruise-msl",
                            "anti-ship",  "drone-B", "drone-C"   };
    long value[6] = { 10, 5, 8, 3, 7, 2 };
    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();

    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 > 1) maxsat_add_at_most_one(m, col, n);
    }
    /* Soft (weighted by threat value): 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_weighted(m, col, n, value[t]);
    }

    long leakage = maxsat_solve(m);

    printf("=== Phase 3: weighted DWTA (saturated defence) ===\n\n");
    printf("  threat picture:\n");
    printf("     id   kind          value   w0 w1 w2\n");
    for (int t = 0; t < n_t; t++) {
        printf("     %s   %-12s    %3ld    ", id[t], kind[t], value[t]);
        for (int w = 0; w < n_w; w++) printf(" %c ", compat[w][t] ? 'X' : '.');
        printf("\n");
    }

    if (leakage == MAXSAT_HARD_UNSAT) {
        printf("\n  status         = HARD UNSAT\n");
    } else {
        long engaged_value = 0;
        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) engaged_value += value[t];
        }
        long total_value = 0;
        for (int t = 0; t < n_t; t++) total_value += value[t];

        printf("\n  status         = optimal\n");
        printf("  total value    = %ld   (sum of all threat values)\n", total_value);
        printf("  engaged value  = %ld   (saved by engagement)\n",       engaged_value);
        printf("  leakage        = %ld   (cost / damage from unengaged)\n", leakage);
        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("   ");
            }
            printf("\n");
        }

        printf("\n    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("%s(%ld) ", id[t], value[t]);
        }
        printf("\n    leaked:     ");
        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("%s(%ld) ", id[t], value[t]);
        }
        printf("\n");
    }

    printf("\n  algorithm      = %s\n",
        maxsat_get_algorithm(m) == MAXSAT_ALG_CORE_GUIDED ?
        "core-guided (Fu-Malik)" : "linear (model-improving)");
    printf("  iterations     = %ld\n", maxsat_iterations(m));
    printf("  cores found    = %ld\n", maxsat_cores_found(m));
    printf("  SAT decisions  = %ld\n", maxsat_total_decisions(m));

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