An incremental and layered procedure for the satisfiability of linear arithmetic logic
From MaRDI portal
Recommendations
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- A practical approach to satisfiability modulo linear integer arithmetic
- A scalable method for solving satisfiability of integer linear arithmetic logic
- Linear quantifier elimination as an abstract decision procedure
- scientific article; zbMATH DE number 4112064
Cited in
(23)- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Experimenting on solving nonlinear integer arithmetic with incremental linearization
- SPASS-SATT. A CDCL(LA) solver
- Linear templates of ACTL formulas with an application to SAT-based verification
- Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
- Satisfiability modulo transcendental functions via incremental linearization
- Efficient theory combination via Boolean search
- Integration of linear arithmetic and goal-oriented resolution for software reasoning
- A practical approach to satisfiability modulo linear integer arithmetic
- An even closer integration of linear arithmetic into inductive theorem proving
- A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
- Satisfiability modulo theories
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
- Linear Arithmetic with Stars
- Solving Sparse Linear Constraints
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- SEPARATING AUXILIARY ARITY HIERARCHY OF FIRST-ORDER INCREMENTAL EVALUATION SYSTEMS USING (3K+1)-ary INPUT RELATIONS
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- A scalable method for solving satisfiability of integer linear arithmetic logic
- Equality detection for linear arithmetic constraints
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- Fast congruence closure and extensions
This page was built for publication: An incremental and layered procedure for the satisfiability of linear arithmetic logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5703769)
