Simplified and Improved Separations Between Regular and General Resolution by Lifting

We give a significantly simplified proof of the exponential separation between regular and general resolution of Alekhnovich et al. (2007) as a consequence of a general theorem lifting proof depth to regular proof length in resolution. This simpler proof then allows us to strengthen the separation f...

Descripción completa

Detalles Bibliográficos
Autores principales: Vinyals, Marc, Elffers, Jan, Johannsen, Jan, Nordström, Jakob
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326554/
http://dx.doi.org/10.1007/978-3-030-51825-7_14
_version_ 1783552369602068480
author Vinyals, Marc
Elffers, Jan
Johannsen, Jan
Nordström, Jakob
author_facet Vinyals, Marc
Elffers, Jan
Johannsen, Jan
Nordström, Jakob
author_sort Vinyals, Marc
collection PubMed
description We give a significantly simplified proof of the exponential separation between regular and general resolution of Alekhnovich et al. (2007) as a consequence of a general theorem lifting proof depth to regular proof length in resolution. This simpler proof then allows us to strengthen the separation further, and to construct families of theoretically very easy benchmarks that are surprisingly hard for SAT solvers in practice.
format Online
Article
Text
id pubmed-7326554
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73265542020-07-01 Simplified and Improved Separations Between Regular and General Resolution by Lifting Vinyals, Marc Elffers, Jan Johannsen, Jan Nordström, Jakob Theory and Applications of Satisfiability Testing – SAT 2020 Article We give a significantly simplified proof of the exponential separation between regular and general resolution of Alekhnovich et al. (2007) as a consequence of a general theorem lifting proof depth to regular proof length in resolution. This simpler proof then allows us to strengthen the separation further, and to construct families of theoretically very easy benchmarks that are surprisingly hard for SAT solvers in practice. 2020-06-26 /pmc/articles/PMC7326554/ http://dx.doi.org/10.1007/978-3-030-51825-7_14 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Vinyals, Marc
Elffers, Jan
Johannsen, Jan
Nordström, Jakob
Simplified and Improved Separations Between Regular and General Resolution by Lifting
title Simplified and Improved Separations Between Regular and General Resolution by Lifting
title_full Simplified and Improved Separations Between Regular and General Resolution by Lifting
title_fullStr Simplified and Improved Separations Between Regular and General Resolution by Lifting
title_full_unstemmed Simplified and Improved Separations Between Regular and General Resolution by Lifting
title_short Simplified and Improved Separations Between Regular and General Resolution by Lifting
title_sort simplified and improved separations between regular and general resolution by lifting
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326554/
http://dx.doi.org/10.1007/978-3-030-51825-7_14
work_keys_str_mv AT vinyalsmarc simplifiedandimprovedseparationsbetweenregularandgeneralresolutionbylifting
AT elffersjan simplifiedandimprovedseparationsbetweenregularandgeneralresolutionbylifting
AT johannsenjan simplifiedandimprovedseparationsbetweenregularandgeneralresolutionbylifting
AT nordstromjakob simplifiedandimprovedseparationsbetweenregularandgeneralresolutionbylifting

Ejemplares similares