IMSc Webinar

Dependency Schemes in Quantified Boolean Formulas

Abhimanyu Choudhury

IMSc

Webinar https://bluejeans.com/985473264 QBF proof complexity is a relatively young field studying proof systems for quantified boolean logic. QBFs extend propositional logic by using both existential and universal quantifiers. Recently there has been great interest in QBF solving since QBFs are more expressive than SAT and have application in fields of formal verification and planning. QBF solving is basically an extension of SAT solving, thus QBF solvers are also based on extending SAT solvers which are based on the DPLL algorithm, however the nature of QBFs reduces the effectiveness of this extension and reduces the power of the solvers. Adding “dependency schemes” to the algorithm are a method of increasing the power of these solvers. In this talk we will cover some standard resolution based QBF proof systems which are key to understanding solving QBFs, then introduce and motivate what dependency schemes are and why they could be potentially very useful, and finally present proof systems for QBFs that incorporate these dependency schemes and provide proofs for their soundness and completeness.