# MaxSAT

A small, self-contained partial MaxSAT solver in C99, built on top of
the SAT engine from the SMT/LCG codebase. All three phases delivered;
the consolidated write-up is Chapter 6 of *Practical Solvers*.

## Phase status

| Phase | Scope                                                       | Status |
|------:|-------------------------------------------------------------|--------|
| 1     | API, model-improving search, sequential-counter cardinality | DONE   |
| 2     | Core-guided MaxSAT (Fu-Malik), deletion-based core extraction | DONE |
| 3     | Weighted soft clauses via replication, DWTA worked example  | DONE   |

The library is feature-complete for the tutorial. The two original
standalone books are preserved in `../books/background/`:
*MaxSAT, Phases 1-3* (`maxsat-book.{tex,pdf}`, implementation) and
*Solving problems with MaxSAT* (`maxsat-user-guide.{md,pdf}`).

## Build

```sh
./build.zsh        # GNU/BSD bash is fine despite the name
```

Sanity: 23 / 23.

## Architecture

A *partial* MaxSAT problem has two kinds of clauses: hard (must be
satisfied) and soft (try to satisfy). The objective is to minimize the
number of unsatisfied soft clauses.

Two algorithms are implemented:

**Linear / model-improving (Phase 1).** Each iteration, a fresh SAT
engine is built with all hard clauses, all soft clauses relaxed with
fresh blocking variables, and a cardinality constraint on the blockers
forcing strict improvement over the current best cost. On UNSAT the
previous model is optimal.

**Core-guided / Fu-Malik (Phase 2, default).** Each iteration, a SAT
engine is built with all hard clauses, all softs extended with chains
of selectors, and unit clauses asserting that every soft must hold. On
UNSAT a subset of softs jointly infeasible (an "unsat core") is
extracted, fresh selectors are appended to each soft in the core, and
an at-most-one constraint over the *old* selectors is added. Each core
contributes 1 to the optimum.

Core extraction in Phase 2 is **deletion-based**: re-solve while
removing each assumption in turn, checking whether it was necessary
for UNSAT. This costs O(n_softs) SAT calls per core. A production
solver would use the SAT engine's native assumption mechanism to
extract the core from the final conflict clause for free; that
requires extending `sat.c`, which we intentionally do not do for the
tutorial. The algorithmic structure --- and the resulting cost --- is
identical either way.

Select the algorithm with `maxsat_set_algorithm`:

```c
MaxSatCtx *m = maxsat_new();
maxsat_set_algorithm(m, MAXSAT_ALG_LINEAR);          /* Phase 1 */
maxsat_set_algorithm(m, MAXSAT_ALG_CORE_GUIDED);     /* Phase 2 (default) */
```

The `examples/ex2_core_vs_linear.c` example runs the same instance
through both algorithms for direct comparison.

## Files

```
src/sat.{h,c}                       SAT engine (reused, unchanged)
src/maxsat.{h,c}                    MaxSAT API + linear + core-guided + weights
sanity.c                            41 smoke tests
examples/ex1_overconstrained_wta.c  unweighted WTA
examples/ex2_core_vs_linear.c       algorithm comparison
examples/ex3_dwta_weighted.c        weighted DWTA worked example
build.zsh                           build + sanity + examples runner
```

## What works

```c
MaxSatCtx *m = maxsat_new();

int x = maxsat_new_var(m);
int y = maxsat_new_var(m);

/* Hard: x or y must be true. */
int cl[2] = { x, y };
maxsat_add_hard_clause(m, cl, 2);

/* Soft: prefer x = true. */
int unit_x = x;
maxsat_add_soft_clause(m, &unit_x, 1);
/* Soft: prefer y = false. */
int unit_ny = -y;
maxsat_add_soft_clause(m, &unit_ny, 1);

long cost = maxsat_solve(m);
/* cost = 0 (both soft clauses satisfied with x=1, y=0). */
maxsat_free(m);
```

The convenience helper `maxsat_add_at_most_one(m, lits, n)` posts a
pairwise at-most-one constraint over the literals as a hard constraint.

## Out of scope (deliberate)

- Native incremental SAT and proper assumption-based core extraction
  (would substantially change `sat.c`; preserved as-is across the series).
- Weight-splitting Fu-Malik (the library uses replication, which scales
  linearly in total weight).
- Advanced cardinality encodings (totalizers, sorters, BDDs) beyond
  Sinz's sequential counter.
- Stratified MaxSAT for problems with large weight gaps.
- Optimization-style usage with continuous objectives.

The implementation book's closing chapter sketches what each of these
would look like.
