The VLSAT-1 Benchmark Suite

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.