On the interplay of cube learning and dependency schemes in QCDCL proof systems

DOI10.4230/LIPICS.FSTTCS.2025.25MaRDI QIDQ7391897zbMATH OpenFDO

Authors Abhimanyu Choudhury, Meena Mahajan

Publication date 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.FSTTCS.2025.25

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theory of computing (68Qxx)

Cites work

• Backdoor sets of quantified Boolean formulas
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Davis and Putnam meet Henkin: solving DQBF with resolution
• Dependency Learning for QBF
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Long-distance Q-resolution with dependency schemes
• Lower bounds for multiplayer noncooperative games of incomplete information
• Lower bounds for QCDCL via formula gauge
• New resolution-based QBF calculi and their proof complexity
• On the power of clause-learning SAT solvers as resolution engines
• QCDCL with cube learning or pure literal elimination -- what is best?
• Shortening QBF proofs with dependency schemes
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Unified QBF certification and its applications

This page was built for publication: On the interplay of cube learning and dependency schemes in QCDCL proof systems

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