AmPharoS is an original parallel SAT solver based on the divid and conquer paradigm. This solver, dedicated to work on plenty of cores, runs workers on sub-formulas restricted by cubes. This page contains scatter plots, resources and data for evaluation purposes of the paper "An adaptive parallel SAT solver" accepted to the 22nd International Conference on Principles and Practice of Constraint Programming (CP'16), pp. 30-48, september 2016.  [PDF]

People involved in this project:

• Gilles Audemard (audemard@cril.fr)
• Jean-Marie Lagniez (lagniez@cril.fr)
• Nicolas Szczepanski (szczepanski@cril.fr)
• Sébastien Tabary (tabary@cril.fr)