Abstract
A minimal unsatisfiable subformula (MUS) of a given CNF is a set of clauses which is unsatisfiable, but becomes satisfiable as soon as we remove any of its clauses. In practical scenarios it is often useful to know, in addition to the unsolvability of an instance, which parts of the instance cause the unsolvability. An approach is here proposed to the problem of automatic detection of such a subformula, with the double aim of finding quickly a small-sized one. We make use of an adaptive technique in order to rapidly select an unsatisfiable subformula which is a good approximation of a MUS. Hard unsatisfiable instances can be reduced to remarkably smaller problems, and hence efficiently solved, through this approach.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. N. Hooker and V. Vinay. Branching Rules for Satisfiability. Journal of Automated Reasoning, 15:359–383, 1995.
D. S. Johnson and M. A. Trick, editors. Cliques, Coloring, and Satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 1996.
O. Kullmann. An application of matroid theory to the SAT Problem. ECCC TR00-018, Feb. 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruni, R., Sassano, A. (2000). Finding Minimal Unsatisfiable Subformulae in Satisfiability Instances. In: Dechter, R. (eds) Principles and Practice of Constraint Programming – CP 2000. CP 2000. Lecture Notes in Computer Science, vol 1894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45349-0_37
Download citation
DOI: https://doi.org/10.1007/3-540-45349-0_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41053-9
Online ISBN: 978-3-540-45349-9
eBook Packages: Springer Book Archive