[Proof Complexity] New paper
Neil Thapen
thapen at math.cas.cz
Tue Nov 4 10:58:16 CET 2014
Dear colleagues,
A new paper, "The space complexity of cutting planes refutations", by
Nicola Galesi, Pavel Pudlak and myself, is available on ECCC, at
http://eccc.hpi-web.de/report/2014/138/
Any comments or corrections are appreciated.
The abstract is: We study the space complexity of the cutting planes proof
system, in which the lines in a proof are integral linear inequalities. We
measure the space used by a refutation as the number of inequalities that
need to be kept on a blackboard while verifying it. We show that any
unsatisfiable set of inequalities has a cutting planes refutation in space
five. This is in contrast to the weaker resolution proof system, for which
the analogous space measure has been well-studied and many optimal lower
bounds are known.
Motivated by this result we consider a natural restriction of cutting
planes, in which all coefficients have size bounded by a constant. We show
that there is a CNF which requires super-constant space to refute in this
system. The system nevertheless already has an exponential speed-up over
resolution with respect to size, and we additionally show that it is
stronger than resolution with respect to space, by constructing
constant-space cutting planes proofs of the pigeonhole principle with
coefficients bounded by two.
We also consider variable space for cutting planes, where we count the
number of instances of variables on the blackboard, and total space, where
we count the total number of symbols.
Best,
Neil
More information about the Proof-Complexity
mailing list