PeneLoPe, a Parallel Clause-Freezer Solver
Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, Cédric Piette · 2012
Abstract—This paper provides a short system description of our new portfolio-based solver called PeneLoPe, based on ManySat. Particularly, this solver focuses on collaboration between threads, providing different policies for exporting and importing learnt clauses between CDCL searches. Moreover, different restart strategies are also available, together with a deterministic mode. I. OVERVIEW PeneLoPe is a portfolio parallel SAT solver that uses the most effective techniques proposed in the sequential frame-work: unit propagation, lazy data structures, activity-based heuristics, progress saving for polarities, clause learning, etc. As for most of existing solvers, a first preprocessing step is achieved. For this step-which is typically sequential- we have chosen to make use of SatElite [3].