The VLSAT-3 Benchmark Suite - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2021

The VLSAT-3 Benchmark Suite

Le jeu de tests VLSAT-3

(1)
1
Pierre Bouvier

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).
VLSAT-3 (acronyme anglais de "très grands problèmes de satisfaisabilité booléenne") est le troisième volet d'une suite de tests destinée aux expérimentations scientifiques et aux compétitions de logiciels pour la résolution de problèmes SAT et SMT (Satisfaisabilité Modulo des Théories). VLSAT-3 contient 1200 formules logiques (600 satisfaisables et 600 insatisfaisables) du premier ordre sans quantificateur, de complexité croissante, fournies en format SMT-LIB sous une licence Creative Commons permissive. Plus de 90% de ces tests ont été utilisés lors de la 16ème Compétition Internationale de Satisfaisabilité Modulo des Théories (SMT-COMP 2021).
Fichier principal
Vignette du fichier
RT-0516.pdf (787.28 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03468625 , version 1 (07-12-2021)

Identifiers

Cite

Pierre Bouvier. The VLSAT-3 Benchmark Suite. [Research Report] RT-0516, INRIA Grenoble Rhône-Alpes. 2021, pp.1-20. ⟨hal-03468625⟩
69 View
28 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More