ReVivAl 0.23 evaluation page


Preliminaries

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.

Comparison of built_2275_500 and minisat2-simp_061208

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.

Category "crafted instances" (CRAFTED) (detailled results)

Solver Name#benchsSolvedUNSATSATUNKNOWNBad AnswersMisc.
built
2275_500
1439794
(55.18%)
379
(26.34%)
415
(28.84%)
645
(44.82%)
0
(0%)
0
minisat2-core
061208
1439745
(51.77%)
349
(24.25%)
396
(27.52%)
694
(48.23%)
0
(0%)
0
minisat2-simp
061208
1439771
(53.58%)
369
(25.64%)
402
(27.94%)
668
(46.42%)
0
(0%)
0

Solver NameProgress
built
2275_500
done
1439
UNSAT
379
SAT
415
?
645
minisat2-core
061208
done
1439
UNSAT
349
SAT
396
?
694
minisat2-simp
061208
done
1439
UNSAT
369
SAT
402
?
668

Category "industrial instances" (INDUST) (detailled results)

Solver Name#benchsSolvedUNSATSATUNKNOWNBad AnswersMisc.
built
2275_500
13051079
(82.68%)
423
(32.41%)
656
(50.27%)
226
(17.32%)
0
(0%)
0
minisat2-core
061208
1305945
(72.41%)
412
(31.57%)
533
(40.84%)
360
(27.59%)
0
(0%)
0
minisat2-simp
061208
13051002
(76.78%)
414
(31.72%)
588
(45.06%)
303
(23.22%)
0
(0%)
0

Solver NameProgress
built
2275_500
done
1305
UNSAT
423
SAT
656
?
226
minisat2-core
061208
done
1305
UNSAT
412
SAT
533
?
360
minisat2-simp
061208
done
1305
UNSAT
414
SAT
588
?
303

Category "Instances from SAT RACE'08" (RACE08) (detailled results)

Some explanations

Back to ReVivAl page

Back to C├ędric Piette Home Page

Lens Computer Science Research Centre (CRIL) where I am working.