The VLSAT-1 Benchmark Suite
Pierre Bouvier (CONVECS), Hubert Garavel (CONVECS)
TL;DR
VLSAT-1 is a benchmark suite of 100 complex Boolean SAT problems designed for evaluating SAT solvers, used in competitions and scientific experiments to advance the field.
Contribution
It introduces the first part of a large benchmark suite with diverse complexity, supporting research and development in SAT-solving.
Findings
Benchmarks used in 2020 International Competition on Model Counting
Contains 100 DIMACS CNF format problems of increasing complexity
Supports scientific experiments and software competitions in SAT solving
Abstract
This report presents VLSAT-1 (an acronym for "Very Large Boolean SATisfiability problems"), the first part of a benchmark suite to be used in scientificexperiments and software competitions addressing SAT-solving issues.VLSAT-1 contains 100~benchmarks of increasing complexity, proposed in DIMACSCNF format under a permissive Creative Commons license. These benchmarks havebeen used by the 2020 International Competition on Model Counting.
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.
Taxonomy
TopicsAdvanced Database Systems and Queries · Formal Methods in Verification · Distributed systems and fault tolerance