pith:M62KI5LT
Understanding CDCL Solvers via Scalability Studies and Proofdoors
Proofdoors explain why CDCL solvers scale linearly on some bounded model checking instances but exponentially on others.
arxiv:2605.15506 v1 · 2026-05-15 · cs.LO
Add to your LaTeX paper
\usepackage{pith}
\pithnumber{M62KI5LT6OLREUKK32JO3AMU5B}
Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge
Record completeness
Claims
By contrast, the recently proposed proofdoor parameter explains this phenomenon well. In support of the proofdoor hypothesis, we make three key contributions. First, we empirically show that CDCL solvers do compute small proofdoors for linearly-scaling BMC instances. Second, we show that for exponentially-scaling instances, sampled proofdoors scale exponentially and are typically not incrementally absorbed.
The assumption that sampled interpolants between formula chunks accurately represent the solver's internal memoization of reasoning effort, as described in the abstract where each interpolant is said to represent memoization on chunks already analyzed. If this representational link does not hold for actual CDCL execution traces, the claimed explanation for linear versus exponential scaling would not follow from the measurements.
CDCL SAT solvers compute small proofdoors on linearly scaling BMC families but large non-absorbed ones on exponential families, as shown by empirical measurements on a 76k+ instance benchmark where prior parameters fail to discriminate regimes.
References
Formal links
Receipt and verification
| First computed | 2026-05-20T00:01:02.183222Z |
|---|---|
| Builder | pith-number-builder-2026-05-17-v1 |
| Signature | Pith Ed25519
(pith-v1-2026-05) · public key |
| Schema | pith-number/v1.0 |
Canonical hash
67b4a47573f39712514ade92ed8194e87404bccd3c4bcc975670d14af37b79f7
Aliases
· · · · ·Agent API
Verify this Pith Number yourself
curl -sH 'Accept: application/ld+json' https://pith.science/pith/M62KI5LT6OLREUKK32JO3AMU5B \
| jq -c '.canonical_record' \
| python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 67b4a47573f39712514ade92ed8194e87404bccd3c4bcc975670d14af37b79f7
Canonical record JSON
{
"metadata": {
"abstract_canon_sha256": "adb079217ef763fbbc609986e699f951b2d48e58904e6abcfef1bfa3ac820223",
"cross_cats_sorted": [],
"license": "http://creativecommons.org/licenses/by/4.0/",
"primary_cat": "cs.LO",
"submitted_at": "2026-05-15T00:56:53Z",
"title_canon_sha256": "d3a0ec244e355500621dfd723003ffd6817be875a5a46b64036c1393facd1d94"
},
"schema_version": "1.0",
"source": {
"id": "2605.15506",
"kind": "arxiv",
"version": 1
}
}