Transcript 20060411153016001

Sporadic Propositional Proofs
Søren Riis
Queen mary,
University of London
New Directions in Proof Complexity
11th of April 2006 at the Newton Instutute Cambridge
General question:
For a given (weak) Propositional Proof System
investigate the proof complexity (as a function
of n) of uniform sequences [η]n of tautologies.
Setup for this: Given a large class C of
propositions from predicate logic. Each
proposition η Є C defines a sequence of
propositions [η]n where [η]n is a propositional
formula expressing that there is no model of η of
size n
Uniform sequences of Tautologies
• Often uniform sequences of proposition
formulae are usually produced by the
Paris-Wilkie translation.
• For many nice theorems in weak
propositional proof complexity we need a
slightly different translation (the RiisSitharam or RS-translation).
Difference between the PW and RS
translations in a nutshell
In the PW-translation [A] of A:=Ez z+z=n Λ φ
becomes equivalent to 0 if n is odd and [φ] if n is even.
In the RS-translation all function and relation symbols are
treated as uninterpreted symbols.
(i.e. +, ≤, * etc are treated as general uninterpreted
relation symbols). This ensure that the translation [A]n
(essentially) becomes closed under the action of the
symmetric group.
,
Idea
For a given (weak) Propositional Proof System P
classify the proof complexity behaviour of [η]n
for a given class C of formulae η of predicate
logic.
Let cP(n) denote the length of the shortest proof
of [η]n.
Question: Which complexity functions cP(n) can
occur?
Tree resolution proofs
Theorem [Riis 99]:
The class of complexity functions Ctr (n) is
included in the set of all functions that
either are bounded by a fixed polynomial
or has growth rate faster than 2cn for some
c>0.
Tree resolution proofs
Conjecture [With Danchev]:
The class of complexity functions C(n) has in three distinct types of
behaviour:
(1) C(n) with C(n)<p(n) for some polynomial p.
(2) C(n) for which there exists 0<c<d such that 2cn <C(n) < 2dn for all but
finitely many values of n.
(3) C(n)>2cn log(n) for some constant c>0.
New type of problem: In case (1) is C(n) given by a
polynomial (for all but finitely many exceptional values of
n)?
Resolution proofs (Hilbert style)
Theorem [Dantchev, Riis 03]:
The class of complexity functions Cres (n)
that arise from “relativised first order
formula” is included in the class of
functions that either are polynomial
bounded or has growth rate faster than
2cn for some c>0.
Resolution proofs (Hilbert style)
Conjecture [With Dantchev]
The class of complexity functions Cres (n)
includes all functions that either are
polynomially bounded or has growth rate
faster than 2cn for some c>0.
New results
Let [η]n be a uniform sequence of
propositional formula.
Let Strue :={n : [η]n is true}
Let Sfalse :={n : [η]n is false}.
Here n denote (as usual) the size of the
underlying model.
BDF proofs
Theorem A:
If Sfalse and Strue both are infinite there
exists an infinite subset N’ in Strue such
that the sequence [η]n for any constant d,
and for any infinite N’’ subset of N’
requires exponential size depth d FregeProofs.
BDF proofs
Theorem B:
Assume Sfalse ={s1,s2,s3,…,sn,…} is not
very sparse (for each c >0 we have
(sk+1-sk)c<sk for infinitely many values of
k).
Then for any d Є {1,2,…} [η]n requires
exponential size depth d Frege-Proofs (on
any infinite subset N’ of Strue)
Corollaries:
The propositional version of each of the following
statements has no subexponential Bound depth Frege
proofs:
(1) There is no field structure on {1,2, …,n} (when n not is a prime power).
(2) The set {1,2,…,n} cannot be organised as a vector space over the field
(3)
(4)
Fq (when n not is a power of q).
There is no 3-regular graph G on the set {1,2,…,n} (when n is odd)
There is no proper rectangular grid on the the set {1,2,..,n} (when n is a
prime number).
Conjecture (for Resolution as well
as for BDF):
• The presence of a hard instance where
C(n) is large, force C(m) to be large for
values of m close to n
(Justification: hard instances ought to have similar consequences as
impossible instances)
In general C(n) is smooth without big
(local) jumps when n increase.
Nullstellensatz-Proofs (over Field of
characteristic q).
Theorem [Riis 06]:
If Pn is a uniform generated sequence of polynomial equations. Then
there are 4 distinct behaviours of the NS degree complexity D(n)
(1) D(n) is bound by a constant
(2) D(n) ≥ l(n) for all sufficiently large values of n
(3) There exists a constant c such that the residue class of n modulo
qc determine if case (1) or case (2) apply
(4) The function D(n) has fluctuating complexity that fluctuates in a
very specific pattern such that (essentially) all complexities
between constant and l(n) occur on some infinite set.
Here log(n) ≤ l(n) ≤ n/2 is a universal function that can be
chosen independently of the actual sequence Pn.
Example of equations that have
fluctuating NS-complexity
•
•
•
•
•
•
•
•
∑j xij + ∑j yij -1 =0 for i Є {1,2,…,n}
∑j xij -1=0 for j Є {1,2,…,n}
∑i yij -1=0 for j Є {1,2,…,n}
xijxik = 0 for i,j,k Є {1,2,…,n}, j ≠ k
yijyik=0 for i,j,k Є {1,2,…,n}, j ≠ k
xijyik=0 for i,j,k Є {1,2,…,n}
yjiyki=0 for i,j,k Є {1,2,…,n}, j ≠ k
yjiyki=0 for i,j,k Є {1,2,…,n}, j ≠ k
This system of equations (that formalise the statement that there is no
bijection form n to 2n) has essentially NS degree complexity D(n)=qa(q,n)
where a(q,n) denote the power of q in the prime factor decomposition of n.
Thus case (4) in the classification is non-empty.
Summery:
• For weak propositional proof systems each
uniform sequence of tautologies has proof
complexity C(n) that behaves in quite
regular fashions.
Is something similar valid for strong
propositional systems?
• Is it possible that the full Frege proof
system only allows certain special
complexity functions?
Hard to say since each C(n) might (for
each uniform sequence of tautologies) be
bound by a polynomial.
Sporadic Proofs:
Consider a uniform sequences [η]n of tautologies.
A proof Rm is sporadic if there is no uniform
sequence Pn of proofs of [η]n where the proof
complexity of Pm is as low as that of Rm.
For many proof systems a high density of
sporadic proofs is not possible! If fact all the
proof systems I have analysed only allowed a
finite number of sporadic proofs.
Sporadic Proofs:
Something vaguely like Kreisels Conjecture: Short proof of A(n) in
PA for each n implies that the universal sentence
Forall x A(n) has a proof in PA.
Kreisel like Conjecture:
If we for an uniform sequences [η]n of tautologies can find short
(size bound by a fixed polynomial p(n) ) proofs of [η]n for each n,
then the corresponding system of bounded arithmetic proves η.
If an uniform sequence [η]n of tautologies has a high density of
short proofs, (i.e. has short proofs for many values of n) this force
in fact the sequence [η]n to have a sequence of fairly uniformly
given proofs.
How to construct hard tautologies
based on predicate logic?
• Is there a method to turn a first order
formulae into a hard sequence of
tautologies? Relativation was one such
method, but for stronger systems we need
harder tautologies.
Mathematical approaches to (weak)
Propositional Complexity
Few examples:
Ajtai: M. Ajtai, The independence of the modulo p
counting principles (1994)
Krajicek, Scanlon: Combinatorics with definable
sets: Euler Characteristics and Grothendieck
rings. (2000)
Krajicek: On degree of ideal membership proofs
from uniform families of polynomials over a
finite field. (2001)