# CLI reference

```text
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

```text
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

```bash
# 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
```