Should Decisions in QCDCL Follow Prefix Order?

DOI10.1007/S10817-024-09694-6MaRDI QIDQ6493568zbMATH OpenWikidataFDO

Authors Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff

Publication date 29 April 2024

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-024-09694-6

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On Q-resolution and CDCL QBF solving
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• On CDCL-Based Proof Systems with the Ordered Decision Strategy
• On CDCL-based proof systems with the ordered decision strategy

Cites work

• Backdoor sets of quantified Boolean formulas
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Dependency Learning for QBF
• Expansion-based QBF solving versus Q-resolution
• Long-distance Q-resolution with dependency schemes
• Lower bounds for QCDCL via formula gauge
• On the power of clause-learning SAT solvers as resolution engines
• Resolution for quantified Boolean formulas
• Solution validation and extraction for QBF preprocessing
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• The relative efficiency of propositional proof systems
• Unified QBF certification and its applications

Cited in

(1)

• QCDCL with cube learning or pure literal elimination -- what is best?

This page was built for publication: Should Decisions in QCDCL Follow Prefix Order?

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