Benchmarks submitted to SAT2002 competition

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: