Concurrent Cube-and-Conquer - (Poster Presentation)

Abstract Satisfiability solvers targeting industrial instances are currently almost always based on conflict-driven clause learning (CDCL) [5]. This technique can successfully solve very large instances. Yet on small, hard problems lookahead solvers [3] often perform better by applying much more reasoning in each search node and then recursively splitting the search space until a solution is found.

Authors

• Peter van der Tak
• Marijn J. H. Heule
• Armin Biere

Keywords

No keywords are indexed for this paper.