SPASS-SATT: A CDCL(LA) Solver - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

SPASS-SATT: A CDCL(LA) Solver

Résumé

SPASS-SATT is a CDCL(LA) solver for linear rational and linear mixed/integer arithmetic. This system description explains its specific features: fast cube tests for integer solvability, bounding transformations for unbounded problems, close interaction between the SAT solver and the theory solver, efficient data structures, and small-clause-normal-form generation. SPASS-SATT is currently one of the strongest systems on the respective SMT-LIB benchmarks.
Fichier principal
Vignette du fichier
cade27spass.pdf (897.42 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02405524 , version 1 (11-12-2019)

Identifiants

Citer

Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach. SPASS-SATT: A CDCL(LA) Solver. CADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.111-122, ⟨10.1007/978-3-030-29436-6_7⟩. ⟨hal-02405524⟩
43 Consultations
200 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More