Abstract:
The notion of an optimal acceptor for TAUT (the optimality property is stated only for input strings from TAUT) comes from the line of research aimed at resolving the question of whether optimal propositional proof systems exist. In this paper we introduce two new types of optimal acceptors, a D-N-optimal acceptor and an N-D-optimal acceptor for TAUT. A deterministic algorithm recognizing TAUT is a D-N-optimal acceptor if no other nondeterministic algorithm accepting TAUT has more than a polynomial speed-up over its running time on instances from TAUT. We further develop the earlier observed connection between optimal acceptors, optimal propositional proof systems, and the structure of easy subsets of TAUT. Namely, we prove that the existence of a D-N-optimal acceptor for TAUT is equivalent to the existence of an optimal and automatizable propositional proof system and to the existence of a suitable recursive presentation of the class of all NP-easy (acceptable by nondeterministic polynomial time machines) subsets of TAUT. Additionally, we show that the question of whether every proof system is weakly automatizable is equivalent to the question of whether every disjoint NP-pair is P-separable.