Author name cluster

Peter van der Tak

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

SAT Conference 2012 Conference Paper

Concurrent Cube-and-Conquer - (Poster Presentation)

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

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.

Details

SAT Conference 2011 Conference Paper

Between Restarts and Backjumps

Antonio Ramos
Peter van der Tak
Marijn J. H. Heule

Abstract This paper introduces a novel technique that significantly reduces the computational costs to perform a restart in conflict-driven clause learning (CDCL) solvers. Our technique exploits the observation that CDCL solvers make many redundant propagations after a restart. It efficiently predicts which decisions will be made after a restart. This prediction is used to backtrack to the first level at which heuristics may select a new decision rather than performing a complete restart. In general, the number of conflicts that are encountered while solving a problem can be reduced by increasing the restart frequency, even though the solving time may increase. Our technique counters the latter effect. As a consequence CDCL solvers will favor more frequent restarts.

Details