License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITCS.2023.101
URN: urn:nbn:de:0030-drops-176043
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17604/
Yolcu, Emre ;
Heule, Marijn J. H.
Exponential Separations Using Guarded Extension Variables
Abstract
We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula Γ in conjunctive normal form, deriving clauses that are not necessarily logically implied by Γ but whose addition to Γ preserves satisfiability. When the derived clauses are allowed to introduce variables not occurring in Γ, the systems we consider become equivalent to extended resolution. We are concerned with the versions of these systems without new variables. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution. Each of these systems formalizes some restricted version of the ability to make assumptions that hold "without loss of generality," which is commonly used informally to simplify or shorten proofs.
Except for SBC⁻, these systems are known to be exponentially weaker than extended resolution. They are, however, all equivalent to it under a relaxed notion of simulation that allows the translation of the formula along with the proof when moving between proof systems. By taking advantage of this fact, we construct formulas that separate RAT⁻ from GER⁻ and vice versa. With the same strategy, we also separate SBC⁻ from RAT⁻. Additionally, we give polynomial-size SBC⁻ proofs of the pigeonhole principle, which separates SBC⁻ from GER⁻ by a previously known lower bound. These results also separate the three systems from BC⁻ since they all simulate it. We thus give an almost complete picture of their relative strengths.
BibTeX - Entry
@InProceedings{yolcu_et_al:LIPIcs.ITCS.2023.101,
author = {Yolcu, Emre and Heule, Marijn J. H.},
title = {{Exponential Separations Using Guarded Extension Variables}},
booktitle = {14th Innovations in Theoretical Computer Science Conference (ITCS 2023)},
pages = {101:1--101:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-263-1},
ISSN = {1868-8969},
year = {2023},
volume = {251},
editor = {Tauman Kalai, Yael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17604},
URN = {urn:nbn:de:0030-drops-176043},
doi = {10.4230/LIPIcs.ITCS.2023.101},
annote = {Keywords: proof complexity, separations, resolution, extended resolution, blocked clauses}
}
|
Keywords: |
|
proof complexity, separations, resolution, extended resolution, blocked clauses |
|
Collection: |
|
14th Innovations in Theoretical Computer Science Conference (ITCS 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
01.02.2023 |
