Local Symmetries in Propositional Logic

Abstract

The symmetry rule in propositional logic allows the exploitation of symmetries present in a problem. In the context of resolution, the rule enables the shortening of refutations by using symmetries present in an initial set of clauses. These symmetries can be local or global. The present paper proves that the local symmetry rule is strictly more powerful than the global symmetry rule. It also exhibits sets of clauses that show exponential lower bounds for the local symmetry rule, where the symmetry group consists of all variable permutations. These examples remain exponentially hard even when the symmetry group is enlarged to include complementation. Examples are exhibited in which resolution with the global symmetry rule has an exponential speed-up with respect to the cutting plane refutation system.