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 cut-off was 2400s on the same machines),
due to the use of our launch-heuristic (comb1 and comb2 are still
unsolved, and considered as easiest by the heuristic). Let us also
notice how zchaff seems well-tuned 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 previously-Unknown benchmark
claimed to be Unsat (recall that no proof were given, and solver have
to be trusted on this answer). All fpga-r/file are
fpga-routing/k2fix_gr_file, 6pipe_o for 6pipe_6_ooo, and
satex-c/cnf-r4-i for satex-challenges/cnf-r4-b1-k1.i-comp.
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 |
|
fpga-r/2pinvar_w8 |
3 771 |
270 136 |
1 620 816 (7) |
- |
|
fpga-r/2pinvar_w9 |
5 028 |
307 674 |
2 438 766 (9) |
- |
|
fpga-r/2pin_w8 |
9 882 |
295 998 |
1 727 100 (7) |
- |
|
fpga-r/2pin_w9 |
13 176 |
345 426 |
2 606 340 (9) |
- |
|
fpga-r/rcs_w8 |
10 056 |
271 393 |
550 328 (9) |
- |
|
satex-c/cnf-r4-1 |
2 424 |
14 812 |
39 764 (25) |
Y |
|
satex-c/cnf-r4-2 |
2 424 |
14 812 |
39 764 (25) |
Y |
limmat (20454) |
fvp-unsat/6pipe |
15 800 |
394 739 |
1 157 225 (116) |
N |
zchaff (12714s) |
fvp-unsat/6pipe_o |
17 064 |
545 612 |
1 608 428 (188) |
N |
zchaff (4398s) |
fvp-unsat/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 pyhala-braun-unsat and pyhala-braun-sat
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) |
xor-chain/x1_36 |
106 |
282 |
844 (4) |
N |
C |
|
xor-chain/x1.1_40 |
118 |
314 |
940 (4) |
N |
C |
|
xor-chain/x1_40 |
118 |
314 |
940 (4) |
N |
C |
zchaff (3165s) |
xor-chain/x2_40 |
118 |
314 |
940 (4) |
N |
C |
|
xor-chain/x1.1_44 |
130 |
346 |
1 036 (4) |
N |
C |
|
xor-chain/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) |
satex-c/par32-2-c |
1 303 |
5 206 |
15 246 (4) |
Y |
C,U |
|
satex-c/par32-1-c |
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) |
satex-c/par32-2 |
3 176 |
10 253 |
27 405 (4) |
Y |
C,U |
|
satex-c/par32-1 |
3 176 |
10 277 |
27 501 (4) |
Y |
C,U |
|
pbu-4/p-b-u-35-4-03 |
7 383 |
24 320 |
62 950 (4) |
N |
C |
|
pbs-4/p-b-s-40-4-03 |
9 638 |
31 795 |
82 345 (4) |
Y |
C,U |
|
pbs-4/p-b-s-40-4-04 |
9 638 |
31 795 |
82 345 (4) |
Y |
C,U |
zchaff (3182s) |
pbu-4/p-b-u-40-4-01 |
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[1-3], 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 |
hgen3-v300-s1766565160 |
300 |
1 050 |
3 150 |
- |
C |
|
hgen3-v300-s1817652174 |
300 |
1 050 |
3 150 |
- |
C |
|
hgen3-v300-s229883414 |
300 |
1 050 |
3 150 |
- |
C |
|
hgen3-v350-s1711636364 |
350 |
1 225 |
3 675 |
- |
C |
|
hgen3-v350-s524562458 |
350 |
1 225 |
3 675 |
- |
C |
|
hgen2-v400-s161064952 |
400 |
1 400 |
4 200 |
Y |
C,U |
unitwalk (20199s) |
hgen3-v400-s344840348 |
400 |
1 400 |
4 200 |
- |
C |
|
hgen3-v400-s553296708 |
400 |
1 400 |
4 200 |
- |
C |
|
hgen2-v450-s41511877 |
450 |
1 575 |
4 725 |
Y |
C,U |
dlmsat3 (94s) |
hgen3-v450-s432353833 |
450 |
1 575 |
4 725 |
- |
C |
|
unif-c1700-v400-s734590802 |
400 |
1 700 |
5 100 |
- |
C |
|
okgen-c1700-v400-s2038016593 |
400 |
1 700 |
5 100 |
- |
C |
|
hgen2-v500-s1216665065 |
500 |
1 750 |
5 250 |
Y |
C,U |
|
hgen3-v500-s1349121860 |
500 |
1 750 |
5 250 |
- |
C |
|
hgen3-v500-s1769527644 |
500 |
1 750 |
5 250 |
- |
C |
|
hgen3-v500-s1803930514 |
500 |
1 750 |
5 250 |
- |
C |
|
hgen3-v500-s1920280160 |
500 |
1 750 |
5 250 |
- |
C |
|
glassybp-v399-s382874052 |
399 |
1 862 |
5 586 |
Y |
C,U |
|
glassybp-v399-s499089820 |
399 |
1 862 |
5 586 |
Y |
C,U |
|
glassyb-v399-s500582891 |
399 |
1 862 |
5 586 |
Y |
C,U |
OKsolver (13834s) |
glassyb-v399-s732524269 |
399 |
1 862 |
5 586 |
Y |
U |
OKsolver(8558s) |
glassy-v450-s1188040332 |
450 |
2 100 |
6 300 |
Y |
U |
OKsolver (15444s) |
glassy-v450-s1679149003 |
450 |
2 100 |
6 300 |
Y |
U |
OKsolver (18766s) |
glassy-v450-s1878038564 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassy-v450-s2052978189 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassy-v450-s325799114 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassybp-v450-s1173211014 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassybp-v450-s1349090995 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassybp-v450-s1976869020 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassybp-v450-s2092286542 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassybp-v450-s40966008 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassyb-v450-s1529438294 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassyb-v450-s1709573704 |
450 |
2 100 |
6 300 |
Y |
U |
|
glassyb-v450-s1729975696 |
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, xor-chain/x1_*,
xor-chain/x1.1_*, xor-chain/x2_*, matrix, Lisa, satex-c/par32-*-c,
satex-c/par32, pbu-4, pbs-4 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 (xor-chains, urq, par32),
which was hors-concours.
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 forced-SAT
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 hand-made 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
2002-09-16