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

Computationally Hard Problems Are Hard for QBF Proof Systems Too

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.

Transforms computationally hard problems from the polynomial hierarchy (Succinct k-Radius, k-Clique Colouring, ALL-EQUAL∃∀3SAT) into QBF families and proves unconditional exponential lower bounds for QU-Res and Q-Res via the cost technique.

Problem

Scarcity of natural, provably hard QBF formula families for analysing QBF proof systems (Q-Res, QU-Res) and testing solvers.

Approach

Encode PH-complete problems as QBFs and build families of "critical" structures that only just fail the property (many almost-k-centers, many 3-colour-selectable cliques, many non-monotonicity-enforceable assignments), then apply the semantic cost lower bound so that the QBFs need exponential-size QU-Res proofs unconditionally.

Key results

• Succinct k-Radius QBFs (SR_k) have cost at least n and require QU-Res proofs of size at least 2^n, with formulas of size O(log n).
• k-Clique Colouring formulas CC3(G_n) have cost at least 20·3^(n-1) and require exponential-size QU-Res proofs.
• ALL-EQUAL∃∀3SAT formulas AE(phi_n) have cost at least 2^n and require exponential-size QU-Res proofs, hence also Q-Res.

Limitations

• Specific problems require individually hand-crafted critical instances; the general method is not fully automated.
• Hardness results are theoretical lower bounds; no solver experiments are reported.
• Only three case-study problems are analysed.

Experimental setup

Metrics: proof size lower bound (exponential) cost of QBF countermodels

Baselines: KBKF formulas equality formulas parity formulas CR formulas

Builds on: cost lower bound technique (Beyersdorff, Blinkhorn, Hinde 2019) Q-Resolution QU-Resolution

Closest papers by meaning

• Using Decomposition-Parameters for QBF: Mind the Prefix! (AAAI 2016 · similarity 0.88)
• Proof Simulation via Round-based Strategy Extraction for QBF (AAAI 2025 · similarity 0.87)
• Breaking Symmetries in Quantified Graph Search: A Comparative Study (AAAI 2025 · similarity 0.87)
• Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.86)
• Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs (AAAI 2024 · similarity 0.85)
• Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.84)