2026-07-22T13:00:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18482 2024-03-06T11:02:01Z ddc:004 open_access

QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas Plank, Andreas Seidl, Martina Minimal Unsatisfiable Core Quantified Boolean Formula 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andreas Plank and Martina Seidl 2023 Is Part Of LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2023.20 urn:nbn:de:0030-drops-184824 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.20 eng https://creativecommons.org/licenses/by/4.0/legalcode