BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Space Complexity of Polynomial Calculus (joint work with Yuval Fil
 mus\, Jakob Nordstrom\, Neil Thapen\, Noga Zewi) - Lauria\, M (Academy of 
 Sciences of the Czech Republic)
DTSTART:20120329T090000Z
DTEND:20120329T093000Z
UID:TALK37153@talks.cam.ac.uk
CONTACT:Mustapha Amrani
DESCRIPTION:During the last decade\, an active line of research in proof c
 omplexity has  been to  study  space complexity  and  time-space trade-off
 s  for proofs.   Besides  being a  natural  complexity  measure of  intrin
 sic interest\,  space is also  an important  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 s
 pace  in resolution and resolution-based proof systems\, and it is probabl
 y fair to say that  resolution is reasonably well understood  from this po
 int of  view. For  other natural  candidates  to study\,  however\, such  
 as polynomial calculus or cutting planes\,  very little has been known. We
  are not aware of any nontrivial space lower bounds for cutting planes\, a
 nd  for polynomial calculus  the only  lower bound  has been  for CNF form
 ulas  of unbounded  width in  [Alekhnovich et  al.'02]\,  where the space 
 lower bound is smaller than  the initial width of the clauses in the  form
 ulas.   Thus\, in  particular\,  it  has  been consistent  with\ncurrent k
 nowledge that polynomial calculus could be able to refute any k-CNF formul
 a in constant space.\n\nIn this  paper\, we  prove several new  results on
  space  in polynomial calculus (PC)\,  and in the  extended 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 for the canonical 3-
 CNF\n    version  of  the pigeonhole  principle  formulas  PHP^m_n with  m
 \n    pigeons and n holes\, and show that this is tight.\n\n  2. For PCR\,
   we  prove an  Omega(n)  space lower  bound  for a  bitwise\n    encoding
  of the functional 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    the width of 
 the formulas.\n\n  3.  We then  present another encoding of a  version of 
 the pigeonhole\n    principle that has  constant width\, and prove an  Ome
 ga(n) space lower\n    bound in PCR for these formulas as well.\n\n  4.  F
 inally\, we prove that any  k-CNF formula can be refuted in PC in\n    sim
 ultaneous exponential  size and  linear space (which  holds for\n    resol
 ution and  thus for PCR\, but  was not obviously  the case for\n    PC).  
 We  also characterize  a natural class  of CNF  formulas for\n    which th
 e space  complexity in resolution and PCR  does not change\n    when the f
 ormula is transformed into a 3-CNF in the canonical way\,\n    something t
 hat  we believe  can be useful  when proving  PCR space\n    lower  bounds
  for  other  well-studied formula  families in  proof\n    complexity.\n
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR