CLI reference

just_count [OPTIONS] file

Positional argument

file (required): DIMACS CNF input file. Standard p cnf <vars> <clauses> header, plus an optional c p show <v1> <v2> ... 0 comment line declaring the variables to project onto for projected model counting. If that line is absent, the count is over all variables.

Options

-p, --progress N (default: 1000): Print a c models: <count> time: <t>s progress line every N models found. 0 disables progress reporting.
-o, --output FILE: Write every satisfying assignment found to FILE, one DIMACS v-line per model, restricted to the projected variables if projection is in use. Pass - to write to stdout instead of a file.
-t, --timeout SECONDS (default: 0, disabled): Stop counting after roughly SECONDS seconds and report the partial count found so far. This is a soft limit: it’s only checked once per model, i.e. once per solve() call between adding blocking clauses — not while a single solve() call is in progress. A pathological instance where one solve() call itself takes minutes can still run well past the requested timeout.
-q, --quiet: Suppress the c just_count version ... / c CaDiCaL version ... banner that’s otherwise printed at startup.
--cadical-version VERSION (default: 3.0.0): Selects which bundled CaDiCaL build to solve with. See {doc}architecture for how multiple versions coexist in one binary. Run just_count --help to see which versions are available in your build (typically 1.9.5, 2.2.1, 3.0.0).
--cadical-option NAME=VALUE (repeatable): Sets a CaDiCaL internal option via CaDiCaL::Solver::set(NAME, VALUE), applied once right after the solver is constructed, before any clauses are added. Repeat the flag to set several options. Available option names and their valid ranges depend on the selected CaDiCaL version — see that version’s src/options.hpp, or the worked example in {doc}investigation for ilb. An unknown or currently-unsettable option name is a fatal error (CaDiCaL <version>: cannot set option '<name>').
By default, ilb=2 (incremental lazy backtracking) is forced on and all inprocessing — sweep, congruence, backbone, condition, elim, vivify, probe, subsume, transred, walk — is forced off, tuned for this tool’s repeated-solve()-per-model workload (see {doc}investigation). Use --cadical-option to override any of these, e.g. --cadical-option sweep=1 to turn SAT sweeping back on.
--version: Print just_count’s own version and, for every bundled CaDiCaL plugin found, its exact reported version string, then exit. Does not require the file argument.
-h, --help: Print the full CLI11-generated usage summary and exit.

Output

c just_count version <git describe>
c CaDiCaL version <version>
c Variables: <N>
c Clauses: <N>
c Projected variables: <N>        (only if projection is in use)
c models: <count> time: <t>s      (progress lines, if enabled)
c timeout after <t>s, models found: <count>   (only if --timeout was hit)
s mc <count>

s mc <count> follows the model-counting-competition output convention (s line, mc = model count). If the run stopped early — either because --timeout was reached, or CaDiCaL returned an unknown result — <count> is a partial count, and a c timeout after ... or s UNKNOWN line precedes it explaining why.

Examples

# Exact count, default (fastest-known) CaDiCaL version
./just_count formula.cnf

# Count with a 5-minute soft timeout, using a specific CaDiCaL version
./just_count --cadical-version 1.9.5 --timeout 300 formula.cnf

# Write every model to stdout, no progress spam
./just_count -p 0 -o - formula.cnf

# Tune CaDiCaL options (see the investigation for why this helps)
./just_count --cadical-version 2.2.1 --cadical-option ilb=2 formula.cnf