Conditional Term Equivalent Symmetry Breaking for SAT

Symmetry-breaking is a technique for efficiently solving SAT instances that contain high degrees of symmetry among the variables of the instance. When satisfiability problems are represented as a relational schema, symmetries between objects in the domain can be detected directly from evidence, that is, variables known to have a particular setting prior to solving. These symmetries between domain objects are called term symmetries. In this work, we present two novel extensions to the technique of term equivalent symmetry breaking which allow the detection and exploitation of conditional or hidden symmetries, those relationships between domain objects that are obscured until the instance is partially solved. We give promising preliminary experimental results for this technique, and discuss how the techniques could be extended for use in probabilistic domains.