Skip to Main content Skip to Navigation
Reports

The VLSAT-2 Benchmark Suite

Pierre Bouvier 1 Hubert Garavel 1 
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This report presents VLSAT-2 (an acronym for "Very Large Boolean SATisfiability problems"), the second part of a benchmark suite to be used in scientific experiments and software competitions addressing SAT-solving issues. VLSAT-2 contains 100 benchmarks (50 satisfiable and 50 unsatisfiable formulas) of increasing complexity, proposed in DIMACS CNF format under a permissive Creative Commons license. 25% of these benchmarks have been used during the 2020 and 2021 editions of the International SAT Competition.
Complete list of metadata

https://hal.inria.fr/hal-03337115
Contributor : Pierre Bouvier Connect in order to contact the contributor
Submitted on : Tuesday, September 7, 2021 - 3:56:16 PM
Last modification on : Wednesday, July 6, 2022 - 4:14:43 AM
Long-term archiving on: : Wednesday, December 8, 2021 - 7:58:46 PM

Files

RT-0514.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03337115, version 1

Citation

Pierre Bouvier, Hubert Garavel. The VLSAT-2 Benchmark Suite. [Technical Report] RT-0514, INRIA Grenoble Rhône-Alpes. 2021, pp.1-8. ⟨hal-03337115⟩

Share

Metrics

Record views

97

Files downloads

52