Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
428886 | Information Processing Letters | 2007 | 5 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics