Cookies

We use cookies to ensure that we give you the best experience on our website. You can change your cookie settings at any time. Otherwise, we'll assume you're OK to continue.


Durham Research Online
You are in:

The complexity of resolution with generalized symmetry rules.

Szeider, S. (2005) 'The complexity of resolution with generalized symmetry rules.', Theory of computing systems., 38 (2). pp. 171-188.

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.

Item Type:Article
Full text:PDF - Accepted Version (179Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/s00224-004-1192-0
Record Created:14 Oct 2008
Last Modified:10 Aug 2011 16:31

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Usage statisticsLook up in GoogleScholar | Find in a UK Library