Concurrent Cube-and-Conquer

Concurrent Cube-and-Conquer

Van der Tak, P.

Heule, M.J.H. (mentor)

Electrical Engineering, Mathematics and Computer Science

Algorithmics group

Computer Science

2012-06-27

Recent work introduced the cube-and-conquer technique to solve hard SAT instances. It combines the two dominant SAT solving techniques: lookahead and conflict-driven clause learning (CDCL). First, it partitions the search space into so called cubes using a lookahead solver. Each cube is tackled by a conflict-driven clause learning solver. Crucial for strong performance is the cutoff heuristic that decides when to switch from lookahead to CDCL. Yet, this offline heuristic is far from ideal. In this work, we present a novel hybrid solver that applies lookahead and CDCL simultaneously. Both solvers work together on each cube, while communication is restricted to synchronization. Our concurrent cube-and-conquer (CCC) solver can solve many instances faster than pure lookahead, pure CDCL and offline cube-and-conquer, but is not suitable for all instances. We have developed two metrics that can be used to accurately select when to apply CCC or to fall back to pure CDCL. We think CCC is especially useful as part of a portfolio that selects a suitable solver based on machine learning techniques, and show that machine learning techniques can indeed be used to select accurately whether CCC or CDCL works best.

satisfiability

http://resolver.tudelft.nl/uuid:7a248cd8-7749-4bd5-a938-ed56a7bd9992

Student theses

master thesis

(c) 2012 Van der Tak, P.