MUP: a minimal unsatisfiability prover

ABSTRACT

After establishing the unsatisfiability of a SAT instance encoding a typical design task, there is a practical need to identify its minimal unsatisfiable subsets, which pinpoint the reasons for the infeasibility of the design. Due to the potentially expensive computation, existing tools for the extraction of unsatisfiable subformulas do not guarantee the minimality of the results. This paper describes a practical algorithm that decides the minimal unsatisfiability of any CNF formula through BDD manipulation. This algorithm has a worse-case complexity that is exponential only in the treewidth of the CNF formula. We provide an empirical evaluation of the algorithm, highlighting its efficiency on a set of hard problems as well as its ability to work with existing subformula extraction tools to achieve optimal results.

REFERENCES

• 1: Ron Aharoni , Nathan Linial, Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas, Journal of Combinatorial Theory Series A, v.43 n.2, p.196-204, Nov. 1986 [doi>10.1016/0097-3165(86)90060-9]
• 2: Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Faster SAT and smaller BDDs via common function structure, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 3: SAT Benchmarks from Automotive Product Configuration, http://www-sr.informatik.uni-tuebingen.de/~sinz/DC/.
• 4: Hans L. Bodlaender , John R. Gilbert , Hjálmtýr Hafsteinsson , Ton Kloks, Approximating treewidth, pathwidth, frontsize, and shortest elimination tree, Journal of Algorithms, v.18 n.2, p.238-255, March 1995 [doi>10.1006/jagm.1995.1009 ]
• 5: Renato Bruni, Approximating minimal unsatisfiable subformulae by means of adaptive core search, Discrete Applied Mathematics, v.130 n.2, p.85-100, 15 August 2003 [doi>10.1016/S0166-218X(02)00399-2]
• 6: Renato Bruni and Antonio Sassano. Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. Electronic Notes in Discrete Mathematics, 9, 2001.
• 7: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 8: Hans Kleine Büning, On subclasses of minimal unsatisfiable formulas, Discrete Applied Mathematics, v.107 n.1-3, p.83-98, Dec. 2000 [doi>10.1016/S0166-218X(00)00245-6 ]
• 9: J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In Proceedings of the International Conference on Very Large Scale Integration, 1991.
• 10: Adnan Darwiche , Mark Hopkins, Using Recursive Decomposition to Construct Elimination Orders, Jointrees, and Dtrees, Proceedings of the 6th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, p.180-191, September 19-21, 2001
• 11: Gennady Davydov , Inna Davydova , Hans Kleine Büning, An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, Annals of Mathematics and Artificial Intelligence, v.23 n.3-4, p.229-245, 1998
• 12: Rina Dechter. Bucket elimination: A unifying framework for probabilistic inference. In Proceedings of the 12th Conference on Uncertainty in Artificial Intelligence, pages 211--219, 1996.
• 13: Herbert Fleischner , Oliver Kullmann , Stefan Szeider, Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference, Theoretical Computer Science, v.289 n.1, p.503-516, 23 October 2002 [doi>10.1016/S0304-3975(01)00337-1 ]
• 14: Ramin Hojati , Sriram C. Krishnan , Robert K. Brayton, Early Quantification and Partitioned Transition Relations, Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, p.12-19, October 07-09, 1996
• 15: Holger H. Hoos and Thomas Sttzle. SATLIB: An Online Resource for Research on SAT. In I. P. Gent, H. v. Maaren, T. Walsh, editors, SAT 2000, pages 283--292. IOS Press, 2000. SATLIB is available online at www.satlib.org.
• 16: Jinbo Huang , Adnan Darwiche, Toward Good Elimination Orders for Symbolic SAT Solving, Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04), p.566-573, November 15-17, 2004 [doi>10.1109/ICTAI.2004.115]
• 17: Oliver Kullmann, An Application of Matroid Theory to the SAT Problem, Proceedings of the 15th Annual IEEE Conference on Computational Complexity, p.116, July 04-07, 2000
• 18: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 19: Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996710]
• 20: Christos H. Papadimitriou and David Wolfe. The complexity of facets resolved. In Proceedings of the 26th Annual Symposium on Foundations of Computer Science, pages 74--78, 1985.
• 21: C. H. Papadimitriou , M. Yannakakis, The complexity of facets (and some facets of complexity), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.255-260, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802199]
• 22: The Annual SAT Competitions: http://www.satlive.org/SATCompetition/.
• 23: Carsten Sinz , Andreas Kaiser , Wolfgang Küchlin, Formal methods for the validation of automotive product configuration data, Artificial Intelligence for Engineering Design, Analysis and Manufacturing, v.17 n.1, p.75-97, January 2003 [doi>10.1017/S0890060403171065]
• 24: Fabio Somenzi. CUDD: CU Decision Diagram Package. Release 2.4.0.
• 25: Stefan Szeider. Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. In Proceedings of the Nineth International Computing and Combinatorics Conference, pages 548--558. Springer Verlag, 2003.
• 26: Dimitrios M. Thilikos , Maria J. Serna , Hans L. Bodlaender, A Polynomial Time Algorithm for the Cutwidth of Bounded Degree Graphs with Small Treewidth, Proceedings of the 9th Annual European Symposium on Algorithms, p.380-390, August 28-31, 2001
• 27: H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDDs. In Proceedings of the IEEE International Conferece on Computer Aided Design, pages 130--133, 1990.
• 28: Alasdair Urquhart, Hard examples for resolution, Journal of the ACM (JACM), v.34 n.1, p.209-219, Jan. 1987 [doi>10.1145/7531.8928]
• 29: Lintao Zhang and Sharad Malik. Extracting small unsatisfiable cores from unsatisfiable Boolean formula. Presented at the Sixth International Conference on Theory and Applications of Satisfiability Testing, 2003.