Sciweavers

IPL
2007

Substitutions into propositional tautologies

13 years 3 months ago
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(...
Jan Krajícek
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where IPL
Authors Jan Krajícek
Comments (0)