The VLSAT-3 Benchmark Suite
Data Structures and Algorithms
2021-12-10 v1 Formal Languages and Automata Theory
Symbolic Computation
Abstract
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% of these benchmarks have been used during the 16th International Satisfiability Modulo TheoriesCompetition (SMT-COMP~2021).
Keywords
Cite
@article{arxiv.2112.03675,
title = {The VLSAT-3 Benchmark Suite},
author = {Pierre Bouvier},
journal= {arXiv preprint arXiv:2112.03675},
year = {2021}
}
Comments
arXiv admin note: text overlap with arXiv:2011.11049, arXiv:2110.06336