SPASS-SATT: A CDCL(LA) Solver - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

SPASS-SATT: A CDCL(LA) Solver

(1, 2) , (2, 1) , (1) , (2, 1)
1
2

Abstract

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
Origin : Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

Cite

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⟩
38 View
165 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More