Should Decisions in QCDCL Follow Prefix Order?
From MaRDI portal
Publication:6493568
DOI10.1007/S10817-024-09694-6WikidataQ128170471 ScholiaQ128170471MaRDI QIDQ6493568
Benjamin Böhm, Olaf Beyersdorff, Tomáš Peitl
Publication date: 29 April 2024
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Cites Work
- On the power of clause-learning SAT solvers as resolution engines
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Backdoor sets of quantified Boolean formulas
- Resolution for quantified Boolean formulas
- Lower bounds for QCDCL via formula gauge
- Expansion-based QBF solving versus Q-resolution
- Solution validation and extraction for QBF preprocessing
- Long-distance Q-resolution with dependency schemes
- Unified QBF certification and its applications
- The relative efficiency of propositional proof systems
- Dependency Learning for QBF
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
This page was built for publication: Should Decisions in QCDCL Follow Prefix Order?
