Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads

Add to your list(s) Download to your calendar using vCal

• Marijn Heule, U. of Texas, Austin
• Thursday 02 August 2012, 11:00-12:00
• Primrose Room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new 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. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel. (Joint work with Oliver Kullmann, Siert Wieringa, and Armin Biere)

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• Primrose Room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• personal list
• rp587

Note that ex-directory lists are not shown.