Finding all minimal unsatisfiable subsets

ABSTRACT

An unsatisfiable set of constraints is minimal if all its (strict) subsets aresatisfiable.A number of forms of error diagnosis, including circuit error diagnosis and type error diagnosis, require finding all minimal unsatisfiable subsets of a given set of constraints (representing an error), in order to generate the best explanation of the error. In this paper we give algorithms for efficiently determining all minimal unsatisfiable subsets for any kind of constraints. We show how taking into account notions of independence of constraints and using incremental constraint solvers can significantly improve the calculation of these subsets.

REFERENCES

• 1: F. Brglez, P. Pownall, and R. Hum. Accelerated ATPG and fault grading via testability analysis. In IEEE Int. Symposium on Circuits and Systems, pages 695--698, 1985.
• 2: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 3: C. Codognet, P. Codognet, and G. File. Yet another intelligent backtracking method. In Logic Programming: Proceedings on the Joint International Conference and Symposium, pages 447--465, 1988.
• 4: Bruce Davey , Natashia Boland , Peter J. Stuckey, Efficient Intelligent Backtracking Using Linear Programming, INFORMS Journal on Computing, v.14 n.4, p.373-386, October 2002 [doi>10.1287/ijoc.14.4.373.2823]
• 5: B. De Backer and H. Beringer. Intelligent backtracking for CLP languages: an application to CLP(R). In Logic Programming: Proceedings of the 1991 International Symposium, pages 405--419, 1991.
• 6: Yousri El Fattah and Rina Dechter. Diagnosing tree-decomposable circuits. In IJCAI, pages 1742--1749, 1995.
• 7: B. Han and S-J. Lee. Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics, 29(2):281--286, 1999.
• 8: Aimin Hou, A theory of measurement in diagnosis from first principles, Artificial Intelligence, v.65 n.2, p.281-328, Feb. 1994 [doi>10.1016/0004-3702(94)90019-1 ]
• 9: Ulrich Junker. Quickxplain: Conflict detection for arbitrary constraint propagation algorithms. In IJCAI'01 Workshop on Modelling and Solving problems with constraints (CONS-1), Seattle, WA, USA, August 2001.
• 10: M. Paterson and M. Wegman. Linear unification. Journal of Computer and System Sciences, 16(2):158--167, 1978.
• 11: R Reiter, A theory of diagnosis from first principles, Artificial Intelligence, v.32 n.1, p.57-95, April 1987 [doi>10.1016/0004-3702(87)90062-2 ]
• 12: M. Schroeder. Revise. http://www.soi.city.ac.uk/~msch/revise/revise.html+.
• 13: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 14: M. Sulzmann and J. Wazny. Chameleon. http://www.comp.nus.edu.sg/~sulzmann/chameleon.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms

Keywords:
constraint solving, minimal unsatisfiable subsets