Abstract
We introduce an algorithm for finding a minimal unsatisfiable subset (MUS) of a CNF formula. We have implemented and evaluated the algorithm and found that its performance is very competitive on a wide range of benchmarks, including both formulas that are close to minimal unsatisfiable and formulas containing MUSes that are only a small fraction of the formula size.
In our simple but effective algorithm we associate assignments with clauses. The notion of associated assignment has emerged from our work on a Brouwer’s fixed point approximation algorithm applied to satisfiability. There, clauses are regarded to be entities that order the set of assignments and that can select an assignment to be associated with them, resulting in a Pareto optimal agreement.
In this presentation we abandon all terminology from this theory which is superfluous with respect to the recent objective and make the paper self contained.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Constraint Satisfaction Problem
- Truth Assignment
- Binary Decision Diagram
- Satisfying Assignment
- Symbolic Model Check
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Nam, G.J., Sakallah, K.A., Rutenbar, R.A.: Satisfiability-based layout revisited: Detailed routing of complex FPGAs vis search-based Boolean SAT. In: FPGA, pp. 167–175 (1999)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
McMillan, K.L.: Interpolants and symbolic model checking. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 89–90. Springer, Heidelberg (2007)
Rintanen, J., Heljanko, K., Niemelä, I.: Planning as satisfiability: parallel plans and algorithms for plan search. Artif. Intell. 170(12-13), 1031–1080 (2006)
Zhang, L., Malik, S.: Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8 (2003)
Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: AMUSE: A minimally-unsatisfiable subformula extractor. In: Malik, S., Fix, L., Kahng, A.B. (eds.) DAC, pp. 518–523. ACM, New York (2004)
Grégoire, É., Mazure, B., Piette, C.: Local-search extraction of MUSes. Constraints 12(3), 325–344 (2007)
Lynce, I., Silva, J.P.M.: On computing minimum unsatisfiable cores. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, Springer, Heidelberg (2005)
Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas [25], 173–186
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (2008)
Wieringa, S.: Finding cores using a Brouwer’s fixed point approximation algorithm. Master’s thesis, Delft University of Technology, Faculty of EWI (2007)
van Maaren, H.: Pivoting algorithms based on Boolean vector labeling. Acta Mathematica Vietnamica 22(1), 183–198 (1997)
Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. [24] 22–35
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. [15] 61–75
Tamiz, M., Mardle, S.J., Jones, D.F.: Detecting IIS in infeasible linear programmes using techniques from goal programming. Computers & OR 23(2), 113–119 (1996)
Galinier, P., Hertz, A.: Solution techniques for the large set covering problem. Discrete Applied Mathematics 155(3), 312–326 (2007)
de Siqueira, N.J.L., Puget, J.-F.: Explanation-based generalisation of failures. In: ECAI, pp. 339–344 (1988)
Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. [24] 36–41
Huang, J.: MUP: A minimal unsatisfiability prover. In: Tang, T.A. (ed.) ASP-DAC, pp. 432–437. ACM Press, New York (2005)
Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult instances of Boolean satisfiability in the presence of symmetry. IEEE Trans. on CAD of Integrated Circuits and Systems 22(9), 1117–1137 (2003)
Darwiche, A.: New advances in compiling CNF into decomposable negation normal form. In: de Mántaras, R.L., Saitta, L. (eds.) ECAI, pp. 328–332. IOS Press, Amsterdam (2004)
Aloul, F.A., Markov, I.L., Sakallah, K.A.: MINCE: A static global variable-ordering heuristic for SAT search and BDD manipulation. J. UCS 10(12), 1562–1596 (2004)
Biere, A., Gomes, C.P. (eds.): SAT 2006. LNCS, vol. 4121. Springer, Heidelberg (2006)
Bacchus, F., Walsh, T. (eds.): SAT 2005. LNCS, vol. 3569. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Maaren, H., Wieringa, S. (2008). Finding Guaranteed MUSes Fast. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)