The VLSAT-2 (Very Large SAT) 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 into Nested-Unit Petri Nets (NUPNs) of a large collection of Petri nets modelling real-life problems, such as communication protocols and concurrent systems. 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.