BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Albert Atserias\, Universitat Politècnica de Catalunya\, Microsof
 t Research Lectures - Albert Atserias\, Universitat Politècnica de Catalu
 nya
DTSTART:20110125T100000Z
DTEND:20110125T110000Z
UID:TALK29341@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Resolution underlies most state-of-the-art satisfiability-solv
 ing algorithms that are used in practice. I will start my talk by discussi
 ng this. Then I will focus on explaining some new understanding of the pow
 er of these algorithms that emerged from a novel kind of analysis of the p
 roduced proofs of unsatisfiability. The outcome is that the current standa
 rd methods for satisfiability-solving have the potential of simulating bou
 nded-width resolution with polynomial-time overhead\, provided they do ran
 dom decisions and restarts often enough.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR