Reichl, F. X., & Slivovsky, F. (2022). Pedant: A Certifying DQBF Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) (pp. 1–10). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2022.20
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
Project (external):
Vienna Science and Technology Fund (WWTF) Austrian Science Fund (FWF)
CC BY 4.0
