![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads
![]() Cube and Conquer: Guiding CDCL SAT Solvers by LookaheadsAdd to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other listsComputer Laboratory Opera Group Seminars RSC South East England Regional Meeting Cambridge University Astronomical Society (CUAS)Other talksLunchtime Talk: Helen's Bedroom Equations in groups Mechanical properties of cells or cell components on the micro- and nanometer scale All-resolutions inference for brain imaging Part Ib Group Project Presentations |