Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR09-014 | 7th February 2009 00:00

On the asymptotic Nullstellensatz and Polynomial Calculus proof complexity


Authors: Soren Riis
Publication: 27th February 2009 04:33
Downloads: 1172


We show that the asymptotic complexity of uniformly generated (expressible in First-Order (FO) logic) propositional tautologies for the Nullstellensatz proof system (NS) as well as for Polynomial Calculus, (PC) has four distinct types of asymptotic behavior over fields of finite characteristic. More precisely, based on some highly non-trivial work by Krajicek, we show that for each prime $p$ there exists a function $l(n) \in \Omega(\log(n))$ for NS and
$l(n) \in \Omega(\log(\log(n))$ for PC, such that the propositional translation of any FO formula (that fails in all finite models), has degree proof complexity over fields of characteristic $p$, that behave in $4$ mutually distinct ways:

(i) The degree complexity is bound by a constant.

(ii) The degree complexity is at least $l(n)$ for all values of $n$.

(iii) The degree complexity is at least $l(n)$ except in a finite number of regular subsequences of inifinite size, where the degree is constant.

(iv) The degree complexity fluctuates between constant and $l(n)$ (and possibly beyond) in a very particular way.

We leave it as an open question whether the classification remains valid for $l(n) \in n^{\Omega(1)}$ or even for $l(n) \in \Omega(n)$.
Finally, we show that for any non-empty proper subset
$A \subseteq \{ (i), (ii), (iii), (iv)\}$ the decision problem of whether a given input FO formula $\psi$ has type belonging to $A$ - is undecidable.

ISSN 1433-8092 | Imprint