Symmetry Reduction for SAT Representations of Transition Systems

All Papers

Symmetries are inherent in systems that consist of several interchangeable objects or components. When reasoning about such systems, big computational savings can be obtained if the presence of symmetries is recognized. In earlier work, symmetries in constraint satisfaction problems have been handled by introducing symmetry-breaking constraints. In reasoning about transition systems, notably in model-checking and reachability analysis in computer-aided verification, symmetries have been handled by symmetry reduction algorithms that eliminate redundant search caused by symmetries. In this work, we investigate symmetry handling in a problem in the intersection of these two areas: handling symmetries in representations of transition systems in the propositional logic. The problem shows up in representations of AI planning as a satisfiability problem, and in recent approaches to model-checking that represent transition systems as propositional formulae. Symmetry-breaking constraints can be added to the propositional logic representation of transition sequences for removing all the symmetry at one point of time, but removing symmetry from the whole transition sequence is much more difficult, and has not been addressed in earlier work. We present a solution to the problem.