Provably total functions in the polynomial hierarchy
Fleming, Noah LU
; Imrek, Deniz
and Marciot, Christophe
LU
(2025)
In LIPIcs
339.
p.1-40
- Abstract
- TFNP studies the complexity of total, verifiable search problems, and represents the first layer of the total function polynomial hierarchy (TFPH). Recently, problems in higher levels of the TFPH have gained significant attention, partly due to their close connection to circuit lower bounds. However, very little is known about the relationships between problems in levels of the hierarchy beyond TFNP. Connections to proof complexity have had an outsized impact on our understanding of the relationships between subclasses of TFNP in the black-box model. Subclasses are characterized by provability in certain proof systems, which has allowed for tools from proof complexity to be applied in order to separate TFNP problems. In this work we begin... (More)
- TFNP studies the complexity of total, verifiable search problems, and represents the first layer of the total function polynomial hierarchy (TFPH). Recently, problems in higher levels of the TFPH have gained significant attention, partly due to their close connection to circuit lower bounds. However, very little is known about the relationships between problems in levels of the hierarchy beyond TFNP. Connections to proof complexity have had an outsized impact on our understanding of the relationships between subclasses of TFNP in the black-box model. Subclasses are characterized by provability in certain proof systems, which has allowed for tools from proof complexity to be applied in order to separate TFNP problems. In this work we begin a systematic study of the relationship between subclasses of total search problems in the polynomial hierarchy and proof systems. We show that, akin to TFNP, reductions to a problem in TFΣ_d are equivalent to proofs of the formulas expressing the totality of the problems in some Σ_d-proof system. Having established this general correspondence, we examine important subclasses of TFPH. We show that reductions to the StrongAvoid problem are equivalent to proofs in a Σ₂-variant of the (unary) Sherali-Adams proof system. As well, we explore the TFPH classes which result from well-studied proof systems, introducing a number of new TFΣ₂ classes which characterize variants of DNF resolution, as well as TFΣ_d classes capturing levels of Σ_d-bounded-depth Frege. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/296eb2eb-3996-4db0-91ce-2484b8e18d56
- author
- Fleming, Noah
LU
; Imrek, Deniz
and Marciot, Christophe
LU
- publishing date
- 2025
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- 40th Computational Complexity Conference (CCC 2025)
- series title
- LIPIcs
- volume
- 339
- pages
- 40 pages
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- external identifiers
-
- scopus:105012176243
- ISBN
- 978-3-95977-379-9
- DOI
- 10.4230/LIPIcs.CCC.2025.28
- language
- English
- LU publication?
- no
- id
- 296eb2eb-3996-4db0-91ce-2484b8e18d56
- date added to LUP
- 2025-11-05 15:34:53
- date last changed
- 2026-07-15 04:46:20
@inproceedings{296eb2eb-3996-4db0-91ce-2484b8e18d56,
abstract = {{TFNP studies the complexity of total, verifiable search problems, and represents the first layer of the total function polynomial hierarchy (TFPH). Recently, problems in higher levels of the TFPH have gained significant attention, partly due to their close connection to circuit lower bounds. However, very little is known about the relationships between problems in levels of the hierarchy beyond TFNP. Connections to proof complexity have had an outsized impact on our understanding of the relationships between subclasses of TFNP in the black-box model. Subclasses are characterized by provability in certain proof systems, which has allowed for tools from proof complexity to be applied in order to separate TFNP problems. In this work we begin a systematic study of the relationship between subclasses of total search problems in the polynomial hierarchy and proof systems. We show that, akin to TFNP, reductions to a problem in TFΣ_d are equivalent to proofs of the formulas expressing the totality of the problems in some Σ_d-proof system. Having established this general correspondence, we examine important subclasses of TFPH. We show that reductions to the StrongAvoid problem are equivalent to proofs in a Σ₂-variant of the (unary) Sherali-Adams proof system. As well, we explore the TFPH classes which result from well-studied proof systems, introducing a number of new TFΣ₂ classes which characterize variants of DNF resolution, as well as TFΣ_d classes capturing levels of Σ_d-bounded-depth Frege.}},
author = {{Fleming, Noah and Imrek, Deniz and Marciot, Christophe}},
booktitle = {{40th Computational Complexity Conference (CCC 2025)}},
isbn = {{978-3-95977-379-9}},
language = {{eng}},
pages = {{1--40}},
publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
series = {{LIPIcs}},
title = {{Provably total functions in the polynomial hierarchy}},
url = {{https://lup.lub.lu.se/search/files/253290625/TFPH.pdf}},
doi = {{10.4230/LIPIcs.CCC.2025.28}},
volume = {{339}},
year = {{2025}},
}