The VLSAT-1 Benchmark Suite

Contents

1. What is the VLSAT-1 benchmark suite?

The VLSAT-1 benchmark suite [BG20] (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.

[BG20]
Pierre Bouvier and Hubert Garavel. The VLSAT-1 Benchmark Suite. INRIA Technical Report 510, November 2020.
[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-1 benchmark suite?

The VLSAT-1 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-1 formulas, but one can download all them at once using either FTP: 

   wget "ftp://ftp.inrialpes.fr/pub/vasy/benchmarks/vlsat/vlsat1*"
or HTTPS: 
   wget -r --no-parent -A "vlsat1*" 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-1 benchmark suite

The VLSAT-1 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 size (.cnf) size (.cnf.bz2)
vlsat1_10_17 10 17 Yes 497 370
vlsat1_12_16 12 16 Yes 490 371
vlsat1_14_19 14 19 Yes 515 384
vlsat1_15_23 15 23 Yes 568 395
vlsat1_16_24 16 24 Yes 564 393
vlsat1_18_21 18 21 Yes 535 390
vlsat1_18_49 18 49 Yes 786 422
vlsat1_21_40 21 40 Yes 737 441
vlsat1_24_34 24 34 Yes 690 428
vlsat1_24_56 24 56 Yes 880 478
vlsat1_27_54 27 54 Yes 873 482
vlsat1_28_56 28 56 Yes 872 480
vlsat1_30_58 30 58 Yes 917 502
vlsat1_32_84 32 84 Yes 1179 542
vlsat1_33_116 33 116 Yes 1460 586
vlsat1_35_82 35 82 Yes 1168 550
vlsat1_38_53 38 53 Yes 841 466
vlsat1_40_108 40 108 Yes 1428 615
vlsat1_44_91 44 91 Yes 1270 603
vlsat1_44_167 44 167 Yes 1999 716
vlsat1_48_128 48 128 Yes 1641 660
vlsat1_51_194 51 194 Yes 2228 787
vlsat1_54_99 54 99 Yes 1359 630
vlsat1_54_270 54 270 Yes 2989 921
vlsat1_56_270 56 270 Yes 3025 959
vlsat1_60_178 60 178 Yes 2148 768
vlsat1_64_152 64 152 Yes 1896 775
vlsat1_68_161 68 161 Yes 1992 805
vlsat1_72_186 72 186 Yes 2237 869
vlsat1_75_367 75 367 Yes 3972 1111
vlsat1_80_178 80 178 Yes 2198 844
vlsat1_81_333 81 333 Yes 3690 1152
vlsat1_85_377 85 377 Yes 4134 1193
vlsat1_90_316 90 316 Yes 3530 1137
vlsat1_93_409 93 409 Yes 4392 1307
vlsat1_96_611 96 611 Yes 6338 1598
vlsat1_102_481 102 481 Yes 5125 1365
vlsat1_108_345 108 345 Yes 3958 1219
vlsat1_112_238 112 238 Yes 2944 1030
vlsat1_117_328 117 328 Yes 3924 1203
vlsat1_120_724 120 724 Yes 7871 1796
vlsat1_120_1016 120 1016 Yes 10,888 2434
vlsat1_130_393 130 393 Yes 4549 1221
vlsat1_135_510 135 510 Yes 6043 1680
vlsat1_140_1371 140 1371 Yes 15,043 3066
vlsat1_144_648 144 648 Yes 7406 2054
vlsat1_153_714 153 714 Yes 8393 1994
vlsat1_160_1028 160 1028 Yes 11,591 2572
vlsat1_168_722 168 722 Yes 8375 2247
vlsat1_170_1247 170 1247 Yes 14,013 2491
vlsat1_185_1132 185 1132 Yes 13,022 2809
vlsat1_195_899 195 899 Yes 10,663 2682
vlsat1_196_1092 196 1092 Yes 12,615 3153
vlsat1_210_1275 210 1275 Yes 14,686 3486
vlsat1_222_1477 222 1477 Yes 16,967 3983
vlsat1_228_3437 228 3437 Yes 38,789 6389
vlsat1_240_1624 240 1624 Yes 18,893 4441
vlsat1_252_3132 252 3132 Yes 36,228 7055
vlsat1_264_1474 264 1474 Yes 18,124 3700
vlsat1_272_1898 272 1898 Yes 22,287 5137
vlsat1_288_2066 288 2066 Yes 24,627 5198
vlsat1_304_2782 304 2782 Yes 32,963 5868
vlsat1_315_3608 315 3608 Yes 42,694 7972
vlsat1_336_2394 336 2394 Yes 28,526 6573
vlsat1_354_3239 354 3239 Yes 37,996 8367
vlsat1_378_1893 378 1893 Yes 22,532 5578
vlsat1_400_1580 400 1580 Yes 19,269 3412
vlsat1_402_10189 402 10,189 Yes 117,708 19,691
vlsat1_418_3119 418 3119 Yes 36,737 8384
vlsat1_448_7592 448 7592 Yes 90,075 16,878
vlsat1_476_1523 476 1523 Yes 18,917 4028
vlsat1_496_18680 496 18,680 Yes 216,271 32,283
vlsat1_510_9201 510 9201 Yes 108,509 12,628
vlsat1_584_28218 584 28,218 Yes 328,466 47,800
vlsat1_588_8050 588 8050 Yes 94,221 18,688
vlsat1_652_29387 652 29,387 Yes 347,320 51,017
vlsat1_702_5565 702 5565 Yes 66,400 13,767
vlsat1_735_23842 735 23,842 Yes 278,885 44,888
vlsat1_810_22731 810 22,731 Yes 270,981 33,431
vlsat1_900_15616 900 15,616 Yes 186,737 39,725
vlsat1_992_13641 992 13,641 Yes 162,859 31,370
vlsat1_1104_75598 1104 75,598 Yes 912,550 139,348
vlsat1_1200_31325 1200 31,325 Yes 387,634 66,709
vlsat1_1365_26963 1365 26,963 Yes 340,634 72,491
vlsat1_1600_31240 1600 31,240 Yes 397,849 52,062
vlsat1_1984_60716 1984 60,716 Yes 789,729 151,463
vlsat1_2289_274818 2289 274,818 Yes 3,632,247 783,074
vlsat1_2450_58066 2450 58,066 Yes 764,904 137,452
vlsat1_3480_149734 3480 149,734 Yes 2,026,499 332,653
vlsat1_3920_93576 3920 93,576 Yes 1,263,265 296,255
vlsat1_4114_186615 4114 186,615 Yes 2,544,604 564,386
vlsat1_5184_184104 5184 184,104 Yes 2,511,401 618,190
vlsat1_6954_399521 6954 399,521 Yes 5,496,879 1,368,790
vlsat1_9588_392364 9588 392,364 Yes 5,430,210 1,411,167
vlsat1_14847_1769105 14,847 1,769,105 Yes 25,893,310 6,874,263
vlsat1_15498_838393 15,498 838,393 Yes 12,109,168 3,210,435
vlsat1_22110_2753207 22,110 2,753,207 Yes 41,433,141 10,801,442
vlsat1_49200_7490695 49,200 7,490,695 Yes 116,913,090 29,925,437
vlsat1_227046_49947755 227,046 49,947,755 Yes 853,973,509 195,050,706
vlsat1_4114810_3879649625 4,114,810 3,879,649,625 Yes 1,081,813,586 186,529,307

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

VLSAT-1 dispersion diagram

4. History of versions - Contributors

Version 1.50 - Date 2021/12/21 11:43:00

Back to the CADP Home Page