Faster constraint solving with subtypes

ABSTRACT

Constraints in predicate or relational logic can be translated into boolean logic and solved with a SAT solver. For faster solving, it is common to exploit the typing of predicates or relations, in order to reduce the number of boolean variables needed to encode the constraint. Here we show how to extend this idea to constraints expressed in a language with subtyping. Our technique, called atomization, refactors the type hierarchy into a flat collection of disjoint atomic types. The constraints are then decomposed into equivalent constraints involving smaller relations or predicates over these new types, which can then be solved in the normal fashion. Experiments with an implementation of this technique within the Alloy Analyzer show improved performance on practical software checking problems.

REFERENCES

• 1: T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A Model Checker for Concurrent Software. Microsoft Research Technical Report MSR-TR-2004-10. January, 2004.
• 2: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 3: Avrim L. Blum , Merrick L. Furst, Fast planning through planning graph analysis, Artificial Intelligence, v.90 n.1-2, p.281-300, Feb. 1997 [doi>10.1016/S0004-3702(96)00047-1]
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2000.
• 6: Jonathan Edwards, Daniel Jackson, and Emina Torlak. A Type System for Object Models. Submitted for publication. http://sdg.lcs.mit.edu/pubs/TR/typesforobjectmodels.pdf
• 7: Peter Harry Eidorff , Fritz Henglein , Christian Mossin , Henning Niss , Morten Heine Sørensen , Mads Tofte, AnnoDomini: from type theory to Year 2000 conversion tool, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292543]
• 8: Michael Ernst, Todd Millstein and Daniel Weld. Automatic SAT compilation of planning problems. Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), 1997.
• 9: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 10: Paul Halmos. Problems for Mathematicians, Young and Old. The Mathematical Association of America, 1991.
• 11: Gerard J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2004.
• 12: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 13: Daniel Jackson , Somesh Jha , Craig A. Damon, Isomorph-free model enumeration: a new method for checking relational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.302-343, March 1998 [doi>10.1145/276393.276396]
• 14: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 15: Rajeev Joshi, Greg Nelson, and Keith Randall. Denali: a goal-directed superoptimizer. http://citeseer.nj.nec.com/joshi01denali.html
• 16: Henry Kautz , Bart Selman, Planning as satisfiability, Proceedings of the 10th European conference on Artificial intelligence, p.359-363, August 1992, Vienna, Austria
• 17: Sarfraz Khurshid , Daniel Jackson, Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer, Proceedings of the 15th IEEE international conference on Automated software engineering, p.13, September 11-15, 2000
• 18: Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 19: Leslie Lamport , Lawrence C. Paulson, Should your specification language be typed, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.502-526, May 1999 [doi>10.1145/319301.319317]
• 20: Michael Leuschel and Michael Butler. ProB: A Model Checker for B. Proceedings Formal Methods Europe, 2003.
• 21: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 22: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 23: 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]
• 24: Robert O'Callahan , Daniel Jackson, Lackwit: a program understanding tool based on type inference, Proceedings of the 19th international conference on Software engineering, p.338-348, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253351]
• 25: Piza, The Prolog Z Animator. http://www.noodles.demon.co.uk/PiZA/PiZAHome.html
• 26: Ilya Shlyakter. Generating effective symmetry-breaking predicates for search problems. Electronic Notes in Discrete Mathematics, Vol. 9 (2001).
• 27: Mandana Vaziri and Daniel Jackson. Checking Properties of Heap-Manipulating Procedures using a Constraint Solver. Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Warsaw, Poland, April, 2003.
• 28: Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing formal specifications with constraint programming. Technical Report 97-12a, Department of Computer Science, Iowa State University, August, 1998.
• 29: D. S. Weld. Recent advances in AI planning. AI Magazine, 20(2):93--123, 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Constraints

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages; Tools

General Terms:
Design, Languages, Verification

Keywords:
SAT, analysis, constraints, relational logic, subtypes, verification