# Lazy Clause Generation

A small CP-with-CDCL solver in C99, built across four phases. Phase 1
delivered: order-encoded integer variables, one explaining propagator
(linear `≤`), and the theory-hook plumbing that lets a propagator's
explanations become learned clauses in a CDCL search.

## Phase status

| Phase | Scope                                                       | Status |
|------:|-------------------------------------------------------------|--------|
| 1     | Reification + linear propagator + architecture              | DONE   |
| 2     | First-class propagator interface and explanation builder    | DONE   |
| 3     | Bounds-consistent `alldifferent` with Hall-set explanations | DONE   |
| 4     | `cumulative` / `no_overlap` + DWTA worked example           | DONE   |

The library is feature-complete for the tutorial. The implementation book
and the user guide live in `../books/background/lcg-book.{tex,pdf}` and
`../books/background/lcg-user-guide.{md,pdf}` respectively. The consolidated
write-up is Chapter 5 of *Practical Solvers*.

## Build

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

Or directly:

```sh
gcc -std=c99 -O2 -Wall -Wextra -Isrc -c src/sat.c -o build/sat.o
gcc -std=c99 -O2 -Wall -Wextra -Isrc -c src/lcg.c -o build/lcg.o
gcc -std=c99 -O2 -Wall -Wextra -Isrc sanity.c build/sat.o build/lcg.o -o build/sanity
./build/sanity
```

Sanity: 21 / 21.

## Architecture (Phase 1)

LCG is a *theory* attached to the SAT engine via the `TheoryHooks`
contract (same one EUF and LRA use in *Satisfiability Modulo Theories*).
The theory's universe is finite-domain integer variables. Each
variable's domain is reified into a chain of order-encoding Boolean
literals: `b[k] ≡ (x ≤ k)`, with monotonicity clauses `b[k] → b[k+1]`.

Propagators look at current bounds, derive new bounds for other
variables, and emit a SAT-shaped explanation clause for every
inference. Conflicts become SAT learnt clauses through the same
channel.

The SAT engine is created lazily inside `lcg_solve`, sized to exactly
the number of atoms LCG has allocated. This avoids the trap of
pre-allocating a generous budget — unused atoms still sit on the
VSIDS heap and force gratuitous decisions, badly inflating the
decision count.

## Files

```
src/sat.{h,c}              SAT engine (reused from SMT codebase,
                           with one Phase 3 addition: empty-theory-
                           conflict short-circuit)
src/lcg.{h,c}              public API + theory plumbing + linear_le
src/prop_alldiff.c         bounds-consistent alldifferent (Phase 3)
src/prop_cumulative.c      time-table cumulative + no_overlap (Phase 4)
sanity.c                   44 smoke tests
examples/                  one runnable example per phase + DWTA
build.zsh                  build + sanity + examples runner
```

## Companion documents

For the canonical write-up, see **Chapter 5 of *Practical Solvers***
(`../books/practical-solvers/practical-solvers.pdf`).

The earlier standalone materials are preserved in `../books/background/`:

  * `lcg-book.{tex,pdf}` --- the implementation book.
  * `lcg-user-guide.{md,pdf}` --- the user guide focused on modelling
    patterns and the worked DWTA example.

## What works

Built-in constraints:

```c
LcgCtx *ctx = lcg_new();
IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
IntVar y = lcg_new_int_var(ctx, 0, 9, "y");

/* Linear inequality. */
int    c[2] = { 1, 1 };
IntVar v[2] = { x, y };
lcg_post_linear_le(ctx, c, v, 2, 5);    /* x + y <= 5 */

/* Bounds-consistent alldifferent. */
IntVar all[2] = { x, y };
lcg_post_alldifferent(ctx, all, 2);     /* x != y */

/* Cumulative resource (scheduling). */
IntVar s[2] = { x, y };
int    du[2] = { 3, 2 };
int    de[2] = { 2, 1 };
lcg_post_cumulative(ctx, s, du, de, 2, /*capacity=*/3);

/* Unary resource / no_overlap (special case of cumulative). */
lcg_post_no_overlap(ctx, s, du, 2);

if (lcg_solve(ctx) == LCG_SAT) {
    int vx = lcg_value(ctx, x);
    int vy = lcg_value(ctx, y);
}
lcg_free(ctx);
```

Custom propagators via the Phase 2 API:

```c
static int my_prop(LcgCtx *ctx, void *data) {
    /* Examine lcg_lb(ctx, v) / lcg_ub(ctx, v).
       Build explanations with lcg_expl_clear/lo/hi.
       Emit derived bounds with lcg_emit_le / lcg_emit_ge / lcg_emit_conflict. */
}
LcgPropagator p = { .data = ..., .propagate = my_prop, .destroy = ... };
lcg_register_propagator(ctx, p);
```

## Examples

- `examples/ex1_linear.c`     -- linear feasibility (Phase 1)
- `examples/ex2_custom_prop.c` -- user-defined `not_equal` propagator (Phase 2)
- `examples/ex3_nqueens.c`     -- N-Queens via three `alldifferent`s (Phase 3)
- `examples/ex4_cumulative.c`  -- cumulative scheduling primer (Phase 4)
- `examples/ex5_dwta.c`        -- DWTA worked example: naval air-defense
                                  channel scheduling (Phase 4)

## Out of scope (deliberate)

- Optimisation (only feasibility / SAT-or-UNSAT).
- Domain-consistent (Régin-matching-based) alldifferent --- would need
  per-value SAT atoms beyond the order encoding.
- Edge-finding / energetic reasoning for cumulative --- only time-table
  propagation is implemented.
- CP-specific search heuristics (uses plain VSIDS over the order-encoded
  atoms).
- Incremental solve --- one shot per `LcgCtx`.
