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

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

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

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):

# 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”):

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

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

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