We present a novel third-order theory W(1)(1) of bounded arithmetic suitable for reasoning about PSPACE functions. This theory has the advantages of avoiding the smash function symbol and is otherwise much simpler tha...
详细信息
ISBN:
(纸本)3540230246
We present a novel third-order theory W(1)(1) of bounded arithmetic suitable for reasoning about PSPACE functions. This theory has the advantages of avoiding the smash function symbol and is otherwise much simpler than previous PSPACE theories. As an example we outline a proof in W(1)(1) that from any configuration in the game of Hex, at least one player has a winning strategy. We then exhibit a translation of theorems of W(1)(1) into families of propositional tautologies with polynomial-size proofs in BPLK (a recent propositionalproof system for PSPACE and an alternative to G). This translation is clearer and more natural in several respects than the analogous ones for previous PSPACE theories.
We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of emph{resolution}. This program build...
详细信息
We explore the relationships between the computational problem of recognizing expander graphs, and the problem of efficiently approximating proof length in the well-known system of emph{resolution}. This program builds upon known connections between graph expansion and resolution lower bounds.A proof system $P$ is emph{(quasi-)automatizable} if there is a search algorithm which finds a $P$-proof of a given formula $f$ in time (quasi)polynomial in the length of a shortest $P$-proof of $f$. It is open whether resolution is (quasi-)automatizable. We prove several conditional non-automatizability results for resolution modulo new conjectures concerning the complexity of identifying bipartite expander graphs. Our reductions use a natural family of formulas and exploit the well-known relationships between expansion and length of resolution proofs. Our hardness assumptions are unsupported; we survey known results as progress towards establishing their plausibility. The major contribution is a conditional hardness result for the quasi-automatizability of resolution
Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there is no regularity condition. For regul...
详细信息
Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there is no regularity condition. For regular proofs, an exponential separation between regular dag-like resolution and both regular WRTL and regular WRTI is given. It is proved that DLL proof search algorithms that use clause learning based on unit propagation can be polynomially simulated by regular WRTI. More generally, non-greedy DLL algorithms with learning by unit propagation are equivalent to regular WRTI. A general form of clause learning, called DLL-Learn, is defined that is equivalent to regular WRTL. A variable extension method is used to give simulations of resolution by regular WRTI, using a simplified form of proof trace extensions. DLL-Learn and non-greedy DLL algorithms with learning by unit propagation can use variable extensions to simulate general resolution without doing restarts. Finally, an exponential lower bound for WRTL where the lemmas are restricted to short clauses is shown.
We prove a limitation on a variant of the KPT theorem proposed for propositionalproof systems by Pich and Santhanam [7], for all proof systems that prove the disjointness of two NP sets that are hard to distinguish.
We prove a limitation on a variant of the KPT theorem proposed for propositionalproof systems by Pich and Santhanam [7], for all proof systems that prove the disjointness of two NP sets that are hard to distinguish.
暂无评论