TL;DR
The VLSAT-3 benchmark suite provides a large collection of complex SAT and SMT problems, facilitating evaluation and development of solving algorithms in scientific and competitive contexts.
Contribution
It introduces VLSAT-3, a new benchmark suite with 1200 diverse quantifier-free first-order logic formulas for SAT and SMT solving research.
Findings
Over 90% of benchmarks used in SMT-COMP 2021
Contains 600 satisfiable and 600 unsatisfiable formulas
Includes formulas of increasing complexity
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).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.