10.4230/LIPICS.STACS.2010.2475
Hirsch, Edward A.
Edward A.
Hirsch
Itsykson, Dmitry
Dmitry
Itsykson
On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Propositional proof complexity
optimal algorithm
Marion, Jean-Yves
Jean-Yves
Marion
Schwentick, Thomas
Thomas
Schwentick
2010
2010-03-09
2010-03-09
2010-03-09
en
urn:nbn:de:0030-drops-24753
10.4230/LIPIcs.STACS.2010
978-3-939897-16-3
1868-8969
10.4230/LIPIcs.STACS.2010
LIPIcs, Volume 5, STACS 2010
27th International Symposium on Theoretical Aspects of Computer Science
2013
5
40
453
464
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Marion, Jean-Yves
Jean-Yves
Marion
Schwentick, Thomas
Thomas
Schwentick
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
5
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
293979 bytes
application/pdf
Creative Commons Attribution-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
The existence of a ($p$-)optimal propositional proof system is a major open question in (proof) complexity; many people conjecture that such systems do not exist. Kraj\'{\i}\v{c}ek and Pudl\'{a}k \cite{KP} show that this question is equivalent to the existence of an algorithm that is optimal\footnote{Recent papers \cite{Monroe}
call such algorithms \emph{$p$-optimal} while traditionally Levin's algorithm was called \emph{optimal}. We follow the older tradition. Also there is some mess in terminology here, thus please see formal definitions in Sect.~\ref{sec:prelim} below.} on all propositional tautologies. Monroe \cite{Monroe} recently gave a conjecture implying that such algorithm does not exist.
We show that in the presence of errors such optimal algorithms \emph{do} exist. The concept is motivated by the notion of heuristic algorithms. Namely, we allow the algorithm to claim a small number of false ``theorems'' (according to any polynomial-time samplable distribution on non-tautologies) and err with bounded probability on other inputs.
Our result can also be viewed as the existence of an optimal proof system in a class of proof systems obtained by generalizing automatizable proof systems.
LIPIcs, Vol. 5, 27th International Symposium on Theoretical Aspects of Computer Science, pages 453-464