Skip to Main content Skip to Navigation
Conference papers

SPASS-SATT: A CDCL(LA) Solver

Martin Bromberger 1, 2 Mathias Fleury 2, 1 Simon Schwarz 1 Christoph Weidenbach 2, 1
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/hal-02405524
Contributor : Stephan Merz <>
Submitted on : Wednesday, December 11, 2019 - 5:24:40 PM
Last modification on : Tuesday, March 3, 2020 - 4:10:24 PM
Document(s) archivé(s) le : Thursday, March 12, 2020 - 11:08:34 PM

File

cade27spass.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

36

Files downloads

95