SPASS-SATT. A CDCL(LA) solver
From MaRDI portal
Publication:2305409
DOI10.1007/978-3-030-29436-6_7OpenAlexW2969721123MaRDI QIDQ2305409
Martin Bromberger, Christoph Weidenbach, Simon Schwarz, Mathias Fleury
Publication date: 10 March 2020
Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_7
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Local Search For Satisfiability Modulo Integer Arithmetic Theories, An efficient subsumption test pipeline for BS(LRA) clauses
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- New techniques for linear arithmetic: cubes and equalities
- A reduction from unbounded linear mixed arithmetic problems into bounded problems
- Fast Cube Tests for LIA Constraint Solving
- Linear Integer Arithmetic Revisited
- Solving SAT and SAT Modulo Theories
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- Reducibility among Combinatorial Problems
- Cutting to the Chase Solving Linear Integer Arithmetic
- Computer Aided Verification
- The MathSAT5 SMT Solver
- Splitting on Demand in SAT Modulo Theories
- Computer Aided Verification