AMUSE: a minimally-unsatisfiable subformula extractor

ABSTRACT

This paper describes a new algorithm for extracting unsatisfiable subformulas from a given unsatisfiable CNF formula. Such unsatisfiable "cores" can be very helpful in diagnosing the causes of infeasibility in large systems. Our algorithm is unique in that it adapts the "learning process" of a modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. Compared to existing approaches, this method can be viewed as a bottom-up core extraction procedure which can be very competitive when the core sizes are much smaller than the original formula size. Repeated runs of the algorithm with different branching orders yield different cores. We present experimental results on a suite of large automotive benchmarks showing the performance of the algorithm and highlighting its ability to locate not just one but several cores.

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: R. Bruni and A. Sassano, "Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae," in Electronic Notes in Discrete Mathematics, vol. 9, 2001.
• 3: 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 [doi>10.1023/A:1018924526592]
• 4: 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]
• 5: 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]
• 6: N. Eén, and N. Sörensson, "An Extensible SAT-solver," in Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT), 2003.
• 7: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 8: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 9: Gi-Joon Nam , Fadi Aloul , Karem Sakallah , Rob Rutenbar, A comparative study of two Boolean formulations of FPGA detailed routing constraints, Proceedings of the 2001 international symposium on Physical design, p.222-227, April 01-04, 2001, Sonoma, California, United States [doi>10.1145/369691.369777]
• 10: Christos H. Papadimitriou , David Wolfe, The complexity of facets resolved, Journal of Computer and System Sciences, v.37 n.1, p.2-13, August 1988 [doi>10.1016/0022-0000(88)90042-6]
• 11: SAT benchmarks from Automotive Product Configuration, http://www-sr.informatik.uni-tuebingen.de/sinz/DC/
• 12: 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]
• 13: Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379019]
• 14: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 15: L. Zhang and S. Malik, "Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula," presented at Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), S. Margherita Ligure - Portofino, Italy, 2003.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.1 Combinatorics
          Subjects: Combinatorial algorithms

General Terms:
Algorithms, Verification

Keywords:
boolean satisfiability (SAT), conjunctive normal form (CNF), diagnosis, minimally-unsatisfiable subformula (MUS)