SPASS-SATT. A CDCL(LA) solver

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

zbMATH Keywords

linear arithmeticinteger arithmeticSMTpreprocessing

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

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

• FLINT
• SPASS
• Yices
• z3
• CVC4
• MathSAT5

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

This page was built for publication: SPASS-SATT. A CDCL(LA) solver