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.2023.20
URN: urn:nbn:de:0030-drops-184824
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18482/
Plank, Andreas ;
Seidl, Martina
QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas
Abstract
In this paper, we present QMusExt, a tool for the extraction of minimal unsatisfiable sets (MUS) from quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF). Our tool generalizes an efficient algorithm for MUS extraction from propositional formulas that analyses and rewrites resolution proofs generated by SAT solvers.
In addition to extracting unsatisfiable cores from false formulas in PCNF, we apply QMusExt also to obtain satisfiable cores from Q-resolution proofs of true formulas in prenex disjunctive normal form (PDNF).
BibTeX - Entry
@InProceedings{plank_et_al:LIPIcs.SAT.2023.20,
author = {Plank, Andreas and Seidl, Martina},
title = {{QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {20:1--20:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18482},
URN = {urn:nbn:de:0030-drops-184824},
doi = {10.4230/LIPIcs.SAT.2023.20},
annote = {Keywords: Minimal Unsatisfiable Core, Quantified Boolean Formula}
}
