The Complexity of Resolution with Generalized Symmetry RulesTheory of Computing Systems (Springer), vol. 38, no. 2, pp. 171-188, 2005. A peliminary version of this paper appeared in the Proceedings of the 20th International Symposium on Theoretical Aspects of Computer Science, STACS 2003, Eds.: H. Alt, M. Habib; Lecture Notes in Computer Science 2607, pp. 475-486, Springer Verlag 2003.) See also the list of open problems collected by Toniann Pitassi at the Theory Open Problems Session, Department of Computer Science, University of Toronto, June 17, 2003. Download: [paper ps] [paper pdf] Abstract:We generalize Krishnamurthy's well-studied symmetry rule for resolution systems by considering homomorphisms instead of symmetries; symmetries are injective maps of literals which preserve complements and clauses; homomorphisms arise from symmetries by releasing the constraint of being injective.We prove that the use of homomorphisms yields a strictly more powerful system than the use of symmetries by exhibiting an infinite sequence of sets of clauses for which the consideration of global homomorphisms yields exponentially shorter proofs than the consideration of local symmetries. It is known that local symmetries give rise to a strictly more powerful system than global symmetries---we show a similar result for local and global homomorphisms. Finally, we pinpoint an exponential lower bound for the resolution system enhanced by the local homomorphism rule. [back to Stefan Szeider's homepage] |