[Back]

F. Reichl, F. Slivovsky, S. Szeider:
"Certified DQBF Solving by Definition Extraction";
Talk: Int. Conference on Theory and Applications of Satisfiability Testing, Barcelona, Spanien; 2021-07-05 - 2021-07-09; in: "Theory and Applications of Satisfiability Testing - SAT 2021", LNCS / Springer, 12831 (2021), ISBN: 978-3-030-80222-6; 499 - 517.

We propose a new decision procedure for dependency quantified
Boolean formulas (DQBFs) that uses interpolation-based definition
extraction to compute Skolem functions in a counter-example guided
inductive synthesis (CEGIS) loop. In each iteration, a family of candidate
Skolem functions is tested for correctness using a SAT solver, which
either determines that a model has been found, or returns an assignment
of the universal variables as a counterexample. Fixing a counterexample
generally involves changing candidates of multiple existential variables
with incomparable dependency sets. Our procedure introduces auxiliary
variables-which we call arbiter variables-that each represent the value
of an existential variable for a particular assignment of its dependency
set. Possible repairs are expressed as clauses on these variables, and a
SAT solver is invoked to find an assignment that deals with all previously
seen counterexamples. Arbiter variables define the values of Skolem functions
for assignments where they were previously undefined, and may lead
to the detection of further Skolem functions by definition extraction.
A key feature of the proposed procedure is that it is certifying by
design: for true DQBF, models can be returned at minimal overhead.
Towards certification of false formulas, we prove that clauses can be
derived in an expansion-based proof system for DQBF.
In an experimental evaluation on standard benchmark sets, a prototype
implementation was able to match (and in some cases, surpass)
the performance of state-of-the-art-solvers. Moreover, models could be
extracted and validated for all true instances that were solved.

http://dx.doi.org/10.1007/978-3-030-80223-3_34

https://publik.tuwien.ac.at/files/publik_300076.pdf