Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR23-068 | 18th July 2023 14:14

Colourful TFNP and Propositional Proofs

RSS-Feed




Revision #1
Authors: Ben Davis, Robert Robere
Accepted on: 18th July 2023 14:14
Downloads: 186
Keywords: 


Abstract:

Recent work has shown that many of the standard TFNP classes — such as PLS, PPADS, PPAD, SOPL, and EOPL — have corresponding proof systems in propositional proof complexity, in the sense that a total search problem is in the class if and only if the totality of the problem can be efficiently proved by the corresponding proof system. We build on this line of work by studying coloured variants of these TFNP classes: C-PLS, C-PPADS, C-PPAD, C-SOPL, and C-EOPL. While C-PLS has been studied in the literature before, the coloured variants of the other classes are introduced here for the first time. We give a family of results showing that these coloured TFNP classes are natural objects of study, and that the correspondence between TFNP and natural propositional proof systems is not an exceptional phenomenon isolated to weak TFNP classes. Namely, we show that:

- Each of the classes C-PLS, C-PPADS, and C-SOPL have corresponding proof systems characterizing them. Specifically, the proof systems for these classes are obtained by adding depth to the formulas in the corresponding proof system for the uncoloured class. For instance, while it was previously known that PLS is characterized by bounded-width Res- olution (i.e. depth 0.5 Frege), we prove that C-PLS is characterized by depth-1.5 Frege (Res(polylog(n))).

- The classes C-PPAD and C-EOPL coincide exactly with the uncoloured classes PPADS and SOPL, respectively. Thus, both of these classes also have corresponding proof systems: unary Sherali-Adams and Reversible Resolution, respectively.

- Finally, we prove a coloured intersection theorem for the coloured sink classes, showing C-PLS $\cap$ C-PPADS = C-SOPL, generalizing the intersection theorem PLS $\cap$ PPADS = SOPL. However, while it is known in the uncoloured world that PLS $\cap$ PPAD = EOPL = CLS, we prove that this equality fails in the coloured world in the black-box setting. More precisely, we show that there is an oracle O relative to which C-PLS $\cap$ C-PPAD $\neq$ C-EOPL.

To prove our results, we introduce an abstract multivalued proof system — the Blockwise Calculus — which may be of independent interest.



Changes to previous version:

Corrected notation error in proof of coloured intersection


Paper:

TR23-068 | 10th May 2023 20:13

Colourful TFNP and Propositional Proofs





TR23-068
Authors: Ben Davis, Robert Robere
Publication: 11th May 2023 17:19
Downloads: 409
Keywords: 


Abstract:

Recent work has shown that many of the standard TFNP classes — such as PLS, PPADS, PPAD, SOPL, and EOPL — have corresponding proof systems in propositional proof complexity, in the sense that a total search problem is in the class if and only if the totality of the problem can be efficiently proved by the corresponding proof system. We build on this line of work by studying coloured variants of these TFNP classes: C-PLS, C-PPADS, C-PPAD, C-SOPL, and C-EOPL. While C-PLS has been studied in the literature before, the coloured variants of the other classes are introduced here for the first time. We give a family of results showing that these coloured TFNP classes are natural objects of study, and that the correspondence between TFNP and natural propositional proof systems is not an exceptional phenomenon isolated to weak TFNP classes. Namely, we show that:

- Each of the classes C-PLS, C-PPADS, and C-SOPL have corresponding proof systems characterizing them. Specifically, the proof systems for these classes are obtained by adding depth to the formulas in the corresponding proof system for the uncoloured class. For instance, while it was previously known that PLS is characterized by bounded-width Res- olution (i.e. depth 0.5 Frege), we prove that C-PLS is characterized by depth-1.5 Frege (Res(polylog(n))).

- The classes C-PPAD and C-EOPL coincide exactly with the uncoloured classes PPADS and SOPL, respectively. Thus, both of these classes also have corresponding proof systems: unary Sherali-Adams and Reversible Resolution, respectively.

- Finally, we prove a coloured intersection theorem for the coloured sink classes, showing C-PLS?C-PPADS = C-SOPL, generalizing the intersection theorem PLS?PPADS = SOPL. However, while it is known in the uncoloured world that PLS ? PPAD = EOPL = CLS, we prove that this equality fails in the coloured world in the black-box setting. More precisely, we show that there is an oracle O relative to which C-PLS ? C-PPAD $\neq$ C-EOPL.

To prove our results, we introduce an abstract multivalued proof system — the Blockwise Calculus — which may be of independent interest.



ISSN 1433-8092 | Imprint