next up previous
Next: Benchmarks Up: The results Previous: First stage

Second 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$ ^{*}$ \begin{displaymath}\begin{cases}\text{berkmin (1025s)}\\ \text{2clseq (1772s)}\end{cases}\end{displaymath}
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$ ^{*}$ \begin{displaymath}\begin{cases}\text{limmat (20919s)}\\ \text{zchaff (6982s)}\end{cases}\end{displaymath}
ip/ip38 49 967 162 142 387 080 (21) N$ ^{*}$ \begin{displaymath}\begin{cases}\text{limmat(5640s)}\\ \text{zchaff (13217s)}\end{cases}\end{displaymath}
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 \begin{displaymath}\begin{cases}\text{limmat (21339s)}\\ \text{berkmin (13071s)}\end{cases}\end{displaymath}
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 \begin{displaymath}\begin{cases}\text{berkmin (3693s)}\\ \text{OKsolver (3073s)}...
...1s)}\\ \text{limmat (4718s)}\\ \text{zchaff (2738s)}\end{cases}\end{displaymath}
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 \begin{displaymath}\begin{cases}\text{OKsolver (13034s)}\\ \text{marchII (7100s)}\\ \text{marchIIse (7064s)}\end{cases}\end{displaymath}
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 up previous
Next: Benchmarks Up: The results Previous: First stage
LE BERRE Daniel 2002-09-16