SAT04 Competition Main Page

LRI,
University of
Paris-Sud

LRI,
University of
Paris-Sud

Abstract: What can be told about the well-known contest? This third edition was great, and located in Vancouver (great place!). All results are available online from this site. You can read more about the contest by reading the Sat 2004 contest howtos.
Added (July, 2004) : detailed poscript description of each solvers, and one check-your-solver-yourself section in this page.

Some statistics about the competition

2 organizers :-) (Daniel Le Berre and Laurent Simon),
3 judges (Fahiem Bacchus, Joao Marques-Silva and Hans Klein Buning)
25 solver main submitters (Alexander Nadel, Allen Van Gelder, Arist Kojevnikov, Armin Biere, Daniel Le Berre, Dave Tompkins, Eugene Nudelman, Frederic Lardeux, Hantao Zhang, Henry Kautz, Holger Hoos, HoonSang Jin, Ines Lynce, Ivor Spence, Jarrod Roy, Johan Alfredsson, Marijn Heule, Massimo Narizzano, N.S. Narayanaswamy, Niklas Een, Olivier Fourdrinoy, Renato Bruni, Richard Ostrowski, Wheeler Ruml, Xiao Yu Li, Zhaohui Fu)
55 solvers were used (adaptnovelty, brchaff, circus, circush0, circush1, cls, compsat, cquest, eqube1, eqube2, forklift, frankensat-high, frankensat-low, funex, gasat, isat1, isat2, isat3, jerusat1.3, kcnfs, lsatv1.1, march-001, march-007, march-eq-010, march-eq-100, minilearning.jar, modoc, nanosat, novelty35, novelty50, oepira, oepirb, oepirc, ofsat, qingting, quantor, rsaps, saprover, saps, sapsnr, sato4.2, sato4.3, satzilla, satzilla_nr, satzilla_r, satzoo_1.02, tts-2-0, unitwalk, walksatauto, walksatmp, walksatskc, werewolf, wllsatv1, zchaff, zchaff_rand)
2 clusters were used (here in Orsay and one in Vancouver)
516 CPU days elapsed (459 in Orsay, 57 in Vancouver) in more that 60,000 launchs

Some remarks...

Buggy solvers are solvers that answered at least one time "UNSAT" on a proved SAT instance. Such solvers were (after checking with their authors) discarded from the official contest. However, some results on this web site still contain references to these solvers, but, please do notice that, in such cases, we only consider SAT (certified by our certificate-checker) answer of these solvers when results also use hors-concours solvers. In a few words, buggy solvers can be considered in some cases as "incomplete hors-concours" solvers in some pages of this web site. In addition, these results are only indicative and are not in the "official parts" of the results.
We had a major conflict between the "no black box rule" and the "previous winner" rule. ForkLift was previous year winner and a black box (bad luck). So we decided to run it as an hors-concours solver only, awarding the first non-black box solvers in each category.
In the random category, we suspect that the incomplete solvers have found all SAT benchmarks during the first stage (exactly 150 SAT benchmarks over 300... Which is (incredibly) exactly what the theory says). All formulas status were unknown at the beginning of the contest. Thus, there were probably no more SAT formula for the second stage, according to our (strict) rules. We decided, with the judges, to consider in the random category, for the second stage, that all benchmarks should enter. Thus, the TOP-N solvers (in the random category) were launched on all the benchmarks on which they failed during the first stage. This gave us the ranking for awarding the solvers in this category. Next year, the rules will change, to take this problem into account.

Final results of the contest (June, 2003)

And finally, after months (and may be years :-)) of suspens, the winners are:

Industrial category
- Award for the best solver on SAT benchmark: Jerusat 1.3 by Nadel Alexander
- Award for the best solver on UNSAT benchmark: zChaff 2004 by Zhaohui Fu and Yogesh Mahajan
- Award for the best solver on ALL (SAT+UNSAT) benchmark: zChaff 2004 by Zhaohui Fu and Yogesh Mahaja
Crafted category
- Award for the best solver on SAT benchmark: None (last year winner Satzoo by Niklas Een)
- Award for the best solver on UNSAT benchmark: March-eq (by Marijn Heule and Hans van Maaren)
- Award for the best solver on ALL (SAT+UNSAT) benchmark: March-eq (by Marijn Heule and Hans van Maaren)
Random category
- Award for the best solver on SAT benchmark: Adaptnovelty by Holger Hoos and Dave Tompkins
- Award for the best solver on UNSAT benchmark: None (last year winner Kcnfs by Gilles Dequen and Olivier Dubois)
- Award for the best solver on ALL (SAT+UNSAT) benchmark: Adaptnovelty by Holger Hoos and Dave Tompkins

Here are the results for all the solvers that entered the second stage (last update: June, 2004):

Solver	#Solved
Industrial (All)

zchaff_rand

Satzoo_1.02

brchaff

Jerusat1.3

quantor

CQuest

CirCUsH1

minilearning

compsat

Solver	#Solved
Industrial (SAT)

Jerusat1.3

CirCUsH1

zchaff_rand

brchaff

compsat

Satzoo_1.02

Solver	#Solved
Industrial (UNSAT)

zchaff_rand

Satzoo_1.02

brchaff

quantor

CQuest

minilearning

Jerusat1.3

compsat

CirCUsH1

Solver	#Solved
Crafted (ALL)
march-eq-100	10
Satzoo_1.02	10
satzilla_nr	3
Jerusat1.3	2
OepirA	2
brchaff	1
nanosat	1

Solver	#Solved
Crafted (SAT)
Satzoo_1.02	2
brchaff	1
nanosat	1

Solver	#Solved
Crafted (UNSAT)
march-eq-100	10
Satzoo_1.02	8
satzilla_nr	3
Jerusat1.3	2
OepirA	2

Solver	#Solved	#New Solved
Random (ALL)
adaptnovelty	150	7
saps	148	4
walksatrnp	145	3
gasat	128	17
qingting	113	2
unitwalk	112	6
satzilla_nr	110	2
kcnfs	90	30
cls	78	13
march-007	63	18

Solver	#Solved	#New Solved
Random (SAT)
adaptnovelty	150	7
saps	148	4
walksatrnp	145	3
GaSAT	128	17
QingTing	113	2
UnitWalk	112	6
satzilla_nr	110	2
cls	78	13
kcnfs	78	18
march-007	45	9

Solver	#Solved	#New Solved
Random (UNSAT)
kcnfs	26	12
march-007	18	9

The results of the first round, sorted by solver name

All solvers on all categories
Results
All results Random Industrials HandMade
SatSolver Remarks #Series #Benchs #Series #Benchs #Series #Benchs #Series #Benchs
adaptnovelty 36 180 26 143 1 1 9 36
brchaff 42 111 5 11 25 58 12 42
CirCUs 31 89 0 0 24 52 7 37
CirCUsH0 31 87 0 0 24 54 7 33
CirCUsH1 31 89 0 0 25 53 6 36
cls 25 89 19 65 3 8 3 16
compsat 34 91 2 3 23 57 9 31
CQuest 32 85 1 5 22 45 9 35
eqube1 30 76 4 8 17 36 9 32
eqube2 25 61 4 8 13 25 8 28
Forklift 39 124 1 5 30 81 8 38
frankensat-high Incorrect on UNSAT 13 30 1 3 6 7 6 20
frankensat-low Incorrect on UNSAT 14 30 1 3 6 7 7 20
funex 29 70 1 2 20 34 8 34
GaSAT 26 111 26 111 0 0 0 0
ISAT1 4 13 3 12 0 0 1 1
ISAT2 4 15 4 15 0 0 0 0
ISAT3 6 20 5 19 0 0 1 1
Jerusat1.3 32 104 2 3 21 56 9 45
kcnfs 17 82 11 60 0 0 6 22
lsatv1.1 8 30 3 8 0 0 5 22
march-001 32 114 8 41 16 19 8 54
march-007 36 124 9 45 17 20 10 59
march-eq-010 31 114 8 38 11 12 12 64
march-eq-100 34 109 8 29 13 16 13 64
minilearning.jar 32 92 3 9 22 44 7 39
modoc 3 6 0 0 0 0 3 6
nanosat 32 95 2 8 21 48 9 39
novelty35 36 169 27 137 0 0 9 32
novelty50 35 178 26 143 0 0 9 35
OepirA 36 134 2 6 25 87 9 41
OepirB 34 134 1 5 24 92 9 37
OepirC 34 133 1 3 24 95 9 35
ofsat 0 0 0 0 0 0 0 0
QingTing 25 133 19 111 1 1 5 21
quantor 32 71 1 2 21 37 10 32
rsaps 40 186 27 143 3 6 10 37
saprover 19 118 15 103 0 0 4 15
saps 40 186 26 144 3 6 11 36
sapsnr 41 188 27 143 3 6 11 39
sato4.2 24 66 2 10 15 34 7 22
sato4.3 20 45 4 11 9 13 7 21
satzilla 39 171 18 112 10 13 11 46
satzilla_nr 40 168 20 108 9 12 11 48
satzilla_r 39 170 18 111 9 13 12 46
Satzoo_1.02 34 106 3 13 19 40 12 53
tts-2-0 3 11 0 0 0 0 3 11
UnitWalk 21 113 17 106 0 0 4 7
walksatauto 31 168 24 138 0 0 7 30
walksatmp 36 171 27 142 0 0 9 29
walksatskc 30 156 21 122 0 0 9 34
Werewolf 7 22 0 0 0 0 7 22
wllsatv1 10 36 3 10 2 11 5 15
zchaff 39 117 2 11 27 65 10 41
zchaff_rand 36 105 1 5 27 67 8 33
SatSolver Remarks #Series #Benchs #Series #Benchs #Series #Benchs #Series #Benchs
All results Random Industrials HandMade
Results

All solvers on all categories
		Results
		All results	Random	Industrials	HandMade
SatSolver	Remarks	#Series	#Benchs	#Series	#Benchs	#Series	#Benchs	#Series	#Benchs
adaptnovelty		36	180	26	143	1	1	9	36
brchaff		42	111	5	11	25	58	12	42
CirCUs		31	89	0	0	24	52	7	37
CirCUsH0		31	87	0	0	24	54	7	33
CirCUsH1		31	89	0	0	25	53	6	36
cls		25	89	19	65	3	8	3	16
compsat		34	91	2	3	23	57	9	31
CQuest		32	85	1	5	22	45	9	35
eqube1		30	76	4	8	17	36	9	32
eqube2		25	61	4	8	13	25	8	28
Forklift		39	124	1	5	30	81	8	38
frankensat-high	Incorrect on UNSAT	13	30	1	3	6	7	6	20
frankensat-low	Incorrect on UNSAT	14	30	1	3	6	7	7	20
funex		29	70	1	2	20	34	8	34
GaSAT		26	111	26	111	0	0	0	0
ISAT1		4	13	3	12	0	0	1	1
ISAT2		4	15	4	15	0	0	0	0
ISAT3		6	20	5	19	0	0	1	1
Jerusat1.3		32	104	2	3	21	56	9	45
kcnfs		17	82	11	60	0	0	6	22
lsatv1.1		8	30	3	8	0	0	5	22
march-001		32	114	8	41	16	19	8	54
march-007		36	124	9	45	17	20	10	59
march-eq-010		31	114	8	38	11	12	12	64
march-eq-100		34	109	8	29	13	16	13	64
minilearning.jar		32	92	3	9	22	44	7	39
modoc		3	6	0	0	0	0	3	6
nanosat		32	95	2	8	21	48	9	39
novelty35		36	169	27	137	0	0	9	32
novelty50		35	178	26	143	0	0	9	35
OepirA		36	134	2	6	25	87	9	41
OepirB		34	134	1	5	24	92	9	37
OepirC		34	133	1	3	24	95	9	35
ofsat		0	0	0	0	0	0	0	0
QingTing		25	133	19	111	1	1	5	21
quantor		32	71	1	2	21	37	10	32
rsaps		40	186	27	143	3	6	10	37
saprover		19	118	15	103	0	0	4	15
saps		40	186	26	144	3	6	11	36
sapsnr		41	188	27	143	3	6	11	39
sato4.2		24	66	2	10	15	34	7	22
sato4.3		20	45	4	11	9	13	7	21
satzilla		39	171	18	112	10	13	11	46
satzilla_nr		40	168	20	108	9	12	11	48
satzilla_r		39	170	18	111	9	13	12	46
Satzoo_1.02		34	106	3	13	19	40	12	53
tts-2-0		3	11	0	0	0	0	3	11
UnitWalk		21	113	17	106	0	0	4	7
walksatauto		31	168	24	138	0	0	7	30
walksatmp		36	171	27	142	0	0	9	29
walksatskc		30	156	21	122	0	0	9	34
Werewolf		7	22	0	0	0	0	7	22
wllsatv1		10	36	3	10	2	11	5	15
zchaff		39	117	2	11	27	65	10	41
zchaff_rand		36	105	1	5	27	67	8	33
SatSolver	Remarks	#Series	#Benchs	#Series	#Benchs	#Series	#Benchs	#Series	#Benchs
		All results	Random	Industrials	HandMade
		Results

Some nice arrays of results:

You can see for the Random category:

You can see for the Industrial category:

You can see for the Crafted category:

Check them yourself (be a winner)!

You can check the following benchmarks with your own solver... Just to see... They remained unsolved even after the second stage of the contest. They are the two smallest unsolved benchmarks:

hgen8-n260-01-S1597732451 (Unsat, 260 variables, 391 clauses, 888 literals)
hgen2-v450-s41511877 (Sat, 1575 variables, 450 clauses, 4725 literals).

Nice Downloads

The official release of the benchmarks is available! They we'll be moved to satlib asap.

Crafted benchmarks (bzipped tar file, 36MB)
Random benchmarks (bzipped tar file, 11MB)
Industrial benchmarks (bzipped tar file, 2GB)

You can download an array of the first phase results here to do your own analysis. You may find the slides (in pdf) of the presentation given in Vancouver.

Scripts last modified on June, 2004
File generated on 3-08-2005