BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads - Marijn 
 Heule\, U. of Texas\, Austin
DTSTART:20120802T100000Z
DTEND:20120802T110000Z
UID:TALK39189@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Satisfiability (SAT) is considered as one of the most importa
 nt core technologies in formal verification and related areas. Even though
  there is steady progress in improving practical SAT solving\, there are l
 imits on scalability of SAT solvers. We address this issue and present a n
 ew approach\, called cube-and-conquer\, targeted at reducing solving time 
 on hard instances. This two-phase approach partitions a problem into many 
 thousands (or millions) of cubes using lookahead techniques.\nAfterwards\,
  a conflict-driven solver tackles the problem\, using the cubes to guide t
 he search. On several hard competition benchmarks\, our hybrid approach ou
 tperforms both lookahead and conflict-driven solvers.\nMoreover\, because 
 cube-and-conquer is natural to parallelize\, it is a competitive alternati
 ve for solving SAT problems in parallel.\n(Joint work with Oliver Kullmann
 \, Siert Wieringa\, and Armin Biere)
LOCATION:Primrose Room\, Microsoft Research Ltd\, 7 J J Thomson Avenue (Of
 f Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR