Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

Tuomas Hakoniemi; Nutan Limaye; Iddo Tzameret

doi:10.1145/3618260.3649616

Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

Tuomas Hakoniemi
, Nutan Limaye
, Iddo Tzameret

Algorithms

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi ‍[J. ‍ACM, 65(6):37:1–55, 2018]) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson ‍[Theory ‍Comput., 17: 1-88, 2021]), which reduces the hardness of refuting a polynomial equation f(x)=0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method.

Original language	English
Title of host publication	Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers
Number of pages	8
Place of Publication	New York
Publisher	Association for Computing Machinery
Publication date	11 Jun 2024
Pages	1396 - 1404
ISBN (Print)	979-8-4007-0383-6
DOIs	https://doi.org/10.1145/3618260.3649616
Publication status	Published - 11 Jun 2024
Event	ACM Symposium on Theory of Computing - Vancouver, Canada Duration: 24 Jun 2024 → 28 Jun 2024 Conference number: 56

Conference

Conference	ACM Symposium on Theory of Computing
Number	56
Country/Territory	Canada
City	Vancouver
Period	24/06/2024 → 28/06/2024

Keywords

ideal proof system
proof complexity
functional lower bound method
algebraic circuits
boolean cube

Access to Document

10.1145/3618260.3649616

Cite this

@inproceedings{ceef471ce97e468890ca1b68427d2545,

title = "Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers",

abstract = "Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi ‍[J. ‍ACM, 65(6):37:1–55, 2018]) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson ‍[Theory ‍Comput., 17: 1-88, 2021]), which reduces the hardness of refuting a polynomial equation f(x)=0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method.",

keywords = "ideal proof system, proof complexity, functional lower bound method, algebraic circuits, boolean cube",

author = "Tuomas Hakoniemi and Nutan Limaye and Iddo Tzameret",

year = "2024",

month = jun,

day = "11",

doi = "10.1145/3618260.3649616",

language = "English",

isbn = "979-8-4007-0383-6",

pages = "1396 -- 1404",

booktitle = "Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers",

publisher = "Association for Computing Machinery",

address = "United States",

note = "ACM Symposium on Theory of Computing, STOC 2024 ; Conference date: 24-06-2024 Through 28-06-2024",

}

Hakoniemi, T, Limaye, N & Tzameret, I 2024, Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers. in Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers. Association for Computing Machinery, New York, pp. 1396 - 1404, ACM Symposium on Theory of Computing, Vancouver, British Columbia, Canada, 24/06/2024. https://doi.org/10.1145/3618260.3649616

Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers. / Hakoniemi, Tuomas; Limaye, Nutan; Tzameret, Iddo.
Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers. New York: Association for Computing Machinery, 2024. p. 1396 - 1404.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

AU - Hakoniemi, Tuomas

AU - Limaye, Nutan

AU - Tzameret, Iddo

N1 - Conference code: 56

PY - 2024/6/11

Y1 - 2024/6/11

N2 - Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi ‍[J. ‍ACM, 65(6):37:1–55, 2018]) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson ‍[Theory ‍Comput., 17: 1-88, 2021]), which reduces the hardness of refuting a polynomial equation f(x)=0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method.

AB - Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi ‍[J. ‍ACM, 65(6):37:1–55, 2018]) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson ‍[Theory ‍Comput., 17: 1-88, 2021]), which reduces the hardness of refuting a polynomial equation f(x)=0 with no Boolean solutions to the hardness of computing the function 1/f(x) over the Boolean cube with an algebraic circuit. Using symmetry we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method.

KW - ideal proof system

KW - proof complexity

KW - functional lower bound method

KW - algebraic circuits

KW - boolean cube

U2 - 10.1145/3618260.3649616

DO - 10.1145/3618260.3649616

M3 - Article in proceedings

SN - 979-8-4007-0383-6

SP - 1396

EP - 1404

BT - Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

PB - Association for Computing Machinery

CY - New York

T2 - ACM Symposium on Theory of Computing

Y2 - 24 June 2024 through 28 June 2024

ER -

Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this