AmPharoS

Information

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)

Resources

Please contact us to obtain the source files of AmPharoS.

SAT-Race 2015 Parallel track benchmarks link :
[sr15bench-hard.zip] (329MB)

Assumptive Unit literals

The left picture represents a decorated tree owned by Manager with the additional literals (in rectangles) given by the solvers S₁ and S₂. The nodes represent variables (a plain (resp. dotted) line means that the variable is assigned to true (resp. false)). S₁ and S₂ are solving sub-problems induced by cubes x₁∧¬x₂∧¬x₄ and x₁∧¬x₂∧x₄ respectively.

Results

32 and 64 cores 32 cores 64 cores

(32 cores)

(64 cores)

Scalability evaluation

Dynamic vs Static