From SAT to QBF Solving

2^nd February 2024, 14:00
Dr Friedrich Slivovsky

Abstract

Propositional satisfiability (SAT) is the canonical NP-complete decision problem. Despite its theoretical hardness, there has been significant progress in practical solving, and SAT solvers have become a standard tool in areas such as formal methods and electronic design automation. However, the increasing complexity of specifications in these domains can lead to prohibitively large encodings that are unmanageable for even the most efficient SAT solvers. This challenge has prompted research into more succinct logics, such as Quantified Boolean Formulas (QBF), which extend propositional logic with universal and existential quantification over the Boolean domain. This talk will provide an introduction to SAT solving and an overview of the current state of QBF solving, including challenges and future research directions.