Here is a local zipped copy of all the benchmarks: sc2002benchs.zip.
Submitter name | Benchs family name | number of instances |
---|---|---|
Industrial category | ||
Fadi A. Aloul | Bart | 21 |
Fadi A. Aloul | Homer | 15 |
Armin Biere | cmpadd | 8 |
Armin Biere | dinphil-SAT | 11 |
Armin Biere | dinphil-UNSAT | 11 |
Samuel Dellacherie-Valiosys | Cache | 2 |
Samuel Dellacherie-Valiosys | Comb | 3 |
Samuel Dellacherie-Valiosys | f2clk | 3 |
Samuel Dellacherie-Valiosys | fifo | 4 |
Samuel Dellacherie-Valiosys | ip | 4 |
Samuel Dellacherie-Valiosys | w08 | 3 |
Samuel Dellacherie-Valiosys | w10 | 4 |
Eugene Goldberg | BMC | 76+ |
Eugene Goldberg | BMC-2 | 6 |
Eugene Goldberg | fpga-routing-1 | 32 |
Eugene Goldberg | rand-net70 | 12 |
Eugene Goldberg | rand-net40 | 12 |
Eugene Goldberg | rand-net50 | 12 |
Eugene Goldberg | rand-net60 | 12 |
Gi-Joon Nam | fpga-routing-2 | 6 |
Steven Prestwich | Mediator | 4 |
Satex-Challenges | satex-challenges | 36 |
Allen Van-Gelder | CheckerInterchange | 4 |
Miroslav Velev | sss-sat-1.0 | 10 |
Miroslav Velev | fvp-unsat-2.0-2pipe | 3 |
Miroslav Velev | fvp-unsat-2.0-3pipe | 5 |
Miroslav Velev | fvp-unsat-2.0-4pipe | 6 |
Miroslav Velev | fvp-unsat-2.0-5pipe | 2 |
Miroslav Velev
|
fvp-unsat-2.0-6pipe
|
2 |
Miroslav Velev
|
fvp-unsat-2.0-7pipe
|
2
|
Emmanuel Zarpas-IBM | IBM-Easy | 3+ |
Emmanuel Zarpas-IBM | IBM-Hard | 3+ |
Emmanuel Zarpas-IBM | IBM-Medium | 2+ |
Andrzej Zbrzezny | BMCTA | 2+ |
Lintao Zhang | sha | 2 |
Handmade category | ||
Fadi A. Aloul | Lisa | 14* |
Eugene Goldberg | hanoi | 3 |
Eugene Goldberg | hanoi-2 | 2 |
Chu-Min Li | Matrix | 5 |
Chu-Min Li | Polynomial | 9 |
Chu-Min Li | Urquhart | 6 |
Dan Pehoushek | ezfact-256 | 1 |
Dan Pehoushek | twentyvars-6cnf20 | 10 |
Dan Pehoushek | twentyvars-7cnf20 | 10 |
Dan Pehoushek | twentyvars-7cnf30 | 8 |
Dan Pehoushek | twentyvars-8cnf20 | 2 |
Dan Pehoushek | ezfact-16 | 10 |
Dan Pehoushek | ezfact-32 | 10 |
Dan Pehoushek | ezfact-48 | 10 |
Dan Pehoushek | ezfact-64 | 10 |
Federico Ricci-Tersinghi | glassy-sat-sel | 12 |
Laurent Simon |
Urquhart3 |
10 |
Laurent Simon |
Urquhart4 |
10 |
Laurent Simon |
Urquhart5 |
10 |
Allen Van-Gelder | GridMNbench | 8 |
Allen Van-Gelder | Rope | 25 |
Hantao Zhang | QGgroup | 19 |
Lintao Zhang | xor-chain-1 | 13 |
Lintao Zhang | xor-chain-1.1 | 13 |
Lintao Zhang | xor-chain-2 | 13 |
Tuomo Pyhala | braun-sat-4-30 | 4 |
Tuomo Pyhala | braun-sat-4-35 | 4 |
Tuomo Pyhala | braun-sat-4-40 | 4 |
Tuomo Pyhala | braun-unsat-4-30 | 4 |
Tuomo Pyhala | braun-unsat-4-35 | 4 |
Tuomo Pyhala | braun-unsat-4-40 | 4 |
Random category | ||
to be available soon |
Please note that these are the various families as submitted by their authors to the competition. To rank the solvers according to series, we merged together some families to make a serie, and even partition one into several series.
Here are the series used for evaluating the solvers:
Series name | Corresponding families (if different) | |
Industrial
series |
||
Bart | ||
Homer | ||
cmpadd | ||
dinphil-SAT | ||
dinphil-UNSAT | ||
cache | ||
comb | ||
f2clk | ||
fifo | ||
ip | ||
w | w08, w10 | |
bmc1 | ||
bmc2 | ||
goldberg/fpga_routing | ||
rand_net | randnet40, randnet50, randnet60, randnet70 | |
nam/fpga-routing | ||
mediator | ||
CheckerInterchange | ||
fvp-unsat.2.0 | fvp-unsat.2.0-2pipe, fvp-unsat.2.0-3pipe, fvp-unsat.2.0-4pipe, fvp-unsat.2.0-5pipe, fvp-unsat.2.0-6pipe, fvp-unsat.2.0-7pipe, | |
sss-sat-1.0 | ||
sha | ||
satex-challenges/2dlx_ca_mc_ex_bp_f | satex-challenges | |
satex-challenges/2dlx_cc_mc_ex_bp_f | satex-challenges | |
satex-challenges/9vliw_bp_mc | satex-challenges | |
satex-challenges/c | satex-challenges | |
satex-challenges/cnf | satex-challenges | |
Handmade
series |
||
Lisa | ||
hanoi | ||
matrix | ||
ezfact | ||
twentyvars/6cnf20 | ||
twentyvars/7cnf | ||
twentyvars/7cnf | ||
twentyvars/8cnf20 | ||
glassy-sat-sel | ||
GridMNbench | ||
Rope | ||
qgbench | ||
xor-chain/x1 | ||
xor-chain/x1.1 | ||
xor-chain/x2 | ||
chu-min-li/urquhart/urquhartX.cnf | Urquhart |
|
chu-min-li/urquhart/urquhartXbis.cnf | Urquhart |
|
simon/Urquhart | ||
pyhala-braun-sat | braun-sat-4-30, braun-sat-4-35, braun-sat-4-40 | |
pyhala-braun-unsat | braun-unsat-4-30, braun-unsat-4-35, braun-unsat-4-40 |
|
simon/satex-challenges/3bitadd_31 | satex-challenges |
|
simon/satex-challenges/f | satex-challenges |
|
simon/satex-challenges/g | satex-challenges |
|
simon/satex-challenges/par32-c | satex-challenges |
|
simon/satex-challenges/par32.cnf | satex-challenges |
|