Results by benchmark

Subcategory instances of the SAT RACE 08

Description of a cell contents

Cell example	Meaning
Answer	Solver result
TT=...	Total Time (TT): this is the CPU time (in seconds) used by the solver until termination. This time is only meaningful for complete solvers because incomplete solvers will always run until they time out

Meaning of some abbreviations

Abbreviation	Meaning
TO	Time Out
MO	Mem. Out (out of memory)

Meaning of the different colors

Color	Meaning
text	the solver cannot handle this instance
text	the solver gave no answer
text	the solver gave a definitive answer (SAT or UNSAT)
text	the solver performed better than the other ones on that instance
text	the solver was ended by a signal
text	the solver gave an incomplete answer
text	the solver was disqualified in the category
text	the solver gave a wrong answer

Bench name	Best results on this instance	built 2275_500	minisat2-core 061208	minisat2-simp 061208
SAT_RACE08/Q1/ 9dlx_vliw_at_b_iq1.cnf		? (TO) TT=1200.08	? (TO) TT=1200.15	? (TO) TT=1200.08
SAT_RACE08/Q1/ 9vliw_m_9stages_iq3_C1_bug8.cnf	SAT TT=30.234	SAT TT=560.64	SAT TT=31.084	SAT TT=30.234
SAT_RACE08/Q1/ AProVE07-16.cnf	UNSAT TT=422.179	UNSAT TT=1026.59	? (TO) TT=1200.06	? (TO) TT=1200.04
SAT_RACE08/Q1/ barrel6.dimacs	UNSAT TT=2.813	UNSAT TT=3.045	UNSAT TT=4.959	UNSAT TT=4.587
SAT_RACE08/ Q1/c6bidw_i.cnf	UNSAT TT=126.74	UNSAT TT=228.158	UNSAT TT=741.386	UNSAT TT=126.74
SAT_RACE08/Q1/ c8nidw.cnf	UNSAT TT=758.037	? (TO) TT=1200	? (TO) TT=1200.14	? (TO) TT=1200.08
SAT_RACE08/ Q1/c9n_i.cnf	UNSAT TT=122.146	UNSAT TT=122.146	UNSAT TT=447.582	UNSAT TT=539.342
SAT_RACE08/Q1/ dated-5-15-u.cnf	UNSAT TT=727.001	UNSAT TT=738.14	? (TO) TT=1200.04	? (TO) TT=1200.07
SAT_RACE08/ Q1/ dspam_dump_vc949.cnf	UNSAT TT=0.998	UNSAT TT=5.086	UNSAT TT=866	UNSAT TT=1.861
SAT_RACE08/ Q1/ dspam_dump_vc973.cnf	UNSAT TT=3.542	UNSAT TT=5.041	? (TO) TT=1200.12	UNSAT TT=3.542
Bench name	Best results on this instance	built 2275_500	minisat2-core 061208	minisat2-simp 061208
SAT_RACE08/Q1/ goldberg03:hard_eq_check:alu4mul.miter.used-as.sat04-326.cnf	UNSAT TT=577.704	UNSAT TT=709.976	UNSAT TT=619.652	UNSAT TT=577.704
SAT_RACE08/Q1/ goldberg03:hard_eq_check:term1mul.miter.used-as.sat04-337.cnf	SIGNAL TT=0.093	? (TO) TT=1200.13	? (TO) TT=1200.04	? (TO) TT=1200.02
SAT_RACE08/Q1/ IBM_FV_2004_rule_batch_01_SAT_dat.k90.cnf	SAT TT=32.413	SAT TT=321.905	SAT TT=256.335	SAT TT=63.588
SAT_RACE08/Q1/ IBM_FV_2004_rule_batch_1_11_SAT_dat.k80.cnf	SAT TT=132.486	SAT TT=823.801	? (TO) TT=1200.1	SAT TT=132.486
SAT_RACE08/Q1/ IBM_FV_2004_rule_batch_23_SAT_dat.k80.cnf	SAT TT=681.009	? (TO) TT=1200.04	? (TO) TT=1200.11	SAT TT=681.009
SAT_RACE08/Q1/ IBM_FV_2004_rule_batch_29_SAT_dat.k25.cnf	UNSAT TT=724.6	UNSAT TT=756.695	? (TO) TT=1200.04	UNSAT TT=1037.52
SAT_RACE08/Q1/ longmult13.dimacs	UNSAT TT=44.35	UNSAT TT=50.682	UNSAT TT=74.754	UNSAT TT=44.35
SAT_RACE08/Q1/ manol-pipe-f9b.cnf		? (TO) TT=1200.04	? (TO) TT=1200.14	? (TO) TT=1200.11
SAT_RACE08/Q1/ marijn:Philips:philips.used-as.sat04-301.cnf	UNSAT TT=1043.79	? (TO) TT=1200.06	? (TO) TT=1200.04	UNSAT TT=1043.79
SAT_RACE08/ Q1/md5_47_3.cnf	SAT TT=189.298	SAT TT=734.853	SAT TT=189.298	SAT TT=932.851
Bench name	Best results on this instance	built 2275_500	minisat2-core 061208	minisat2-simp 061208
SAT_RACE08/ Q1/md5_47_4.cnf	SAT TT=618.602	? (TO) TT=1200.05	? (TO) TT=1200.12	SAT TT=618.602
SAT_RACE08/ Q1/md5_48_2.cnf	SAT TT=524.263	SAT TT=875.416	? (TO) TT=1200.07	SAT TT=524.263
SAT_RACE08/Q1/ mizh-md5-47-5.cnf	SAT TT=348.019	? (TO) TT=1200.07	? (TO) TT=1200.05	SAT TT=467.219
SAT_RACE08/Q1/ mizh-sha0-35-4.cnf	SAT TT=42.756	SAT TT=160.643	SAT TT=42.756	SAT TT=934.683
SAT_RACE08/ Q1/ partial-10-15-s.cnf	SIGNAL TT=38.161	? (TO) TT=1200.01	? (TO) TT=1200.18	? (TO) TT=1200.18
SAT_RACE08/Q1/ pico:prop00_75_fixed.cnf	UNSAT TT=0.195	UNSAT TT=0.206	UNSAT TT=72.362	UNSAT TT=26.561
SAT_RACE08/Q1/ pico:prop05_75_fixed.cnf	UNSAT TT=101.286	UNSAT TT=157.653	UNSAT TT=454.593	UNSAT TT=101.286
SAT_RACE08/Q1/ SAT_dat.k100.cnf	UNSAT TT=338.879	UNSAT TT=787.655	UNSAT TT=572.754	UNSAT TT=1117.72
SAT_RACE08/Q1/ SAT_dat.k30.cnf	UNSAT TT=1098.66	? (TO) TT=1200.08	? (TO) TT=1200.12	UNSAT TT=1098.66
SAT_RACE08/Q1/ SAT_dat.k60.cnf		? (TO) TT=1200.01	? (TO) TT=1200.11	? (TO) TT=1200.12
Bench name	Best results on this instance	built 2275_500	minisat2-core 061208	minisat2-simp 061208
SAT_RACE08/Q1/ SAT_dat.k75_22.cnf	SAT TT=520.666	SAT TT=701.054	? (TO) TT=1200.04	SAT TT=520.666
SAT_RACE08/Q1/ SAT_dat.k75_29.cnf	SAT TT=113.406	SAT TT=1075.51	SAT TT=241.687	SAT TT=791.669
SAT_RACE08/Q1/ SAT_dat.k75.cnf	SIGNAL TT=2.376	? (TO) TT=1200.07	? (TO) TT=1200.12	? (TO) TT=1200.12
SAT_RACE08/Q1/ SAT_dat.k80_04.cnf	SAT TT=104.137	SAT TT=553.424	SAT TT=461.689	SAT TT=104.137
SAT_RACE08/Q1/ SAT_dat.k80.cnf	SAT TT=785.58	SAT TT=1168.99	? (TO) TT=1200.1	SAT TT=785.58
SAT_RACE08/Q1/ SAT_dat.k85.cnf		? (TO) TT=1200	? (TO) TT=1200.07	? (TO) TT=1200.08
SAT_RACE08/Q1/ SAT_dat.k90.cnf		? (TO) TT=1200	? (TO) TT=1200.06	? (TO) TT=1200.1
SAT_RACE08/Q1/ schuppan03:l2s:abp4-1-k31-unsat.used-as.sat04-438.cnf	UNSAT TT=84.756	UNSAT TT=132.426	UNSAT TT=148.768	UNSAT TT=84.756
SAT_RACE08/Q1/ schuppan03:l2s:motors-stuck-2-k314-unsat.used-as.sat04-434.cnf	UNSAT TT=153.052	UNSAT TT=574.893	? (TO) TT=1200.06	UNSAT TT=166.599
SAT_RACE08/Q1/ schuppan03:l2s:motors-stuck-2-k315-sat.used-as.sat04-435.cnf	SAT TT=116.254	SAT TT=551.892	? (TO) TT=1200.04	SAT TT=116.254
Bench name	Best results on this instance	built 2275_500	minisat2-core 061208	minisat2-simp 061208
SAT_RACE08/ Q1/sha0_35_3.cnf	SAT TT=50.931	SAT TT=50.931	SAT TT=60.45	? (TO) TT=1200.08
SAT_RACE08/ Q1/sha0_36_3.cnf	SAT TT=329.935	SAT TT=649.129	? (TO) TT=1200.06	? (TO) TT=1200.05
SAT_RACE08/ Q1/sha0_36_4.cnf	SAT TT=152.837	? (TO) TT=1200.1	? (TO) TT=1200.09	? (TO) TT=1200.15
SAT_RACE08/Q1/ simon03:sat02bis:cnf-r4-b1-k1.1-comp.used-as.sat04-354.cnf	SAT TT=44.437	SAT TT=68.154	SAT TT=608.496	SAT TT=68.867
SAT_RACE08/Q1/ simon03:sat02:f2clk_50.used-as.sat04-365.cnf	SIGNAL TT=0.491	? (TO) TT=1200.04	? (TO) TT=1200.06	? (TO) TT=1200.06
SAT_RACE08/Q1/ simon03:sat02:fifo8_300.used-as.sat04-362.cnf	UNSAT TT=66.88	UNSAT TT=205.811	UNSAT TT=224.439	UNSAT TT=66.88
SAT_RACE08/Q1/ simon03:sat02:fifo8_400.used-as.sat04-363.cnf	UNSAT TT=144.906	UNSAT TT=430.612	UNSAT TT=799.984	UNSAT TT=174.065
SAT_RACE08/Q1/ simon03:sat02:w08_15.used-as.sat04-360.cnf	SAT TT=156.046	SAT TT=629.853	SAT TT=747.848	SAT TT=156.046
SAT_RACE08/Q1/ sortnet-7-ipc5-h16-sat.cnf	SAT TT=629.921	? (TO) TT=1200.06	? (TO) TT=1200.07	? (TO) TT=1200.03
SAT_RACE08/Q1/ uts-l06-ipc5-h34-unknown.cnf	SAT TT=80.347	SAT TT=628.322	SAT TT=223.925	SAT TT=236.394

Some statistics...

	built 2275_500	minisat2-core 061208	minisat2-simp 061208
Number of times the solver is able to give the best known answer	33	22	34
Number of times the solver is the best solver from a complete solver point of view (i.e. best known answer and best TT time)	2	2	19

Back to ReVivAl page

Back to ReVivAl 0.23 evaluation page

Back to Cédric Piette Home Page

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