A combinatorial characterization of resolution width

Mostra el registre complet Registre parcial de l'ítem

• 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.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.en
• 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.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.doi http://dx.doi.org/10.1016/j.jcss.2007.06.025
• dc.identifier.issn 0022-0000
• dc.identifier.uri http://hdl.handle.net/10230/36435
• dc.language.iso eng
• dc.publisher Elsevier
• dc.relation.ispartof Journal of Computer and System Sciences. 2008 May;74(3):323-34.
• 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 © Elsevier http://dx.doi.org/10.1016/j.jcss.2007.06.025
• dc.rights.accessRights info:eu-repo/semantics/openAccess
• 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.title A combinatorial characterization of resolution width
• dc.type info:eu-repo/semantics/article
• dc.type.version info:eu-repo/semantics/acceptedVersion