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.
