The VLSAT-1 Benchmark Suite

Pierre Bouvier and Hubert Garavel

INRIA Technical Report 510, November 2020


This report presents VLSAT-1 (an acronym for "Very Large Boolean SATisfiability problems"), the first part of a benchmark suite to be used in scientific experiments and software competitions addressing SAT-solving issues. VLSAT-1 contains 100 benchmarks of increasing complexity, proposed in DIMACS CNF format under a permissive Creative Commons license. These benchmarks have been used by the 2020 International Competition on Model Counting.

6 pages