BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Validating SAT Refutations - Nathan Wetzler\, UT Austin
DTSTART:20130730T090000Z
DTEND:20130730T100000Z
UID:TALK46463@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We give an overview of our recent work on validating satisfiab
 ility refutations.  Satisfiability (SAT) solvers are used not only to find
  a solution for a Boolean formula\, but also to make the claim that no sol
 ution exists.  If no solution is reported\, a solver can emit a proof of u
 nsatisfiability\, or refutation\, which can then be validated by an unsati
 sfiability proof checker.  Ideally\, SAT refutations should be:  easy to e
 mit\, compact\, checked efficiently\, checked in a trusted way\, and expre
 ssive.  Existing proof formats support at most two of these five propertie
 s.  We present a new clausal proof format\, called DRUP\, that uses clause
  deletion information and can be checked efficiently.
LOCATION: Microsoft Research Ltd\, 21 Station Road\, Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR