Benchmarks submitted to SAT2002 competition


The following benchmarks were submitted to SAT2002 competition. The original instances were modified (variable renaming, clause shuffling) before being used for the competition. To download the benchmarks, just click on their family name (not available yet, but you can download the whole family here ( TGZ (140Mb), BZ2 (114Mb)).

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
* 29 instances were submitted but 15 of them did not respect the input format (they contained clauses containing both one literal and its negation).
+ These instances did not respect the input format : they contain duplicate literals in clauses. We decided not to take them into account for the awards (both solvers and benchmarks awards).

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