|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
The VLSAT-3 Benchmark Suite
Pierre Bouvier
INRIA Technical Report 516, December 2021
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 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 |  |
 PostScript |