Research map / Learning theory and algorithms / Combinatorial and search optimization
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Shows that for QBF, QCDCL runs can be exponentially longer than the QBF resolution proofs extracted from them, via a master theorem combining gauge lower bounds on trail size with quadratic extracted-proof upper bounds across MLD, MQ and MQU models.
Problem
Whether QCDCL on QBFs can be exponentially slower than the size of proofs extracted from its own runs (the extracted-proof question Q2), whereas for SAT CDCL trail size and extracted resolution proof size differ only polynomially.
Approach
A master theorem combining an exponential trail-size lower bound (gauge technique applied to fully reduced primitive Q-Res refutations) with a polynomial extracted-proof upper bound, instantiated with equality-based QBF families (Eqn/TwinModEqn reversions and simplicity formulas) for three QCDCL models.
Key results
- For MLD (LD-Q-Res QCDCL), the composed formula ERTMEn has trail size 2^Omega(n) for any refutation but an MLD refutation with extracted proof size O(n^2) exists (Corollary 5.9).
- For MQ (Q-Res) on SREn, trail size is 2^Omega(n) while an extracted refutation of size O(n^2) exists (Corollary 5.17).
- For MQU (QU-Res), the same separation holds on SREn: trail size 2^Omega(n) versus extracted size O(n^2) (Corollary 5.19).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use MLD QCDCL on ERTMEn | MLD · ERTMEn | proof size: trail-size 2^Ω(n); extr-size O(n2) | Mixed |
| Use MQ QCDCL on SREn | MQ · SREn | proof size: trail-size 2^Ω(n); extr-size O(n2) | Mixed |
| Use MQU QCDCL on SREn | MQU · SREn | proof size: trail-size 2^Ω(n); extr-size O(n2) | Mixed |
Surprising findings
- Even for false QBFs, cube learning from satisfying assignments can create an exponential bottleneck, since learned cubes do not appear in the extracted proof.
- Unlike SAT, where trail size and extracted proof size differ by only a linear factor, QCDCL on QBF shows an exponential gap between trail size and extracted proof size.
Limitations
- Results are purely theoretical with no experiments on practical QBF solvers.
- Separations hold only when decisions follow the quantifier prefix (LEV-ORD); arbitrary decisions remove the gap.
- Analysis is restricted to plain QCDCL without advanced techniques such as dependency learning.
Experimental setup
Metrics: trail size extracted proof size proof size lower and upper bounds
Baselines: LD-Q-Res QCDCL (MLD) Q-Res QCDCL (MQ) QU-Res QCDCL (MQU)
Builds on: gauge lower bound technique (Böhm and Beyersdorff 2021) twin formulas and reversion (Böhm, Peitl, and Beyersdorff 2022) QCDCL as proof systems (Beyersdorff and Böhm 2023) equality formulas (Beyersdorff, Blinkhorn, and Hinde 2019)
Closest papers by meaning
- Proof Simulation via Round-based Strategy Extraction for QBF (AAAI 2025 · similarity 0.87)
- Hardness of Random Reordered Encodings of Parity for Resolution and CDCL (AAAI 2024 · similarity 0.86)
- Computationally Hard Problems Are Hard for QBF Proof Systems Too (AAAI 2025 · similarity 0.85)
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.83)
- 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes (NeurIPS 2025 · similarity 0.83)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.