/*
 * maxsat.h -- A partial MaxSAT solver built on top of the SAT engine.
 *
 * Phase 1: unweighted partial MaxSAT via model-improving (linear search).
 *          Each call to maxsat_solve runs a sequence of SAT queries,
 *          each one tighter than the previous, until UNSAT proves
 *          the previously-found cost is optimal.
 *
 * Phase 2 (planned): core-guided MaxSAT (Fu-Malik / OLL).
 * Phase 3 (planned): weighted soft clauses, stratification, DWTA example.
 *
 *
 *   API CONVENTIONS
 *
 * Variables are positive integers starting at 1, allocated through
 * maxsat_new_var. Literals are signed integers: +v means "v is true",
 * -v means "v is false". This matches the underlying SAT engine.
 *
 * Hard clauses must be satisfied in any model the solver returns.
 * Soft clauses each contribute cost 1 if unsatisfied; the solver
 * minimizes the total cost.
 *
 * After maxsat_solve, query each variable's value with maxsat_value.
 */
#ifndef MAXSAT_H
#define MAXSAT_H

#ifdef __cplusplus
extern "C" {
#endif

typedef struct MaxSatCtx MaxSatCtx;

/* Returned by maxsat_solve when the hard clauses alone are infeasible. */
#define MAXSAT_HARD_UNSAT  (-1)

/* Available algorithms. Set via maxsat_set_algorithm before solving. */
typedef enum {
    MAXSAT_ALG_LINEAR      = 0,    /* Phase 1: model-improving search */
    MAXSAT_ALG_CORE_GUIDED = 1,    /* Phase 2: Fu-Malik core-guided   */
} MaxSatAlgorithm;

MaxSatCtx *maxsat_new(void);
void       maxsat_free(MaxSatCtx *m);

/* Select the search algorithm. Default is MAXSAT_ALG_CORE_GUIDED. */
void             maxsat_set_algorithm(MaxSatCtx *m, MaxSatAlgorithm alg);
MaxSatAlgorithm  maxsat_get_algorithm(const MaxSatCtx *m);

/* Allocate a fresh SAT variable; returns its positive id. */
int maxsat_new_var(MaxSatCtx *m);

/* Add a hard clause. The literal array is copied. */
void maxsat_add_hard_clause(MaxSatCtx *m, const int *lits, int n);

/* Add a soft clause. Unsatisfied soft clauses each contribute cost 1.
 * Equivalent to maxsat_add_soft_clause_weighted with weight 1. */
void maxsat_add_soft_clause(MaxSatCtx *m, const int *lits, int n);

/* Add a soft clause with integer weight. Unsatisfied contributes
 * `weight` to the cost. A weight of 0 makes the clause a no-op;
 * negative weights are invalid and silently dropped.
 *
 * Phase 3 implements weights via *replication*: a clause with weight w
 * is internally stored as w identical unit-weight clauses, so the
 * memory cost is proportional to total weight. This makes the
 * weighted semantics transparent (weight = count in the cardinality
 * profile) and requires no changes to the underlying algorithms.
 * For tutorial-scale weights (up to a few hundred) it is fine; a
 * production solver uses weight-splitting Fu-Malik or pseudo-Boolean
 * cardinality encodings to handle large weights efficiently. */
void maxsat_add_soft_clause_weighted(MaxSatCtx *m, const int *lits, int n,
                                     long weight);

/* Convenience: assert that at most one of the literals is true.
 * Phase 1 uses pairwise encoding (O(n^2) binary clauses), which is
 * fine for small n. */
void maxsat_add_at_most_one(MaxSatCtx *m, const int *lits, int n);

/* Solve to optimality. Returns:
 *     MAXSAT_HARD_UNSAT   if the hard clauses alone are infeasible.
 *     >= 0                the minimum number of unsatisfied soft clauses.
 *
 * After a non-negative return, the model is accessible via maxsat_value.
 * The function may only be called once per context. */
long maxsat_solve(MaxSatCtx *m);

/* After a successful solve, return the truth value of `var` in the
 * optimal model (0 or 1). Returns 0 for unknown variables. */
int maxsat_value(const MaxSatCtx *m, int var);

/* Statistics. */
long maxsat_iterations     (const MaxSatCtx *m);
long maxsat_total_decisions(const MaxSatCtx *m);
long maxsat_cores_found    (const MaxSatCtx *m);  /* core-guided only */

#ifdef __cplusplus
}
#endif

#endif
