The Power of Negative Reasoning

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

The Power of Negative Reasoning. / de Rezende, Susanna F.; Lauria, Massimo; Nordström, Jakob; Sokolov, Dmitry.

36th Computational Complexity Conference, CCC 2021. ed. / Valentine Kabanets. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. 40 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 200).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

de Rezende, SF, Lauria, M, Nordström, J & Sokolov, D 2021, The Power of Negative Reasoning. in V Kabanets (ed.), 36th Computational Complexity Conference, CCC 2021., 40, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics, LIPIcs, vol. 200, 36th Computational Complexity Conference, CCC 2021, Virtual, Toronto, Canada, 20/07/2021. https://doi.org/10.4230/LIPIcs.CCC.2021.40

APA

de Rezende, S. F., Lauria, M., Nordström, J., & Sokolov, D. (2021). The Power of Negative Reasoning. In V. Kabanets (Ed.), 36th Computational Complexity Conference, CCC 2021 [40] Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Leibniz International Proceedings in Informatics, LIPIcs Vol. 200 https://doi.org/10.4230/LIPIcs.CCC.2021.40

Vancouver

de Rezende SF, Lauria M, Nordström J, Sokolov D. The Power of Negative Reasoning. In Kabanets V, editor, 36th Computational Complexity Conference, CCC 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2021. 40. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 200). https://doi.org/10.4230/LIPIcs.CCC.2021.40

Author

de Rezende, Susanna F. ; Lauria, Massimo ; Nordström, Jakob ; Sokolov, Dmitry. / The Power of Negative Reasoning. 36th Computational Complexity Conference, CCC 2021. editor / Valentine Kabanets. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 200).

Bibtex

@inproceedings{197fed6470264a24a69cf653039fb41e,
title = "The Power of Negative Reasoning",
abstract = "Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gr{\"o}bner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.",
keywords = "Nullstellensatz, Polynomial calculus, Proof complexity, Sherali-Adams, Sums-of-squares",
author = "{de Rezende}, {Susanna F.} and Massimo Lauria and Jakob Nordstr{\"o}m and Dmitry Sokolov",
note = "Publisher Copyright: {\textcopyright} Susanna F. de Rezende, Massimo Lauria, Jakob Nordstr{\"o}m, and Dmitry Sokolov;; 36th Computational Complexity Conference, CCC 2021 ; Conference date: 20-07-2021 Through 23-07-2021",
year = "2021",
doi = "10.4230/LIPIcs.CCC.2021.40",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
editor = "Valentine Kabanets",
booktitle = "36th Computational Complexity Conference, CCC 2021",

}

RIS

TY - GEN

T1 - The Power of Negative Reasoning

AU - de Rezende, Susanna F.

AU - Lauria, Massimo

AU - Nordström, Jakob

AU - Sokolov, Dmitry

N1 - Publisher Copyright: © Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov;

PY - 2021

Y1 - 2021

N2 - Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.

AB - Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.

KW - Nullstellensatz

KW - Polynomial calculus

KW - Proof complexity

KW - Sherali-Adams

KW - Sums-of-squares

U2 - 10.4230/LIPIcs.CCC.2021.40

DO - 10.4230/LIPIcs.CCC.2021.40

M3 - Article in proceedings

AN - SCOPUS:85115341992

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 36th Computational Complexity Conference, CCC 2021

A2 - Kabanets, Valentine

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 36th Computational Complexity Conference, CCC 2021

Y2 - 20 July 2021 through 23 July 2021

ER -

ID: 306898812