1 Search Results for "Reichl, Franz-Xaver"

Document
DOI: 10.4230/LIPIcs.SAT.2022.20
Pedant: A Certifying DQBF Solver

Authors: Franz-Xaver Reichl and Friedrich Slivovsky

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.
Cite as

Franz-Xaver Reichl and Friedrich Slivovsky. Pedant: A Certifying DQBF Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 20:1-20:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{reichl_et_al:LIPIcs.SAT.2022.20,
  author =	{Reichl, Franz-Xaver and Slivovsky, Friedrich},
  title =	{{Pedant: A Certifying DQBF Solver}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{20:1--20:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.20},
  URN =		{urn:nbn:de:0030-drops-166941},
  doi =		{10.4230/LIPIcs.SAT.2022.20},
  annote =	{Keywords: DQBF, DQBF Solver, Decision Procedure, Certificates}
}
  • Refine by Author
  • 1 Reichl, Franz-Xaver
  • 1 Slivovsky, Friedrich

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning

  • Refine by Keyword
  • 1 Certificates
  • 1 DQBF
  • 1 DQBF Solver
  • 1 Decision Procedure

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact