License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.24
URN: urn:nbn:de:0030-drops-166986
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16698/
Go to the corresponding LIPIcs Volume Portal

Slivovsky, Friedrich

Quantified CDCL with Universal Resolution

pdf-format:
LIPIcs-SAT-2022-24.pdf (0.9 MB)

Abstract

Quantified Conflict-Driven Clause Learning (QCDCL) solvers for QBF generate Q-resolution proofs. Pivot variables in Q-resolution must be existentially quantified. Allowing resolution on universally quantified variables leads to a more powerful proof system called QU-resolution, but so far, QBF solvers have used QU-resolution only in very limited ways. We present a new version of QCDCL that generates proofs in QU-resolution by leveraging propositional unit propagation. We detail how conflict analysis must be adapted to handle universal variables assigned by propagation, and show that the procedure is still sound and terminating. We further describe how dependency learning can be incorporated in the algorithm to increase the flexibility of decision heuristics. Experiments with crafted instances and benchmarks from recent QBF evaluations demonstrate the viability of the resulting version of QCDCL.

BibTeX - Entry

@InProceedings{slivovsky:LIPIcs.SAT.2022.24,
  author =	{Slivovsky, Friedrich},
  title =	{{Quantified CDCL with Universal Resolution}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{24:1--24:16},
  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.dagstuhl.de/opus/volltexte/2022/16698},
  URN =		{urn:nbn:de:0030-drops-166986},
  doi =		{10.4230/LIPIcs.SAT.2022.24},
  annote =	{Keywords: QBF, Q-Resolution, QU-Resolution, CDCL}
}

Keywords: QBF, Q-Resolution, QU-Resolution, CDCL
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022
Supplementary Material: Software (Source Code): https://github.com/fslivovsky/miniQU

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI