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
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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, December 17, 2019 - 2:25:41 AM

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. 27th International Conference on Automated Deduction (CADE-27), 2019, Natal, Brazil. pp.111-122, ⟨10.1007/978-3-030-29436-6_7⟩. ⟨hal-02405524⟩

Share

Metrics

Record views

16

Files downloads

35