just_count

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 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.