BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Space Complexity of Polynomial Calculus (joint wor
k with Yuval Filmus\, Jakob Nordstrom\, Neil Thape
n\, Noga Zewi) - Lauria\, M (Academy of Sciences o
f the Czech Republic)
DTSTART;TZID=Europe/London:20120329T100000
DTEND;TZID=Europe/London:20120329T103000
UID:TALK37153AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/37153
DESCRIPTION:During the last decade\, an active line of researc
h in proof complexity has been to study space c
omplexity and time-space trade-offs for proofs.
Besides being a natural complexity measure
of intrinsic interest\, space is also an import
ant issue in SAT solving\, and so research has
mostly focused on weak systems that are used
by SAT solvers.\n\nThere has been a relatively
long sequence of papers on space in resolutio
n and resolution-based proof systems\, and it is p
robably fair to say that resolution is reasonably
well understood from this point of view. For o
ther natural candidates to study\, however\, su
ch as polynomial calculus or cutting planes\, ve
ry little has been known. We are not aware of any
nontrivial space lower bounds for cutting planes\,
and for polynomial calculus the only lower bou
nd has been for CNF formulas of unbounded widt
h in [Alekhnovich et al.'02]\, where the space
lower bound is smaller than the initial width of
the clauses in the formulas. Thus\, in particu
lar\, it has been consistent with\ncurrent kno
wledge that polynomial calculus could be able to r
efute any k-CNF formula in constant space.\n\nIn t
his paper\, we prove several new results on spa
ce in polynomial calculus (PC)\, and in the ext
ended proof system polynomial calculus resolution
(PCR) studied in [Alekhnovich et al.'02]:\n\n 1.
We prove an Omega(n) space lower bound in PC fo
r the canonical 3-CNF\n version of the pigeon
hole principle formulas PHP^m_n with m\n pi
geons and n holes\, and show that this is tight.\n
\n 2. For PCR\, we prove an Omega(n) space lo
wer bound for a bitwise\n encoding of the fu
nctional pigeonhole principle with m pigeons and\n
n holes. These formulas have width O(log(n))
\, and so this is an\n exponential improvement
over [Alekhnovich et al.'02] measured in\n t
he width of the formulas.\n\n 3. We then presen
t another encoding of a version of the pigeonhole
\n principle that has constant width\, and pro
ve an Omega(n) space lower\n bound in PCR for
these formulas as well.\n\n 4. Finally\, we prov
e that any k-CNF formula can be refuted in PC in\
n simultaneous exponential size and linear sp
ace (which holds for\n resolution and thus fo
r PCR\, but was not obviously the case for\n
PC). We also characterize a natural class of C
NF formulas for\n which the space complexity
in resolution and PCR does not change\n when t
he formula is transformed into a 3-CNF in the cano
nical way\,\n something that we believe can b
e useful when proving PCR space\n lower boun
ds for other well-studied formula families in
proof\n complexity.\n
LOCATION:Seminar Room 1\, Newton Institute
CONTACT:Mustapha Amrani
END:VEVENT
END:VCALENDAR