Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Simplified and Improved Separations Between Regular and General Resolution by Lifting

Vinyals, Marc ; Elffers, Jan LU ; Johannsen, Jan and Nordström, Jakob LU (2020) 23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020 In Lecture Notes in Computer Science 12178. p.182-200
Abstract

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.

Please use this url to cite or link to this publication:
author
; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Theory and Applications of Satisfiability Testing – SAT 2020 : 23rd International Conference, Proceedings - 23rd International Conference, Proceedings
series title
Lecture Notes in Computer Science
editor
Pulina, Luca and Seidl, Martina
volume
12178
pages
19 pages
publisher
Springer
conference name
23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020
conference location
Virtual, Online
conference dates
2020-07-03 - 2020-07-10
external identifiers
  • scopus:85088278995
ISSN
1611-3349
0302-9743
ISBN
9783030518240
9783030518257
DOI
10.1007/978-3-030-51825-7_14
language
English
LU publication?
yes
id
c273df6c-78a1-4518-a0b7-809297e4f965
date added to LUP
2020-12-18 22:14:25
date last changed
2025-01-11 01:18:14
@inproceedings{c273df6c-78a1-4518-a0b7-809297e4f965,
  abstract     = {{<p>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.</p>}},
  author       = {{Vinyals, Marc and Elffers, Jan and Johannsen, Jan and Nordström, Jakob}},
  booktitle    = {{Theory and Applications of Satisfiability Testing – SAT 2020 : 23rd International Conference, Proceedings}},
  editor       = {{Pulina, Luca and Seidl, Martina}},
  isbn         = {{9783030518240}},
  issn         = {{1611-3349}},
  language     = {{eng}},
  pages        = {{182--200}},
  publisher    = {{Springer}},
  series       = {{Lecture Notes in Computer Science}},
  title        = {{Simplified and Improved Separations Between Regular and General Resolution by Lifting}},
  url          = {{http://dx.doi.org/10.1007/978-3-030-51825-7_14}},
  doi          = {{10.1007/978-3-030-51825-7_14}},
  volume       = {{12178}},
  year         = {{2020}},
}