Faster constraint solving with subtypes

10 years 9 months ago
Faster constraint solving with subtypes
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. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features – Constraints; D.2.1 [Software Engineering]: Requirements/Specifications – Languages, Tool...
Jonathan Edwards, Daniel Jackson, Emina Torlak, Vi
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Authors Jonathan Edwards, Daniel Jackson, Emina Torlak, Vincent Yeung
Comments (0)