The VLSAT-2 Benchmark Suite

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.