Abstract
Recent work introduced an effective method for extraction of reduced unsatisfiable cores of CNF formulas as a by-product of validation of clausal proofs emitted by conflict-driven clause learning SAT solvers. In this paper, we demonstrate that this method for trimming CNF formulas can also benefit state-of-the-art tools for the computation of a Minimal Unsatisfiable Subformula (MUS). Furthermore, we propose a number of techniques that improve the quality of trimming, and demonstrate a significant positive impact on the performance of MUS extractors from the improved trimming. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Belov, A., Heule, M. J. H., & Marques-Silva, J. (2014). MUS extraction using clausal proofs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8561 LNCS, pp. 48–57). Springer Verlag. https://doi.org/10.1007/978-3-319-09284-3_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
