Next: Benchmarks
Up: The results
Previous: First stage
In this stage, Top 5 solvers were run on smallest remaining unsolved
instances for 6 hours. For industrial benchmarks, only 31 instances
remained unsolved. So, we used all of them for complete solvers, and
only satisfiable instances for all solvers. Thus, in Table
4, berkmin, OKsolver, 2clseq, simo and
zchaff were launched on all instances. unitwalk was only launched on
all instances that were not known to be unsatisfiable. Over the 31
instances, only 15 were solved. One can notice that, surprisingly,
berkmin and 2clseq are able to solve comb/comb3 instance in less than
2000s. This benchmark was not solved during the first stage of the
competition (recall that cpu cutoff was 2400s on the same machines),
due to the use of our launchheuristic (comb1 and comb2 are still
unsolved, and considered as easiest by the heuristic). Let us also
notice how zchaff seems welltuned for this category: it is able to
solve instances with billions of literals.
Table 4:
Industrial benchmarks used for the second stage. ``N'',
in the ``SAT?'' colmun, denotes a previouslyUnknown benchmark
claimed to be Unsat (recall that no proof were given, and solver have
to be trusted on this answer). All fpgar/file are
fpgarouting/k2fix_gr_file, 6pipe_o for 6pipe_6_ooo, and
satexc/cnfr4i for satexchallenges/cnfr4b1k1.icomp.
Name 
Nb Var 
Nb Clauses 
Length(Max) 
SAT? 
Solved by 
Homer/homer17 
286 
1 742 
3 718 (12) 
N 
limmat (6957s) 
Homer/homer18 
308 
2 030 
4 312 (12) 
N 

Homer/homer19 
330 
2 340 
4 950 (12) 
N 

Homer/homer20 
440 
4 220 
8 800 (12) 
N 

dinphil/dp11u10 
9 197 
25 271 
59 561 (12) 
N 

dinphil/dp12u11 
11 137 
30 792 
72 531 (13) 
N 

comb/comb1 
5 910 
16 804 
38 654 (29) 
 

comb/comb2 
31 933 
112 462 
274 030 (14) 
 

comb/comb3 
4 774 
16 331 
39 495 (14) 
N 

f2clk/f2clk_40 
27 568 
80 439 
186 255 (26) 
 

f2clk/f2clk_50 
34 678 
101 319 
234 655 (26) 
 

fifo8/fifo8_300 
194 762 
530 713 
1 200 865 (12) 
N 
zchaff (5716s) 
fifo8/fifo8_400 
259 762 
707 913 
1 601 865 (12) 
N 
zchaff (16083s) 
ip/ip36 
47 273 
153 368 
366 122 (21) 
N 

ip/ip38 
49 967 
162 142 
387 080 (21) 
N 

ip/ip50 
66 131 
214 786 
512 828 (21) 
 

w08/w08_14 
120 367 
425 316 
1 038 230 (16) 
Y 
zchaff (16359s) 
w08/w08_15 
132 555 
469 519 
1 146 761 (16) 
 

bmc2/cnt10 
20 470 
68 561 
187 229 (4) 
Y 

fpgar/2pinvar_w8 
3 771 
270 136 
1 620 816 (7) 
 

fpgar/2pinvar_w9 
5 028 
307 674 
2 438 766 (9) 
 

fpgar/2pin_w8 
9 882 
295 998 
1 727 100 (7) 
 

fpgar/2pin_w9 
13 176 
345 426 
2 606 340 (9) 
 

fpgar/rcs_w8 
10 056 
271 393 
550 328 (9) 
 

satexc/cnfr41 
2 424 
14 812 
39 764 (25) 
Y 

satexc/cnfr42 
2 424 
14 812 
39 764 (25) 
Y 
limmat (20454) 
fvpunsat/6pipe 
15 800 
394 739 
1 157 225 (116) 
N 
zchaff (12714s) 
fvpunsat/6pipe_o 
17 064 
545 612 
1 608 428 (188) 
N 
zchaff (4398s) 
fvpunsat/7pipe 
23 910 
751 118 
2 211 468 (146) 
N 

sha/sha1 
61 377 
255 417 
769 041 (5) 
Y 

sha/sha2 
61 377 
255 417 
769 041 (5) 
Y 


Table 5:
Handmade benchmarks used for the second stage. pbu and pbs
are pyhalabraununsat and pyhalabraunsat
respectively. Comp/Un. denotes which solvers were used: ``C'' means
that we tried berkmin, OKsolver, 2clseq, limmat and zchaff on the
considered benchmark. ``U'' means that unitwalk was also launched
(see previous section for the Top 5 in Handmade category) and note
that berkmin, OKsolver, limmat and zchaff where common in both
Complete/All categories.
Name 
Nb Var 
Nb Cl. 
Len. 
SAT? 
Comp/Un. 
Solved by 
urq/urq3_25bis 
99 
264 
792 (4) 
N 
C 
berkmin (2825s) 
xorchain/x1_36 
106 
282 
844 (4) 
N 
C 

xorchain/x1.1_40 
118 
314 
940 (4) 
N 
C 

xorchain/x1_40 
118 
314 
940 (4) 
N 
C 
zchaff (3165s) 
xorchain/x2_40 
118 
314 
940 (4) 
N 
C 

xorchain/x1.1_44 
130 
346 
1 036 (4) 
N 
C 

xorchain/x2_44 
130 
346 
1 036 (4) 
N 
C 

urq/urq3_25 
153 
408 
1 224 (4) 
N 
C 

urq/urq4_25bis 
192 
512 
1 536 (4) 
N 
C 

urq/urqu4_25 
288 
768 
2 304 (4) 
N 
C 

matrix/Mat26 
744 
2 464 
6 432 (4) 
N 
C 
zchaff (18604s) 
satexc/par322c 
1 303 
5 206 
15 246 (4) 
Y 
C,U 

satexc/par321c 
1 315 
5 254 
15 390 (4) 
Y 
C,U 

Lisa/lisa21_99_a 
1 453 
7 967 
26 577 (23) 
Y 
C,U 
berkmin (20459s) 
satexc/par322 
3 176 
10 253 
27 405 (4) 
Y 
C,U 

satexc/par321 
3 176 
10 277 
27 501 (4) 
Y 
C,U 

pbu4/pbu35403 
7 383 
24 320 
62 950 (4) 
N 
C 

pbs4/pbs40403 
9 638 
31 795 
82 345 (4) 
Y 
C,U 

pbs4/pbs40404 
9 638 
31 795 
82 345 (4) 
Y 
C,U 
zchaff (3182s) 
pbu4/pbu40401 
9 638 
31 795 
82 345 (4) 
N 
C 

hanoi/hanoi6 
4 968 
39 666 
98 346 (10) 
Y 
C,U 
berkmin (2551s) 
matrix/Mat317 
24 435 
85 050 
227 610 (4) 
 
C,U 


Table 6:
Random benchmarks used for the second stage. Clause max
length is not reported (it is exactly 4 for all benchmarks). Comp is
``C'' if 2clseq, OKsolver, marchII, marchIIse and rb2cl were
launched; and ``U'' if dlmsat[13], unitwalk and OKsolver were
launched (see previous section for Top 5 solvers and random
instances).
Name 
Nb Var 
Nb Cl. 
Len. 
SAT? 
Comp/Un. 
Solved by 
hgen3v300s1766565160 
300 
1 050 
3 150 
 
C 

hgen3v300s1817652174 
300 
1 050 
3 150 
 
C 

hgen3v300s229883414 
300 
1 050 
3 150 
 
C 

hgen3v350s1711636364 
350 
1 225 
3 675 
 
C 

hgen3v350s524562458 
350 
1 225 
3 675 
 
C 

hgen2v400s161064952 
400 
1 400 
4 200 
Y 
C,U 
unitwalk (20199s) 
hgen3v400s344840348 
400 
1 400 
4 200 
 
C 

hgen3v400s553296708 
400 
1 400 
4 200 
 
C 

hgen2v450s41511877 
450 
1 575 
4 725 
Y 
C,U 
dlmsat3 (94s) 
hgen3v450s432353833 
450 
1 575 
4 725 
 
C 

unifc1700v400s734590802 
400 
1 700 
5 100 
 
C 

okgenc1700v400s2038016593 
400 
1 700 
5 100 
 
C 

hgen2v500s1216665065 
500 
1 750 
5 250 
Y 
C,U 

hgen3v500s1349121860 
500 
1 750 
5 250 
 
C 

hgen3v500s1769527644 
500 
1 750 
5 250 
 
C 

hgen3v500s1803930514 
500 
1 750 
5 250 
 
C 

hgen3v500s1920280160 
500 
1 750 
5 250 
 
C 

glassybpv399s382874052 
399 
1 862 
5 586 
Y 
C,U 

glassybpv399s499089820 
399 
1 862 
5 586 
Y 
C,U 

glassybv399s500582891 
399 
1 862 
5 586 
Y 
C,U 
OKsolver (13834s) 
glassybv399s732524269 
399 
1 862 
5 586 
Y 
U 
OKsolver(8558s) 
glassyv450s1188040332 
450 
2 100 
6 300 
Y 
U 
OKsolver (15444s) 
glassyv450s1679149003 
450 
2 100 
6 300 
Y 
U 
OKsolver (18766s) 
glassyv450s1878038564 
450 
2 100 
6 300 
Y 
U 

glassyv450s2052978189 
450 
2 100 
6 300 
Y 
U 

glassyv450s325799114 
450 
2 100 
6 300 
Y 
U 

glassybpv450s1173211014 
450 
2 100 
6 300 
Y 
U 

glassybpv450s1349090995 
450 
2 100 
6 300 
Y 
U 

glassybpv450s1976869020 
450 
2 100 
6 300 
Y 
U 

glassybpv450s2092286542 
450 
2 100 
6 300 
Y 
U 

glassybpv450s40966008 
450 
2 100 
6 300 
Y 
U 

glassybv450s1529438294 
450 
2 100 
6 300 
Y 
U 

glassybv450s1709573704 
450 
2 100 
6 300 
Y 
U 

glassybv450s1729975696 
450 
2 100 
6 300 
Y 
U 


For handmade instances (Table 5), only a few
families remained (but several instances per family) so we took the
smallest 2 SAT+UNSAT instances in each family for complete solvers,
and 2 smallest SAT benchmarks in each family for all solvers
(families are urq/urq*bis, urq/urq, xorchain/x1_*,
xorchain/x1.1_*, xorchain/x2_*, matrix, Lisa, satexc/par32*c,
satexc/par32, pbu4, pbs4 and hanoi). One can notice that the only
incomplete solver used in this stage (i.e., uniwalk) was not able to
solve any instance during this stage. Let us just recall that most
instances in this table are easy for lsat (xorchains, urq, par32),
which was horsconcours.
The selection of random benchmarks was guided by the following
considerations: the smallest unsolved unsatisfiable instance had
already been found in the
handmade category (the smallest unsolved random instance
was larger than it). Concerning SAT instances, all the SAT
instances in the industrial and handmade categories were tested for
the second stage and the smallest unsolved one had 82 345 literals
(handmade pbs4 instance).
One feature of random category is that most instances are unknown.
So, to be sure to award the smallest SAT instance, we needed to keep
the smallest instances for the second stage, independently of their
series.
As a consequence, if all the series were present in that second
stage, the number of instances per series varied.
Table 6 shows all the results for randomly
generated instances, sorted by their respective length. Note that all
solved instances were previously known as SAT (by forcedSAT
generators).
We finally give as summary of results, in Tables
7, 8 and
9. The leftmost number denotes the total number
of instances solved during the second stage. Rightmost numbers (if
any) denote the 1st stage result (number of solved series and total
number of instances solved to break ties).
Table 7:
Second stage results on industrial benchmarks (summary)
Complete solvers 
All solvers on satisfiable benchmarks 
7 
zchaff 
2 
limmat 

5 
limmat 
1 
zchaff 
[11] 
2 
berkmin 
1 
berkmin 
[8] 
1 
2clseq 
0 
simo 
[7] 
0 
simo 
0 
unitwalk 
[6] 

Table 8:
Second stage results on handmade benchmarks (summary)
Complete solvers 
All solvers on satisfiable benchmarks 
3 
zchaff 

2 
berkmin 
[11] 
2 
berkmin 

2 
zchaff 
[10] 
1 
OKsolver 
[20] 
1 
OKsolver 
[11] 
1 
limmat 
[19 140] 
1 
limmat 
[10] 
1 
2clseq 
[19 126] 
0 
unitwalk 


Table 9:
Second stage results on randomly generated benchmarks (summary)
Complete solvers 
All solvers on satisfiable benchmarks 
4 
OKsolver 

5 
OKsolver 

3 
march2, march2se 

1 
dlmsat3 
[23] 
0 
2clseq 
[34] 
1 
unitwalk 
[22] 
0 
rb2cl 
[31] 
0 
dlmsat1, dlmsat2 


Next: Benchmarks
Up: The results
Previous: First stage
LE BERRE Daniel
20020916