The VLSAT-2 Benchmark Suite

Contents

1. What is the VLSAT-2 benchmark suite?

The VLSAT-2 benchmark suite (where "VL" stands for "Very Large") is a collection of 100 SAT formulas to be used as benchmarks in scientific experiments and software competitions.

These SAT formulas have been obtained from the automatic conversion [BGP20] into Nested-Unit Petri Nets (NUPNs) [Gar19] of a large collection of Petri nets modelling real-life problems, such as communication protocols and concurrent systems.

For that, a complete tool chain has been developed [BGP20], which expresses the conversion either as a SAT problem, an SMT problem, a graph coloring problem, or a maximum clique problem. When a conversion method involving SAT solving is selected, the tool chain produces standard formulas to be given to any SAT solver.

The VLSAT-2 benchmarks consist of 50 satisfiable formulas and 50 unsatisfiable formulas, which have been carefully selected among a large collection of more than 132,000 formulas produced by the tool chain. We used five SAT solvers (namely, CaDiCal 1.3.0, Kissat 1.0.3, MathSAT 5.6.5, MiniSAT 2.2.0, and Z3 4.8.9) to reject all formulas that can be solved in less than one minute of CPU time by at least one of these solvers, and that can be solved within two hours by each of these solvers (experiments done on a Xeon E5-2630 v4 with 256 GB RAM). We also tried to provide formulas of increasing complexities, with a good compromise between the size of a formula and the time taken by the fastest solver to process this formula.

25% of the VLSAT-2 benchmarks have been selected by the organizers of recent SAT competitions: 7 satisfiable and 7 unsatisfiable formulas have been chosen for the SAT Competition 2020, and 5 satisfiable and 8 unsatisfiable formulas have been chosen for the SAT Competition 2021 [BG21b].

[BG21c]
Pierre Bouvier and Hubert Garavel. The VLSAT-2 Benchmark Suite. INRIA Technical Report 514, September 2021.
[BG21b]
Pierre Bouvier and Hubert Garavel. SAT-Competition Benchmarks Spawning from Concurrency Theory. In Proceedings of SAT Competition 2021 - Solver and Benchmark Descriptions, Report B-2021-1, pages 47-48, University of Helsinki, Department of Computer Science, July 2021.
[BGP20]
Pierre Bouvier, Hubert Garavel, and Hernán Ponce de León. Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. In Proceedings of the 41th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'20), Paris, France, June 2020.
[Gar19]
Hubert Garavel. Nested-Unit Petri Nets. Journal of Logical and Algebraic Methods in Programming, vol. 104, pages 60-85, April 2019.

2. How to use the VLSAT-2 benchmark suite?

The VLSAT-2 formulas are expressed in Conjunctive Normal Form.

Each formula is provided as a separate file, encoded in the DIMACS-CNF format, and then compressed using bzip2.

We do not provide a single archive file containing all the VLSAT-2 formulas, but one can download all them at once using either FTP: 

   wget "ftp://ftp.inrialpes.fr/pub/vasy/benchmarks/vlsat/vlsat2*"
or HTTPS: 
   wget -r --no-parent -A "vlsat2*" https://cadp.inria.fr/ftp/benchmarks/vlsat
With the latter command, the formulas will be put in directory "./cadp.inria.fr/ftp/benchmarks/vlsat".

3. Contents of the VLSAT-2 benchmark suite

The VLSAT-2 benchmarks can be downloaded from the table below. Each row of the table corresponds to one benchmark. The columns of the table contain the following data:

name
(.cnf.bz2)		 #variables #clauses satisfiable competitions difficulty size (.cnf) size (.cnf.bz2)
vlsat2_544_8738 544 8738 No 3 103,128 19,319
vlsat2_600_11440 600 11,440 No 3 135,133 22,237
vlsat2_684_9417 684 9417 No 3 113,357 22,376
vlsat2_684_13953 684 13,953 No 2 167,207 29,054
vlsat2_708_10259 708 10,259 No 3 123,522 24,322
vlsat2_736_11022 736 11,022 No 2 131,680 26,616
vlsat2_798_17543 798 17,543 No 3 208,580 41,591
vlsat2_1000_22250 1000 22,250 Yes 4 266,156 31,829
vlsat2_1022_14955 1022 14,955 No 3 179,549 39,934
vlsat2_1125_15795 1125 15,795 No 3 193,186 37,959
vlsat2_1134_26703 1134 26,703 No 2021 4 325,451 66,161
vlsat2_1155_42917 1155 42,917 No 2021 4 522,584 76,848
vlsat2_1183_26975 1183 26,975 No 3 327,673 70,187
vlsat2_1209_29889 1209 29,889 No 3 366,088 76,265
vlsat2_1326_35956 1326 35,956 No 3 445,250 92,403
vlsat2_1352_42432 1352 42,432 No 3 526,899 107,337
vlsat2_1560_54564 1560 54,564 No 3 692,988 141,344
vlsat2_1586_57751 1586 57,751 No 3 735,662 148,035
vlsat2_2231_68844 2231 68,844 No 2 889,477 179,888
vlsat2_2340_70758 2340 70,758 No 2 918,848 181,298
vlsat2_2403_100259 2403 100,259 No 2 1,318,337 288,693
vlsat2_2548_119204 2548 119,204 No 3 1,575,104 344,403
vlsat2_3252_372331 3252 372,331 No 3 4,975,961 1,121,956
vlsat2_3456_192912 3456 192,912 Yes 2 2,625,512 567,856
vlsat2_3480_190496 3480 190,496 No 3 2,555,096 443,845
vlsat2_4424_545056 4424 545,056 No 2021 3 7,442,595 1,737,375
vlsat2_5152_824642 5152 824,642 No 2021 3 11,211,531 2,715,340
vlsat2_5525_327765 5525 327,765 No 3 4,421,014 1,078,802
vlsat2_5568_1124240 5568 1,124,240 No 3 15,309,882 3,723,913
vlsat2_5600_1042700 5600 1,042,700 No 2021 3 14,218,953 3,478,727
vlsat2_7452_334035 7452 334,035 Yes 3 4,650,927 1,097,941
vlsat2_11130_1186888 11,130 1,186,888 Yes 2021 0 (149 s) 16,668,852 3,945,369
vlsat2_11280_4223777 11,280 4,223,777 No 2021 3 59,310,545 14,492,714
vlsat2_11374_1150943 11,374 1,150,943 Yes 2021 1 (1803 s) 16,245,119 4,244,525
vlsat2_11664_5532624 11,664 5,532,624 No 4 78,058,925 20,649,888
vlsat2_12690_1481522 12,690 1,481,522 Yes 2 21,238,726 5,612,588
vlsat2_14016_1374747 14,016 1,374,747 Yes 4 19,884,641 5,307,674
vlsat2_14280_6781327 14,280 6,781,327 No 2021 3 98,015,994 24,677,623
vlsat2_14424_7585190 14,424 7,585,190 No 2021 4 109,998,942 29,201,546
vlsat2_14637_1778453 14,637 1,778,453 Yes 2 25,930,092 6,909,765
vlsat2_14640_1323246 14,640 1,323,246 No 5 19,067,794 4,273,241
vlsat2_15249_1937993 15,249 1,937,993 Yes 2 28,335,204 7,578,561
vlsat2_15440_1409906 15,440 1,409,906 No 2020 5 20,601,801 4,676,949
vlsat2_15704_1804650 15,704 1,804,650 Yes 3 26,537,952 6,973,131
vlsat2_15960_1464039 15,960 1,464,039 No 2020 5 21,455,438 4,883,223
vlsat2_16269_2203672 16,269 2,203,672 Yes 3 32,441,569 8,700,470
vlsat2_16297_1562268 16,297 1,562,268 No 5 22,876,222 6,059,485
vlsat2_16676_1598591 16,676 1,598,591 Yes 2020 2 23,472,063 6,207,328
vlsat2_16788_9021307 16,788 9,021,307 No 3 132,557,263 35,550,378
vlsat2_17688_1741702 17,688 1,741,702 No 5 25,707,421 6,828,454
vlsat2_18250_2995915 18,250 2,995,915 Yes 2 44,628,896 9,925,321
vlsat2_19565_3665001 19,565 3,665,001 Yes 2 54,951,575 14,875,900
vlsat2_20424_2157568 20,424 2,157,568 No 5 32,269,453 8,637,701
vlsat2_21114_2240429 21,114 2,240,429 No 2020 5 33,603,637 9,009,594
vlsat2_21190_2597791 21,190 2,597,791 Yes 3 39,475,185 10,130,016
vlsat2_21546_2615351 21,546 2,615,351 Yes 3 39,304,100 10,749,665
vlsat2_21573_2289124 21,573 2,289,124 Yes 3 34,385,201 9,221,951
vlsat2_22032_3022731 22,032 3,022,731 Yes 2 45,544,328 12,317,757
vlsat2_23961_2714844 23,961 2,714,844 No 5 41,056,605 11,071,241
vlsat2_24450_2770239 24,450 2,770,239 Yes 2020 1 (721 s) 41,946,322 9,668,057
vlsat2_26104_3131630 26,104 3,131,630 No 5 47,619,531 12,815,904
vlsat2_26606_3191844 26,606 3,191,844 Yes 2 48,609,631 13,112,154
vlsat2_26988_3251923 26,988 3,251,923 No 5 49,551,699 13,333,811
vlsat2_27507_3314450 27,507 3,314,450 Yes 3 50,571,233 13,623,887
vlsat2_28930_6497511 28,930 6,497,511 Yes 4 99,265,442 26,583,542
vlsat2_29040_3874024 29,040 3,874,024 Yes 2 57,652,741 14,214,635
vlsat2_29205_3712921 29,205 3,712,921 No 5 56,839,848 14,845,666
vlsat2_29456_6615638 29,456 6,615,638 Yes 2 101,163,429 27,959,639
vlsat2_29736_3780419 29,736 3,780,419 Yes 2021 2 57,914,686 15,634,864
vlsat2_29945_3796274 29,945 3,796,274 Yes 4 58,092,719 15,892,830
vlsat2_30195_3855554 30,195 3,855,554 No 2020 5 59,090,523 15,400,229
vlsat2_30744_3925645 30,744 3,925,645 Yes 2020 5 60,212,560 16,262,069
vlsat2_31552_5400750 31,552 5,400,750 Yes 4 82,890,808 22,771,957
vlsat2_32480_4362044 32,480 4,362,044 No 2020 5 67,074,994 18,145,707
vlsat2_33040_4437242 33,040 4,437,242 Yes 4 68,294,318 18,571,082
vlsat2_33582_4529625 33,582 4,529,625 No 5 69,738,548 18,890,409
vlsat2_34099_4695729 34,099 4,695,729 Yes 3 72,436,687 19,844,403
vlsat2_34161_4607712 34,161 4,607,712 Yes 2020 4 70,973,369 19,255,906
vlsat2_35929_5082743 35,929 5,082,743 No 2020 5 78,503,883 21,488,665
vlsat2_36518_5166057 36,518 5,166,057 Yes 4 79,874,314 21,717,488
vlsat2_36603_5137412 36,603 5,137,412 Yes 3 79,577,444 21,786,831
vlsat2_36792_5273558 36,792 5,273,558 Yes 2 81,508,355 22,335,704
vlsat2_37758_5364539 37,758 5,364,539 Yes 2020, 2021 4 83,034,177 22,535,124
vlsat2_39552_5878762 39,552 5,878,762 No 2020 5 91,146,414 24,701,537
vlsat2_40170_5970608 40,170 5,970,608 Yes 2020 5 92,604,219 24,315,257
vlsat2_40896_6104639 40,896 6,104,639 No 5 94,715,376 25,675,449
vlsat2_41535_6200014 41,535 6,200,014 Yes 4 96,258,394 25,275,136
vlsat2_41875_6420498 41,875 6,420,498 Yes 4 99,989,870 27,421,704
vlsat2_45150_7165285 45,150 7,165,285 Yes 4 111,825,248 28,452,556
vlsat2_46440_7369989 46,440 7,369,989 Yes 2 115,133,192 31,539,411
vlsat2_47817_1337056 47,817 1,337,056 Yes 2 21,200,670 5,771,789
vlsat2_57038_10572502 57,038 10,572,502 Yes 2020 5 165,941,588 45,805,427
vlsat2_58380_10775711 58,380 10,775,711 Yes 4 169,155,895 46,530,946
vlsat2_59204_10973962 59,204 10,973,962 Yes 4 172,369,127 47,341,291
vlsat2_67996_13708722 67,996 13,708,722 Yes 5 215,955,109 58,856,459
vlsat2_68760_13862744 68,760 13,862,744 Yes 5 218,414,167 56,276,323
vlsat2_69524_14016766 69,524 14,016,766 Yes 5 220,874,192 60,131,742
vlsat2_70288_14170788 70,288 14,170,788 Yes 2021 4 223,343,005 60,633,415
vlsat2_71816_14478832 71,816 14,478,832 Yes 3 228,310,698 61,904,292
vlsat2_83334_20350783 83,334 20,350,783 Yes 4 323,680,106 84,174,162

The diagram below illustrates the dispersion of the VLSAT-2 benchmarks. To improve the diagram readability, both axis are represented with a logarithmic scale.

VLSAT-2 dispersion diagram

4. History of versions - Contributors

Version 1.44 - Date 2021/12/21 11:43:10

Back to the CADP Home Page