Symmetry Reduction for SAT Representations of Transition Systems

8 years 5 months ago
Symmetry Reduction for SAT Representations of Transition Systems
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...
Jussi Rintanen
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Where AIPS
Authors Jussi Rintanen
Comments (0)