PeneLoPe, a parallel SAT solver
The purpose of this page is to provide information about the PeneLoPe solver.
PeneLoPe stands for Parallel Lbd and PSM.
Information
- People involved in this project:
- Related papers:
- Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez and Cédric Piette, "Revisiting Clause Exchange in Parallel SAT Solving". In Fifteenth International Conference on Theory and Applications of Satisfiability Testing (SAT'12), pp. 200--213, may 2012. [PDF]
- Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs, "On freezeing and reactivating learnt clauses". In International Conference on Theory and Applications of Satisfiability Testing (SAT'11), pp. 188-200, june 2011.
- Gilles Audemard, Laurent Simon, "Predicting Learnt Clauses Quality in Modern SAT Solver". In Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), pp. 399-404, july 2009.
- Youssef Hamadi, Saïd Jabbour, Lakhdar Saïs, "ManySAT: a new Parallel SAT solver", In Journal of Satisfiability Boolean Modeling and Computation, (JSAT), special issue on Parallel SAT solving, pp. 245-262, 2009
- Niklas Een, Niklas Sörensson, "An Extensible SAT-solver", In International Conference on Theory and Applications of Satisfiability Testing (SAT '03)
- Complete traces are available here in an archive (~750Mo).
- Following sections provide some graph comparing PeneLoPe with other well known solver: plingeling, ppfolio, cryptominisat and manysat.
- A system description can also be found in Proceedings of SAT Challenge 2012, available here.
Sources
The sources of PeneLope can be obtained at bitbucket.Competition
During the 2012 Challenge, PeneLoPe arrived second in the parallel track, at just one instance from the first position!
During the 2013 SAT Competition, PeneLoPe arrived third place! During the 2014 SAT Competition, PeneLoPe obtained the second place!
Results on 8 cores
Complete cpu time (in seconds) for the different versions of PeneLoPe are available here. Those results were obtained using the deterministic mode.The results of the non deterministic versions of Penelope used against other state of the art solver and their result in wallclock time are available here as an archive.
We provide some graphical comparison between PeneLoPe (version freeze) with state of the art solvers (click to enlarge)
- cryptominisat
- manysat
- plingeling
- ppfolio
Results on 32 cores
The result of the non deterministic version of Penelope used against other state of the art solver and their result in wallclock time are available here as an archive.We provide some graphical comparison between PeneLoPe (version freeze) with state of the art solvers (click to enlarge)
- cryptominisat
- manysat
- plingeling
- ppfolio
Binary executable
The version submitted to the SAT Challenge 2012 can be downloaded LINUX x86_64. We also provide windows 32bits version and a windows 64bits version. Those were compiled using the mingw compiler and were not heavily tested. Feel free to contact us if you have any problem.If you need a version for another architecture/os, please contact us.
In order to be able to reproduce the results of our paper "Revisiting Clause Exchange in Parallel SAT Solving", we provide the linux x86_64 binaries that were used: penelope freeze and penelope no-freeze. A readme file explain the content of those archives.