<div class="csl-bib-body">
<div class="csl-entry">Reichl, F. X., & Slivovsky, F. (2022). Pedant: A Certifying DQBF Solver. In <i>25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)</i> (pp. 1–10). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2022.20</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/150299
-
dc.description.abstract
Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) that combines propositional definition extraction with Counterexample-Guided Inductive Synthesis (CEGIS) to compute a model of a given formula. Pedant 2 improves upon an earlier version in several ways. We extend the notion of dependencies by allowing existential variables to depend on other existential variables. This leads to more and smaller definitions, as well as more concise repairs for counterexamples. Additionally, we reduce counterexamples by determining minimal separators in a conflict graph, and use decision tree learning to obtain default functions for undetermined variables. An experimental evaluation on standard benchmarks showed a significant increase in the number of solved instances compared to the previous version of our solver.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)