The VLSAT-3 Benchmark Suite

Pierre Bouvier

INRIA Technical Report 516, December 2021


This report presents VLSAT-3 (an acronym for ``Very Large Boolean SATisfiability problems''), the third part of a benchmark suite to be used in scientific experiments and software competitions addressing SAT and SMT (Satisfiability Modulo Theories) solving issues. VLSAT-3 contains 1200 (600 satisfiable and 600 unsatisfiable) quantifier-free first-order logic formulas of increasing complexity, proposed in SMT-LIB format under a permissive Creative Commons license. More than 90% of these benchmarks have been used during the 16th International Satisfiability Modulo Theories Competition (SMT-COMP 2021).

20 pages