Dynamic QBF dependencies in reduction and expansion

DOI10.1145/3355995MaRDI QIDQ4972172zbMATH OpenOpenAlexWikidataFDO

Authors Olaf Beyersdorff, Joshua Blinkhorn

Publication date 22 November 2019

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3355995

zbMATH Keywords

dependency schemesproof complexityquantified Boolean formulas

Mathematics Subject Classification ID

Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Shortening QBF proofs with dependency schemes
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Variable dependencies and Q-resolution
• Dependency Learning for QBF
• Dependency learning for QBF

Cited in

(9)

• Shortening QBF proofs with dependency schemes
• QBFFam: a tool for generating QBF families from proof complexity
• Proof complexity of QBF symmetry recomputation
• Using decomposition-parameters for QBF: mind the prefix!
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Understanding and extending incremental determinization for 2QBF
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Strong (D)QBF dependency schemes via implication-free resolution paths

This page was built for publication: Dynamic QBF dependencies in reduction and expansion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4972172)