Quantified CDCL and Dependency Schemes: A proof-theoretic study [HBNI Th278]

Abstract

Quantified Conflict Driven Clause Learning (QCDCL) is one of the main approaches to solving Quantified Boolean Formulas (QBF). Cube-learning is employed in this approach to ensure that true formulas can be verified. Dependency Schemes help to detect spurious dependencies that are implied by the variable ordering in the quantifier prefix of QBFs but are not essential for constructing (counter)models. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The simplest underlying proof system QCDCL [BB23a], formalises the reasoning in the QCDCL approach on false formulas, when neither cube-learning nor dependency schemes is used. The work of [BPB24] further incorporates cube-learning. This thesis is the first work that incorporates the dependency scheme heuristic in the QCDCL proof system. The usage of dependency schemes in QCDCL proof system with and with- out cube-learning are formalised and these new family of systems, the D1 + QCDCLORD (ClausePol, CubePol) proof systems, which incorporates dependency schemes into the proof system, and show it to be sound and complete. When the decisions are restricted to follow level order, but dependency schemes are used in propagation and learning, in conjunction with cube-learning, the resulting proof systems using the dependency schemes Dstd and Drrs are investigated in detail and their relative strengths are analysed.