Is the Standard Proof System for SAT P-optimal?

Johannes Koebler, Jochen Messner

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


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 the question whether there is an optimal proof system for TAUT that has the effective interpolation property, and show some relations between various completeness assumptions.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Start Conference Manager
Conference Systems