/*
 * ex2_core_vs_linear.c -- Phase 2 demonstration.
 *
 * The same MaxSAT instance is solved twice: once with Phase 1's
 * model-improving (linear) algorithm, once with Phase 2's core-guided
 * (Fu-Malik) algorithm. We print the cost (which must agree) and the
 * SAT decision count, so the reader can see how the algorithmic
 * choice affects the search effort.
 *
 *
 *   THE INSTANCE
 *
 *   Imagine a tasking problem with K capacity slots and N tasks, where
 *   every task wants to be scheduled. The hard constraint is the
 *   capacity: at most K tasks can be active at once. Each task is a
 *   soft clause: "I want to be scheduled" (i.e., (x_i)). Setting more
 *   than K of the x_i true is forbidden, so at least N - K soft
 *   clauses must be unsatisfied. Optimal cost = N - K.
 *
 *   This is a textbook over-constrained instance --- and a textbook
 *   stress test for cardinality-based MaxSAT, because:
 *
 *     * Phase 1 (linear search) must repeatedly solve under
 *       sum(b_i) <= cost - 1 cardinality constraints, with cost
 *       descending from N down to N - K. That's K iterations of
 *       solving with O(N * cost) auxiliary clauses each.
 *
 *     * Phase 2 (core-guided) discovers N - K cores, each of size
 *       K + 1. Each core relaxes with a small at-most-one over K + 1
 *       old selectors. Total auxiliary clauses: O((N - K) * K^2)
 *       binary clauses.
 *
 *   The two algorithms have different asymptotic behaviour; on
 *   tutorial-scale inputs the difference is observable but not
 *   dramatic. The intent is to show the *shape* of the difference,
 *   not to benchmark.
 */
#include "maxsat.h"

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

static long solve_with(MaxSatAlgorithm alg, int N, int K, long *cost_out) {
    MaxSatCtx *m = maxsat_new();
    maxsat_set_algorithm(m, alg);

    int *x = malloc((size_t)N * sizeof(int));
    for (int i = 0; i < N; i++) x[i] = maxsat_new_var(m);

    /* Hard: at most K of the x_i are true.
     * Implemented via Sinz's sequential counter directly here. */
    /* For simplicity, just use pairwise at-most-(K+1) by forbidding
     * every (K+1)-subset all true.  For our tutorial sizes (N ~ 7,
     * K ~ 3) this gives a few dozen clauses, fine. */
    /* Better: post a chain of at-most-1 constraints over rolling
     * windows? No, simpler: just one at-most-K constraint. We don't
     * have a public helper for at-most-K, so we'll use pairwise for
     * at-most-1 sub-cases and rely on the MaxSAT layer.
     *
     * Actually, the cleanest thing: encode at-most-K by hand with the
     * sequential-counter formulation that maxsat.c already uses
     * internally. But that's not exposed. So we just use pairwise
     * forbidding of every (K+1)-tuple --- O(C(N, K+1)) clauses,
     * which for N=7, K=3 is C(7,4) = 35 clauses. Fine. */
    /* Enumerate all (K+1)-subsets and forbid each. */
    int *subset = malloc((size_t)(K + 1) * sizeof(int));
    for (int i = 0; i <= K; i++) subset[i] = i;
    while (1) {
        int cl[16];
        for (int i = 0; i <= K; i++) cl[i] = -x[subset[i]];
        maxsat_add_hard_clause(m, cl, K + 1);

        int j = K;
        while (j >= 0 && subset[j] == N - (K + 1) + j) j--;
        if (j < 0) break;
        subset[j]++;
        for (int k = j + 1; k <= K; k++) subset[k] = subset[k - 1] + 1;
    }
    free(subset);

    /* Soft: each x_i = true. */
    for (int i = 0; i < N; i++) {
        int cl = x[i];
        maxsat_add_soft_clause(m, &cl, 1);
    }

    long cost = maxsat_solve(m);
    *cost_out = cost;
    long decisions = maxsat_total_decisions(m);

    free(x);
    maxsat_free(m);
    return decisions;
}

int main(void) {
    int N = 7, K = 3;

    long cost_linear, cost_core;
    long dec_linear = solve_with(MAXSAT_ALG_LINEAR,      N, K, &cost_linear);
    long dec_core   = solve_with(MAXSAT_ALG_CORE_GUIDED, N, K, &cost_core);

    printf("=== Phase 2: linear vs core-guided on at-most-%d-of-%d ===\n\n", K, N);
    printf("  optimum cost   = %ld   (expect %d)\n", cost_linear, N - K);
    printf("  both agree     = %s\n",  cost_linear == cost_core ? "yes" : "NO");
    printf("\n");
    printf("                       SAT decisions\n");
    printf("  linear              =      %6ld\n", dec_linear);
    printf("  core-guided         =      %6ld\n", dec_core);
    printf("\n");
    printf("  Both algorithms find the same optimum. On this small\n");
    printf("  instance the linear algorithm wins on raw SAT-call cost\n");
    printf("  because Phase 2's deletion-based core extraction does\n");
    printf("  O(soft) SAT calls per core. A production core-guided\n");
    printf("  solver uses native SAT assumptions to extract cores for\n");
    printf("  free, and beats linear search by orders of magnitude on\n");
    printf("  hard instances. The algorithmic structure shown here is\n");
    printf("  the same; only the SAT-engine support differs.\n");

    return cost_linear == cost_core ? 0 : 1;
}
