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.
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
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⟩
