Slicing for declarative models

With the growing popularity of analyzable declarative modeling languages, in general, and Alloy, in particular, it is imperative to develop new techniques that allow the underlying SAT solvers to scale to real systems. Slicing for declarative models is a novel technique that enables efficient analyses using constraint prioritization. Given a declarative model, the slicing algorithm identifies a slice which represents the model's base constraints. For the identification of base relations we have used three techniques: partial ordering, candidate set generation and heuristic evaluation. A satisfying solution to the extracted base slice is then systematically extended to generate a solution for the entire model, while unsatisfiability of the base implies unsatisfiability of the entire model. The experimental results show that it is possible to achieve significant improvements in the solving time using slicing and by generating candidate set it is possible to find the base set that improves the performance of the slicing algorithm significantly.