The VLSAT-1 Benchmark Suite


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 Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

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

3. Contents of the VLSAT-1 benchmark suite

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:

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

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.
August 28, 2021:
Hubert Garavel fixed a few typos in this Web page.
September 02, 2021:
The URL of this Web page changed from "http://cadp.inria.fr/resources/vlsat" to "http://cadp.inria.fr/resources/vlsat/1.html".

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

Back to the CADP Home Page