University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads

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 lists

Room SG2 of the Alison Richard Building, 7 West Road, CB39DT, Cambridge GR04, English Faculty Building, 9 West Road, Sidgwick Site and online West 2, West Hub

Other talks

TBC CUSCRS and Renal Medicine Tea and Coffee Break Semiconductor-based neutron detector development at QMUL TBC Cooperation as a Laboratory of Being
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity