CDCL is a Collapse Chain: A Formal Equivalence Between Conflict-Driven Clause Learning and Irreversible Uncertainty Reduction
Fuente:
Zenodo
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Recurso digital |
| Lingua: | inglese |
| Pubblicazione: |
Zenodo
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866901773311016960 |
|---|---|
| author | Rao, Huiying |
| author_facet | Rao, Huiying |
| contents | <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">We prove that the Conflict-Driven Clause Learning (CDCL) algorithm is formally equivalent to a branching collapse chain: a collection of collapse chains that share information through learned clauses, with globally monotone non-decreasing information content despite local backtracking.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">The equivalence resolves the backtracking paradox: backtracking does not reverse collapse. It terminates the current chain and initiates a new one from a checkpoint, with the learned clause serving as the irreversible information transfer between chains. The global information content of CDCL is monotone non-decreasing (Information Monotonicity Theorem), consistent with the branching collapse chain definition.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Three consequences follow: (1) The Information Monotonicity Theorem — each k-literal learned clause contributes n−k bits of information, explaining why modern CDCL implementations prioritise short clauses; (2) The Gradient Impossibility Theorem — no differentiable collapse operator can improve upon CDCL for SAT near the phase transition, providing a principled explanation for the hard wall; (3) Empirical validation — 47 out of 100 variables exhibit intrinsic uncertainty across satisfying assignments at α=4.2, confirming that residual uncertainty after CDCL is structural, not epistemic.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Part of the NSD / MOEH research programme. Companion papers: "Collapse as a Unifying Language for NP-Hard Optimisation" (Zenodo: 10.5281/zenodo.19574013) and "A Landscape-Aware Classification Framework for NP-Hard Optimisation Problems" (under review at JAIR #22499).</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_19600733 |
| institution | Zenodo |
| language | eng |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | CDCL is a Collapse Chain: A Formal Equivalence Between Conflict-Driven Clause Learning and Irreversible Uncertainty Reduction Rao, Huiying CDCL SAT collapse chain unit propagation clause learning phase transition uncertainty reduction information monotonicity hard wall NP-hard <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">We prove that the Conflict-Driven Clause Learning (CDCL) algorithm is formally equivalent to a branching collapse chain: a collection of collapse chains that share information through learned clauses, with globally monotone non-decreasing information content despite local backtracking.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">The equivalence resolves the backtracking paradox: backtracking does not reverse collapse. It terminates the current chain and initiates a new one from a checkpoint, with the learned clause serving as the irreversible information transfer between chains. The global information content of CDCL is monotone non-decreasing (Information Monotonicity Theorem), consistent with the branching collapse chain definition.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Three consequences follow: (1) The Information Monotonicity Theorem — each k-literal learned clause contributes n−k bits of information, explaining why modern CDCL implementations prioritise short clauses; (2) The Gradient Impossibility Theorem — no differentiable collapse operator can improve upon CDCL for SAT near the phase transition, providing a principled explanation for the hard wall; (3) Empirical validation — 47 out of 100 variables exhibit intrinsic uncertainty across satisfying assignments at α=4.2, confirming that residual uncertainty after CDCL is structural, not epistemic.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Part of the NSD / MOEH research programme. Companion papers: "Collapse as a Unifying Language for NP-Hard Optimisation" (Zenodo: 10.5281/zenodo.19574013) and "A Landscape-Aware Classification Framework for NP-Hard Optimisation Problems" (under review at JAIR #22499).</p> |
| title | CDCL is a Collapse Chain: A Formal Equivalence Between Conflict-Driven Clause Learning and Irreversible Uncertainty Reduction |
| topic | CDCL SAT collapse chain unit propagation clause learning phase transition uncertainty reduction information monotonicity hard wall NP-hard |
| url | https://doi.org/10.5281/zenodo.19600733 |