# Investigation: why is CaDiCaL 2.2.1/3.0.0 so much slower than 1.9.5?

This page is a worked example of using `--cadical-version` and
`--cadical-option` (see {doc}`cli-reference`) to diagnose and fix a real
performance regression, run against a formula with 1572 variables, 169124
clauses, and 288 projected variables (`rel_cp.cnf`, not included in this
repository).

## Initial benchmark: 5-minute soft timeout per version

```bash
./just_count --cadical-version 1.9.5 --timeout 300 rel_cp.cnf
./just_count --cadical-version 2.2.1 --timeout 300 rel_cp.cnf
./just_count --cadical-version 3.0.0 --timeout 300 rel_cp.cnf
```

| CaDiCaL | Result | Time | Models/sec |
|---|---|---|---|
| **1.9.5** | **Completed exhaustively: `s mc 348535`** | 24.4s | ~14,300/s |
| 2.2.1 | Timed out, partial count 145293 | 303.5s | ~479/s |
| 3.0.0 | Timed out, partial count 145293 | 303.8s | ~478/s |

1.9.5 finished the *entire* count in 24 seconds. 2.2.1 and 3.0.0 both ran
out of a 5-minute budget at roughly **1/30th** the throughput — and
notably found the *exact same* partial count (145293) at nearly the same
wall-clock time, which is a strong hint that whatever changed, changed
between 1.9.5 and 2.2.1, and 3.0.0 didn't change it further.

## Bisecting with a short timeout

A 5-minute-per-run feedback loop is too slow for trial and error, so the
rest of the investigation used a 2-second soft timeout — short enough for
fast iteration, long enough to give a stable throughput signal (dozens to
tens of thousands of models, depending on configuration).

```bash
./just_count --cadical-version 1.9.5 --timeout 2 -p 0 -q rel_cp.cnf
# c timeout after 2s, models found: 34034      (~17,000/s)

./just_count --cadical-version 2.2.1 --timeout 2 -p 0 -q rel_cp.cnf
# c timeout after 2.00184s, models found: 209   (~104/s)
```

### First guess: newer preprocessing techniques — wrong

CaDiCaL 2.2.1 added several substantial preprocessing/inprocessing
techniques not present in 1.9.5, all enabled by default: `sweep` (SAT
sweeping), `congruence` (congruence closure / gate extraction),
`backbone` (backbone literal computation), plus a `condition` option
family. Any of these running on every incremental `solve()` call would
plausibly explain a large per-call slowdown, so the natural first
hypothesis was "one of these is expensive and shouldn't run every model."

Testing each individually via `--cadical-option`:

```bash
for opt in sweep=0 congruence=0 backbone=0 condition=0 elim=0 vivify=0 \
           probe=0 subsume=0 transred=0 walk=0; do
  ./just_count --cadical-version 2.2.1 --cadical-option "$opt" \
    --timeout 2 -p 0 -q rel_cp.cnf
done
```

Every single one landed at **200–210 models** — indistinguishable from
the baseline. Disabling *all of them at once* didn't help either (205
models). So none of the "obviously expensive-sounding" new preprocessing
techniques were the cause. A longer run (10s, with progress every 500
models) with everything disabled showed a flat ~100–110 models/sec
throughout, not a one-time startup cost that would amortize away — this
was a genuine **per-call** regression, not a one-off.

### Second guess: `ilb` — correct

`just_count`'s workload is unusual for a general-purpose SAT benchmark:
it calls `solve()` **repeatedly**, adding exactly one new (blocking)
clause between calls, and expects each subsequent call to be *cheap*
because almost nothing changed since the last one. That's precisely the
scenario CaDiCaL's **Incremental Lazy Backtracking (`ilb`)** option
exists for — it avoids backtracking all the way to decision level 0 (and
re-deriving most of the search) on every incremental `solve()` call.

Comparing the option's definition between versions
(`src/options.hpp`):

```text
# CaDiCaL 1.9.5 — boolean, defaults ON
OPTION( ilb,  1,  0,  1, ..., "ILB (incremental lazy backtrack)")

# CaDiCaL 2.2.1 — tri-state, defaults OFF
OPTION( ilb,  0,  0,  2, ..., "ILB (incremental lazy backtrack)
                                (0: no, 1: assumptions only, 2: everything)")
```

`ilb` silently changed from **on by default** to **off by default**, and
gained a middle "assumptions only" state that doesn't help `just_count`
at all — it doesn't use assumption literals, only clause addition. The
option `just_count` needs is `ilb=2` ("everything"):

```bash
./just_count --cadical-version 2.2.1 --cadical-option ilb=1 \
  --timeout 2 -p 0 -q rel_cp.cnf
# 219 models — no better; ilb=1 only reuses the trail for assumptions

./just_count --cadical-version 2.2.1 --cadical-option ilb=2 \
  --timeout 2 -p 0 -q rel_cp.cnf
# 13167 models  (~6,000/s — about 58x faster than the default)
```

Confirmed on 3.0.0 too:

```bash
./just_count --cadical-version 3.0.0 --cadical-option ilb=2 \
  --timeout 2 -p 0 -q rel_cp.cnf
# 13167 models — same fix, same effect
```

### Stacking `ilb=2` with the earlier (individually useless) options

The preprocessing techniques that didn't help *on their own* turned out
to still be worth disabling once `ilb=2` is set — with fast incremental
re-solves doing most of the work, their overhead becomes visible again:

```bash
./just_count --cadical-version 2.2.1 --cadical-option ilb=2 \
  --cadical-option sweep=0 --cadical-option congruence=0 \
  --cadical-option backbone=0 --cadical-option condition=0 \
  --cadical-option elim=0 --cadical-option vivify=0 \
  --cadical-option probe=0 --cadical-option subsume=0 \
  --cadical-option transred=0 --cadical-option walk=0 \
  --timeout 2 -p 0 -q rel_cp.cnf
# 49807 models  (~24,900/s)
```

## Final validation: full run to completion

| Configuration | Time to `s mc 348535` |
|---|---|
| 1.9.5, defaults | ~27–28s |
| 2.2.1, `ilb=2` + the ten options above disabled | **~14s** |

Both report the identical exact count (348535), confirming the tuning
changes performance, not correctness — and the tuned 2.2.1 run is
**about 2x faster than 1.9.5's untouched defaults** on this formula.

## What actually shipped

The full tuning — `ilb=2` plus all ten inprocessing techniques disabled
(`sweep`, `congruence`, `backbone`, `condition`, `elim`, `vivify`,
`probe`, `subsume`, `transred`, `walk`) — is unconditionally applied in
`jc_cadical_new()` for every bundled version (see {doc}`architecture`).
This was initially left partial (`ilb=2` only, on the theory that
silently changing what CaDiCaL preprocesses by default was too broad a
change), but re-measuring with only `ilb=2` shipped still showed 1.9.5
about 4x ahead of 2.2.1/3.0.0 (148585 vs 35751 models in 10s) — the
newer versions' extra preprocessing, left at its own defaults, was still
costing more than it recovered. Applying the full profile everywhere
closes that gap and then some:

| CaDiCaL (full tuning baked in) | Models found in 10s | Full run to `s mc 348535` |
|---|---|---|
| 1.9.5 | 225915 | ~16.0s |
| 2.2.1 | 245161 | ~14.1s |
| **3.0.0** | **251870** | **~14.1s** |

1.9.5 improved too (148585 → 225915 in 10s) since it already has
`elim`/`vivify`/`probe`/`subsume`/`transred`/`walk` even though it
predates `sweep`/`congruence`/`backbone`/`condition` — but 2.2.1 and
3.0.0 now tie for fastest, both modestly ahead of 1.9.5. All three report
the identical exact count, confirming this doesn't change correctness.

**`CADICAL_DEFAULT_VERSION` is `3.0.0`** — it ties 2.2.1 for fastest and
is the actively maintained release, breaking the tie. `--cadical-option`
still overrides any of the baked-in options per run (e.g.
`--cadical-option sweep=1` to turn SAT sweeping back on).

## Takeaways

- When comparing solver versions for an **incremental** workload
  (repeated `solve()` calls with small deltas), check options that
  specifically affect incremental re-solving before suspecting
  general-purpose preprocessing — `ilb` had far more impact here than
  any of the newer inprocessing techniques, individually or combined.
- A short `--timeout` (seconds, not minutes) is enough to get a stable
  throughput signal for this kind of bisection, and made the whole
  investigation above take a couple of minutes of wall-clock time rather
  than tens of minutes.
- `--cadical-option` generalizes beyond this one finding — it's a direct
  pass-through to `CaDiCaL::Solver::set()`, so any option documented in a
  given version's `src/options.hpp` can be tuned from the command line
  without a rebuild.