What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Newsletters Wikipedia
CADP Community
Forum Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

Contents

1. What is the VLSAT-1 benchmark suite?
2. How to use the VLSAT-1 benchmark suite?
3. Contents of the VLSAT-1 benchmark suite
4. History of versions - Contributors

---

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.

[BPG20]

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 (ICATPN'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 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:

• Column 1: Benchmark name, of the form "vlsat_M_N.cnf.bz2", where M is the number variables, and N is the number of clauses.
• Column 2: Number of variables
• Column 3: Number of clauses
• Column 4: Satisfiability of the formula
• Column 5: Size of the CNF file (in bytes)
• Column 6: Size of the CNF file (in bytes)

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.

---

4. History of versions - Contributors

• March 06, 2020:
  Pierre Bouvier and Hubert Garavel published VLSAT-1.

• March 11, 2020:
  The VLSAT-1 benchmark suite now has a DOI: 10.18709/perscido.2020.03.ds300.

• April 07, 2020:
  All VLSAT-1 benchmark files have been renamed: each "vlsat_*" became "vlsat1_*".

• April 11, 2020:
  All VLSAT-1 benchmark files have been renamed: their extension ".dimacs" became ".cnf".

• November 23, 2020:
  An INRIA technical report describing VLSAT-1 was published.

• February 11, 2021:
  An HTTP mirror of the FTP site containing the VLSAT-1 benchmark files was set up.

• April 20, 2021:
  The use of "wget" for downloading all the formulas at once was documented.

---

Version 1.28 - Date 2021/04/20 17:00:20

---

Back to the CADP Home Page