CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS
We consider sets ${\it\Gamma}(n,s,k)$ of narrow clauses expressing that no definition of a size $s$ circ...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Cambridge University Press
2016-01-01
|
| Series: | Forum of Mathematics, Sigma |
| Subjects: | |
| Online Access: | https://www.cambridge.org/core/product/identifier/S205050941600013X/type/journal_article |
| _version_ | 1811156243990970368 |
|---|---|
| author | JAN KRAJÍČEK |
| author_facet | JAN KRAJÍČEK |
| author_sort | JAN KRAJÍČEK |
| collection | DOAJ |
| description | We consider sets
${\it\Gamma}(n,s,k)$
of narrow clauses expressing that no definition of a size
$s$
circuit with
$n$
inputs is refutable in resolution R in
$k$
steps. We show that every CNF with a short refutation in extended R, ER, can be easily reduced to an instance of
${\it\Gamma}(0,s,k)$
(with
$s,k$
depending on the size of the ER-refutation) and, in particular, that
${\it\Gamma}(0,s,k)$
when interpreted as a relativized NP search problem is complete among all such problems provably total in bounded arithmetic theory
$V_{1}^{1}$
. We use the ideas of implicit proofs from Krajíček [J. Symbolic Logic, 69 (2) (2004), 387–397; J. Symbolic Logic, 70 (2) (2005), 619–630] to define from
${\it\Gamma}(0,s,k)$
a nonrelativized NP search problem
$i{\it\Gamma}$
and we show that it is complete among all such problems provably total in bounded arithmetic theory
$V_{2}^{1}$
. The reductions are definable in theory
$S_{2}^{1}$
. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them. |
| first_indexed | 2024-04-10T04:47:18Z |
| format | Article |
| id | doaj.art-88c982446e66453c8e53209fb6f0b4c6 |
| institution | Directory Open Access Journal |
| issn | 2050-5094 |
| language | English |
| last_indexed | 2024-04-10T04:47:18Z |
| publishDate | 2016-01-01 |
| publisher | Cambridge University Press |
| record_format | Article |
| series | Forum of Mathematics, Sigma |
| spelling | doaj.art-88c982446e66453c8e53209fb6f0b4c62023-03-09T12:34:41ZengCambridge University PressForum of Mathematics, Sigma2050-50942016-01-01410.1017/fms.2016.13CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMSJAN KRAJÍČEK0Faculty of Mathematics and Physics, Charles University in Prague, Czech Republic;We consider sets ${\it\Gamma}(n,s,k)$ of narrow clauses expressing that no definition of a size $s$ circuit with $n$ inputs is refutable in resolution R in $k$ steps. We show that every CNF with a short refutation in extended R, ER, can be easily reduced to an instance of ${\it\Gamma}(0,s,k)$ (with $s,k$ depending on the size of the ER-refutation) and, in particular, that ${\it\Gamma}(0,s,k)$ when interpreted as a relativized NP search problem is complete among all such problems provably total in bounded arithmetic theory $V_{1}^{1}$ . We use the ideas of implicit proofs from Krajíček [J. Symbolic Logic, 69 (2) (2004), 387–397; J. Symbolic Logic, 70 (2) (2005), 619–630] to define from ${\it\Gamma}(0,s,k)$ a nonrelativized NP search problem $i{\it\Gamma}$ and we show that it is complete among all such problems provably total in bounded arithmetic theory $V_{2}^{1}$ . The reductions are definable in theory $S_{2}^{1}$ . We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them.https://www.cambridge.org/core/product/identifier/S205050941600013X/type/journal_article03F20 (primary)68Q15 (secondary) |
| spellingShingle | JAN KRAJÍČEK CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS Forum of Mathematics, Sigma 03F20 (primary) 68Q15 (secondary) |
| title | CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS |
| title_full | CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS |
| title_fullStr | CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS |
| title_full_unstemmed | CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS |
| title_short | CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS |
| title_sort | consistency of circuit evaluation extended resolution and total np search problems |
| topic | 03F20 (primary) 68Q15 (secondary) |
| url | https://www.cambridge.org/core/product/identifier/S205050941600013X/type/journal_article |
| work_keys_str_mv | AT jankrajicek consistencyofcircuitevaluationextendedresolutionandtotalnpsearchproblems |