Previous Up Next

Using a SAT solver

We also have a C++ implementation of the proposed axiomatic model, based upon the minisat SAT solver. This new simulator accepts cycles of candidate relaxations as input, build the corresponding tests internally and and checks the Allow/Forbid status of the resulting tests.

As a consequence, we can run this new solver only on the 5544 tests that were build from cycles.1 We did so, and confirmed the results found by the ppcmem simulators.

As demonstrated by the following table, the performance improvement over ppcmem is dramatic:

 Navg (sec.)geom (sec.)max (sec.)effort (days)memory (Gb)
Operational3565/45032562.21126.262.4e+051024.1840.0
Axiom4480/45031394.1420.572.3e+0582.174.0
SAT5544/55442.672.2610.260.13

The SAT solver terminates on all its input, running no test in more than about 10 seconds in reduced memory space. The total computing effort is of about 3 hours — effective wall-clock time is of about 25 minutes on an 8-cores machine, using simple parallelisation techniques.


Previous Up Next