Research map / Learning theory and algorithms / Combinatorial and search optimization

Proof Simulation via Round-based Strategy Extraction for QBF

AAAI 2025 · Learning theory and algorithms › Combinatorial and search optimization · approach: SAT and model counting solvers · 0 citations (OpenAlex)

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.

The paper formalises round-based strategy extraction for QBF refutations as extension-variable circuitry and uses it to show that eFrege+∀red p-simulates LD-Q(Drrs)-Resolution.

Problem

QBF proof complexity lacks a proof-system simulation showing that QCDCL-related systems (LD-Q(Drrs)-Resolution, the proof system behind Qute) can be efficiently simulated by Extended Frege plus universal reduction, which would enable certification of QCDCL solvers.

Approach

Formalises round-based strategy extraction (restrict the proof by outer-block assignments and prune) as polynomial-size extension variables and connectivity relations, then uses the soundness of the extracted strategy inside eFrege+∀red to derive a QBF refutation, giving a p-simulation (quartic in proof size).

Key results

• Proves eFrege+∀red p-simulates LD-Q(Drrs)-Resolution (Theorem 1), resolving an open problem in QBF proof complexity.
• The p-simulation is quartic in proof size, with strategy-soundness lemma of O(s(π)^4) size.
• Shows local strategies yield a Skolemisation-based SAT-oracle certification alternative with O(k·s(π)) added clauses.

Limitations

• The p-simulation is quartic, and the authors note the exponent may be reducible.
• The SAT-oracle certification path is not polynomial-time checkable and its clauses do not pass DRAT-trim RAT checks.

Experimental setup

Baselines: local strategy extraction (Chew and Slivovsky 2022)

Builds on: Extended Frege + ∀red LD-Q(Drrs)-Resolution local strategy extraction (Chew and Slivovsky 2022) QRAT Q-Res

Closest papers by meaning

• Computationally Hard Problems Are Hard for QBF Proof Systems Too (AAAI 2025 · similarity 0.87)
• Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs (AAAI 2024 · similarity 0.87)
• 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes (NeurIPS 2025 · similarity 0.83)
• Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.82)
• MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.82)
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.82)