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

Created from the Publication Database of the Vienna University of Technology.