Alasdair Urquhart (with Noriko H. Arai)
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.