# just_count

`just_count` is a small, exact (and projected) **model counter** for
propositional CNF formulas in DIMACS format. It counts satisfying
assignments — either over all variables, or projected onto a chosen subset
of "sampling" variables — using a straightforward blocking-clause loop
built on top of the [CaDiCaL](https://github.com/arminbiere/cadical) SAT
solver:

1. Parse the DIMACS CNF file (`p cnf <vars> <clauses>`, plus an optional
   `c p show <vars> 0` line declaring the variables to project onto).
2. Repeatedly call `solve()`.
   - `UNSAT` → done, return the count.
   - `SAT` → record the model, add a *blocking clause* that rules out the
     current assignment (restricted to the projected variables), and
     solve again.

This document covers how to build it, its full CLI, why it can switch
between several CaDiCaL versions at runtime, and a worked investigation
into why one of those versions was ~150x slower than another on a real
formula — and how a single solver option closed that gap.

```{tableofcontents}
```