ReVivAl 0.23 has been extensively evalued from an empirical point of view. This page sums up obtained results.
Those experiments compare minisat2-simp_061208 with or without the use of ReVivAl 0.23. ReVivAl has been used in a procedure called "built_2275_500", that first calls ReVivAl in order to vivify the provided CNF formula during at most 500 seconds. Then, minisat is called. We also compared these approaches with the "core" version of minisat 2.0
The experiments have been conducted on a large number of structured (i.e. crafted and industrial) instances from SAT competitions, SAT Races, and various other sources. All our experiments have been conducted on Intel Xeon 3GHz under Linux CentOS 4.1. (kernel 2.6.9) with a RAM limit of 900MB. For all experiments, a timeout of 1,200 seconds has been respected.
A special thank to Olivier Roussel for making his evaluation system available.
NB: Most of links come from internal evaluation system and do not work. Only blinked ones (detailled results) are effective.
Each point in the figure below represents the CPU time needed by the two solvers to solve a same instance. Points above the diagonal line represent instances where built_2275_500 performs better. Points below the diagonal line represent instances where minisat2-simp_061208 performs better.
| Solver Name | #benchs | Solved | UNSAT | SAT | UNKNOWN | Bad Answers | Misc. |
|---|---|---|---|---|---|---|---|
| built 2275_500 |
1439 | 794 (55.18%) |
379 (26.34%) |
415 (28.84%) |
645 (44.82%) |
0 (0%) |
0 |
| minisat2-core 061208 |
1439 | 745 (51.77%) |
349 (24.25%) |
396 (27.52%) |
694 (48.23%) |
0 (0%) |
0 |
| minisat2-simp 061208 |
1439 | 771 (53.58%) |
369 (25.64%) |
402 (27.94%) |
668 (46.42%) |
0 (0%) |
0 |
| Solver Name | Progress | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| built 2275_500 |
| ||||||||||
| minisat2-core 061208 |
| ||||||||||
| minisat2-simp 061208 |
| ||||||||||
| Solver Name | #benchs | Solved | UNSAT | SAT | UNKNOWN | Bad Answers | Misc. |
|---|---|---|---|---|---|---|---|
| built 2275_500 |
1305 | 1079 (82.68%) |
423 (32.41%) |
656 (50.27%) |
226 (17.32%) |
0 (0%) |
0 |
| minisat2-core 061208 |
1305 | 945 (72.41%) |
412 (31.57%) |
533 (40.84%) |
360 (27.59%) |
0 (0%) |
0 |
| minisat2-simp 061208 |
1305 | 1002 (76.78%) |
414 (31.72%) |
588 (45.06%) |
303 (23.22%) |
0 (0%) |
0 |
| Solver Name | Progress | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| built 2275_500 |
| ||||||||||
| minisat2-core 061208 |
| ||||||||||
| minisat2-simp 061208 |
| ||||||||||