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...

• Type: Conference
• Year: 2003
• Where: AIPS
• Authors: Jussi Rintanen
• Keywords: AIPS 2003, Artificial Intelligence, Symmetries, Symmetry-breaking Constraints, Transition Systems