License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2010.2475
URN: urn:nbn:de:0030-drops-24753
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2475/
Go to the corresponding LIPIcs Volume Portal

Hirsch, Edward A. ; Itsykson, Dmitry

On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity

pdf-format:
1001.HirschEdward.2475.pdf (0.3 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{hirsch_et_al:LIPIcs:2010:2475,
  author =	{Edward A. Hirsch and Dmitry Itsykson},
  title =	{{On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{453--464},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Jean-Yves Marion and Thomas Schwentick},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2475},
  URN =		{urn:nbn:de:0030-drops-24753},
  doi =		{10.4230/LIPIcs.STACS.2010.2475},
  annote =	{Keywords: Propositional proof complexity, optimal algorithm}
}

Keywords: Propositional proof complexity, optimal algorithm
Collection: 27th International Symposium on Theoretical Aspects of Computer Science
Issue Date: 2010
Date of publication: 09.03.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI