The VLSAT-3 Benchmark Suite
share
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 experimentsand 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 formulasof increasing complexity, proposed in SMT-LIB format under a permissive Creative Commons license.More than 90 during the 16th International Satisfiability Modulo TheoriesCompetition (SMT-COMP 2021).
READ FULL TEXT