SPASS-SATT. A CDCL(LA) solver

DOI10.1007/978-3-030-29436-6_7MaRDI QIDQ2305409zbMATH OpenOpenAlexFDO

Authors Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach

Publication date 10 March 2020

Full work available at URL https://doi.org/10.1007/978-3-030-29436-6_7

zbMATH Keywords

integer arithmeticlinear arithmeticpreprocessingSMT

Mathematics Subject Classification ID

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

Recommendations

• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• A practical approach to satisfiability modulo linear integer arithmetic
• Tools and Algorithms for the Construction and Analysis of Systems
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• From Propositional Satisfiability to Satisfiability Modulo Theories

Cites work

• A practical approach to satisfiability modulo linear integer arithmetic
• A reduction from unbounded linear mixed arithmetic problems into bounded problems
• Computer Aided Verification
• Computer Aided Verification
• Computing small clause normal forms
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Cutting to the chase. Solving linear integer arithmetic
• Efficient Term-ITE Conversion for Satisfiability Modulo Theories
• Fast cube tests for LIA constraint solving
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 3249560 (Why is no real title available?)
• Lazy satisfiability modulo theories
• Linear integer arithmetic revisited
• New techniques for linear arithmetic: cubes and equalities
• Reducibility among combinatorial problems
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Splitting on Demand in SAT Modulo Theories
• The MathSAT5 SMT solver

Cited in

(5)

• An efficient subsumption test pipeline for BS(LRA) clauses
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Local Search for SMT on Linear Integer Arithmetic
• ALASCA: reasoning in quantified linear arithmetic
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2305409)