| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
SPASS-SATT: A CDCL(LA) Solver
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.
Cited literature [34 references]
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
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)