Skip to main content

Research Repository

Advanced Search

The Complexity of Resolution with Generalized Symmetry Rules

Szeider, Stefan

The Complexity of Resolution with Generalized Symmetry Rules Thumbnail


Authors

Stefan Szeider



Abstract

We generalize Krishnamurthys well-studied symmetry rule for resolution systems by considering homomorphisms instead of symmetries; symmetries are injective maps of literals whichpreserve 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 allows 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 prove a similar result for local and global homomorphisms. Finally, we obtain an exponential lower bound for the resolution system enhanced by the local homomorphism rule.

Citation

Szeider, S. (2005). The Complexity of Resolution with Generalized Symmetry Rules. Theory of Computing Systems, 38(2), 171-188. https://doi.org/10.1007/s00224-004-1192-0

Journal Article Type Article
Publication Date 2005-02
Deposit Date Oct 14, 2008
Publicly Available Date Oct 14, 2008
Journal Theory of Computing Systems
Print ISSN 1432-4350
Electronic ISSN 1433-0490
Publisher Springer
Peer Reviewed Peer Reviewed
Volume 38
Issue 2
Pages 171-188
DOI https://doi.org/10.1007/s00224-004-1192-0

Files





You might also like



Downloadable Citations