Substitutions into propositional tautologies

We prove that there is a polynomial time substitution (y1, . . . , yn) := g(x1, . . . , xk) with k << n such that whenever the substitution instance A(g(x1, . . . , xk)) of a 3DNF formula A(y1, . . . , yn) has a short resolution proof it follows that A(y1, . . . , yn) is a tautology. The qualification “short” depends on the parameters k and n. Let A(y) be a 3DNF propositional formula in n variables y = (y1, . . . , yn) and assume that we want to prove that A(y) is a tautology. By substituting y := g(x) with x = (x1, . . . , xk) we get formula A(g(x)) which is, as long as g is computable in (non-uniform) time nO(1), expressible as 3DNF of size nO(1). The formula uses nO(1) auxiliary variables z besides variables x but only x are essential: We know apriori (and can witness by a polynomial time constructible resolution proof) that any truth assignment satisfying ¬A(g(x1, . . . , xk)) would be determined already by its values at x1, . . . , xk. If A(y) is a tautology, so is A(...

• Type: Journal
• Year: 2007
• Where: IPL
• Authors: Jan Krajícek
• Keywords: IPL 2007, Polynomial Time Substitution, Short Resolution Proof, Substitution Instance