Abstract
We tackle the problem of finding a smallest-cardinality MUS (SMUS) of a given formula. The SMUS provides a succinct explanation of infeasibility and is valuable for applications that rely on such explanations. We present a branch-and-bound algorithm that utilizes iterative MAXSAT solutions to generate lower and upper bounds on the size of the SMUS, and branch on specific subformulas to find it. We report experimental results on formulas from DIMACS and DaimlerChrysler product configuration suites.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bruni, R., Sassano, A.: Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae. Electronic Notes in Discrete Mathematics 9 (2001)
Huang, J.: MUP: A Minimal Unsatisfiability Prover. In: Proceedings of Asia South Pacific Design Automation Conference (2005)
Liffiton, M., Andraus, Z., Sakallah, K.: From MAX-SAT to Min-UNSAT: Insights and Applications. Technical Report CSE-TR-506-05, University of Michigan (2005)
Lynce, I., Marques-Silva, J.: On Computing Minimum Unsatisfiable Cores. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 305–310. Springer, Heidelberg (2005)
SAT benchmarks from Automotive Product Configuration, http://www-sr.informatik.unituebingen.de/~sinz/DC/
Zhang, L., Malik, S.: Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mneimneh, M., Lynce, I., Andraus, Z., Marques-Silva, J., Sakallah, K. (2005). A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_40
Download citation
DOI: https://doi.org/10.1007/11499107_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)