Direkt zum Inhalt

Is the Standard Proof System for SAT P-optimal?

Johannes Köbler and Jochen Messner

Abstract:

We investigate the question whether there is a (p-)optimal proof system for SAT or for TAUT and its relation to completeness and collapse results for nondeterministic function classes. A p-optimal proof system for SAT is shown to imply (1) that there exists a complete function for the class of all total nondeterministic multi-valued functions and (2) that any set with an optimal proof system has a p-optimal proof system. By replacing the assumption of the mere existence of a (p)optimal proof system by the assumption that certain proof systems are (p-)optimal we obtain stronger consequences, namely collapse results for various function classes. Especially we investigate the question whether the standard proof system for SAT is p-optimal. We show that this assumption is equivalent to a variety of complexity theoretical assertions studied before, and to the assumption that every optimal proof system is p-optimal. Finally, we investigate whether there is an optimal proof system for TAUT that admits an effective interpolation, and show some relations between various completeness assumptions.

Ps-File: Is the Standard Proof System for SAT P-optimal?
zuletzt geändert: 31.10.05 SK
Document Actions
Persönliche Werkzeuge
« August 2008 »
Mo Di Mi Do Fr Sa So
        1 2 3
4 5 6 7 8 9 10
11 12 13 14 15 16 17
18 19 20 21 22 23 24
25 26 27 28 29 30 31