Notice
This item was automatically migrated from a legacy system. It's data has not been checked and might not meet the quality criteria of the present system.
Reichl, F.-X., Slivovsky, F., & Szeider, S. (2021). Certified DQBF Solving by Definition Extraction. In Theory and Applications of Satisfiability Testing – SAT 2021 (pp. 499–517). LNCS / Springer. https://doi.org/10.1007/978-3-030-80223-3_34
E192-01 - Forschungsbereich Algorithms and Complexity
-
Published in:
Theory and Applications of Satisfiability Testing – SAT 2021
-
Date (published):
2021
-
Event name:
SAT 2021
-
Event date:
5-Jul-2021 - 9-Jul-2021
-
Event place:
Barcelona, Spain
-
Number of Pages:
19
-
Publisher:
LNCS / Springer, 12831
-
Peer reviewed:
Yes
-
Abstract:
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 return...
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.