Results by benchmark

Subcategory instances of the SAT RACE 08

Description of a cell contents

Cell exampleMeaning
AnswerSolver 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

AbbreviationMeaning
TOTime Out
MOMem. Out (out of memory)

Meaning of the different colors

ColorMeaning
textthe solver cannot handle this instance
textthe solver gave no answer
textthe solver gave a definitive answer (SAT or UNSAT)
textthe solver performed better than the other ones on that instance
textthe solver was ended by a signal
textthe solver gave an incomplete answer
textthe solver was disqualified in the category
textthe solver gave a wrong answer
Bench nameBest 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 nameBest 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 nameBest 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 nameBest 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 nameBest 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 answer332234
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)2219

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.