We here give additional performance figures for runs on the test base of various ACE enumerators connected to the SAT solver:
Additionaly, we provide figures for memevents with internal encoding of model (memevents -axiom sela3, appears as MEM below).
N | avg (sec.) | geom (sec.) | max (sec.) | effort (days) | memory (Gb) | |
Operational | 3565/4503 | 2562.21 | 126.26 | 2.4e+05 | 1024.18 | 40.0 |
Axiom | 4480/4503 | 1394.14 | 20.57 | 2.3e+05 | 82.17 | 4.0 |
SAT | 4480/4503 | 1281.50 | 82.98 | 2.3e+05 | 66.45 | 4.0 |
SAT2 | 4480/4503 | 1159.16 | 20.90 | 1.7e+05 | 60.10 | 4.0 |
MEM-ACE | 4480/4503 | 2.26 | 1.57 | 2.6e+02 | 0.12 | 4.0 |
MEM | 4480/4503 | 2.02 | 0.12 | 4.1e+02 | 0.16 | 4.0 |