Solving of Dependency Quantified Boolean Formulas with Counterexample-Guided Synthesis

Abstract:
Dependency Quantified Boolean Formulas (DQBF) succinctly encode the existence of Boolean functions subject to constraints, and as such can naturally express synthesis problems in verification. In this talk, I will present an algorithm for solving DQBF that iteratively refines a candidate model based on counterexamples. I will cover techniques that are crucial to make it work well in practice, such as identifying uniquely determined functions by definition extraction. One limitation of this approach is that counterexamples often contain spurious literals that are required only to ensure consistency of the candidate model. In the second part of the talk, I will present ongoing work towards getting rid of these literals and working with concise counterexamples.

Biodata:
Friedrich Slivovsky completed his PhD in Computer Science at TU Wien (Vienna) under Stefan Szeider. He will be serving as Program Co-Chair of SAT 2023, the premier conference in the area of Theory and Practice of Satisfiability