Show simple item record

dc.contributor.author Atserias, Albert
dc.contributor.author Dalmau, Víctor
dc.date.accessioned 2019-01-25T08:13:34Z
dc.date.available 2019-01-25T08:13:34Z
dc.date.issued 2008
dc.identifier.citation Atserias A, Dalmau A. A combinatorial characterization of resolution width. J Comput Syst Sci. 2008 May;74(3):323-34. DOI: 10.1016/j.jcss.2007.06.025
dc.identifier.issn 0022-0000
dc.identifier.uri http://hdl.handle.net/10230/36435
dc.description.abstract We provide a characterization of the resolution width introduced in the context of propositional proof complexity in terms of the existential pebble game introduced in the context of finite model theory. The characterization is tight and purely combinatorial. Our first application of this result is a surprising proof that the minimum space of refuting a 3-CNF formula is always bounded from below by the minimum width of refuting it (minus 3). This solves a well-known open problem. The second application is the unification of several width lower bound arguments, and a new width lower bound for the dense linear order principle. Since we also show that this principle has resolution refutations of polynomial size, this provides yet another example showing that the relationship between size and width cannot be made subpolynomial.
dc.description.sponsorship Supported in part by CICYT TIN2004-04343 and by the European Commission through the RTN COMBSTRU HPRN-CT2002-00278. Research partially supported by the MEC under the program “Ramon y Cajal,” grants TIC 2002-04470-C03 and TIC 2002-04019-C03, the EU PASCAL Network of Excellence, IST-2002-506778, and the MODNET Marie Curie Research Training Network, MRTN-CT-2004-512234.
dc.format.mimetype application/pdf
dc.language.iso eng
dc.publisher Elsevier
dc.relation.ispartof Journal of Computer and System Sciences. 2008 May;74(3):323-34.
dc.rights © Elsevier http://dx.doi.org/10.1016/j.jcss.2007.06.025
dc.title A combinatorial characterization of resolution width
dc.type info:eu-repo/semantics/article
dc.identifier.doi http://dx.doi.org/10.1016/j.jcss.2007.06.025
dc.subject.keyword Resolution
dc.subject.keyword Width
dc.subject.keyword Pebble games
dc.subject.keyword 3-CNF formula
dc.subject.keyword Finite model theory
dc.subject.keyword Constraint satisfaction problems
dc.relation.projectID info:eu-repo/grantAgreement/ES/2PN/TIN2004-04343
dc.relation.projectID info:eu-repo/grantAgreement/ES/1PN/TIC2002-04470-C03
dc.relation.projectID info:eu-repo/grantAgreement/ES/1PN/TIC2002-04019-C03
dc.relation.projectID info:eu-repo/grantAgreement/EC/FP6/506778
dc.relation.projectID info:eu-repo/grantAgreement/EC/FP6/512234
dc.rights.accessRights info:eu-repo/semantics/openAccess
dc.type.version info:eu-repo/semantics/acceptedVersion


This item appears in the following Collection(s)

Show simple item record

Search DSpace


Advanced Search

Browse

My Account

Statistics

Compliant to Partaking