SAT modulo linear arithmetic for solving polynomial constraints

DOI10.1007/S10817-010-9196-8zbMATH Open1243.68210OpenAlexW1974368544MaRDI QIDQ438576FDOQ438576

Salvador Lucas, Cristina Borralleras, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio

Publication date: 31 July 2012

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10251/37666

Recommendations

• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• raSAT: An SMT Solver for Polynomial Constraints
• raSAT: an SMT solver for polynomial constraints
• From simplification to a partial theory solver for non-linear real polynomial constraints
• Solving non-linear arithmetic

zbMATH Keywords

terminationconstraint solvingnon-linear arithmeticpolynomial constraintsSAT modulo theoriessystem verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Semidefinite programming relaxations for semialgebraic problems
• Algorithms in real algebraic geometry
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Title not available (Why is that?)
• Constructing invariants for hybrid systems
• Non-linear loop invariant generation using Gröbner bases
• Proving Termination Properties with mu-term
• Computer Aided Verification
• Title not available (Why is that?)
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Polynomials over the reals in proofs of termination : from theory to practice
• Computer Science Logic
• Static Analysis
• Logic Programming
• Search Techniques for Rational Polynomial Orders
• Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\)
• Mechanically proving termination using polynomial interpretations

Cited In (13)

• Optimization modulo non-linear arithmetic via incremental linearization
• Inferring Congruence Equations Using SAT
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Title not available (Why is that?)
• Automatic synthesis of logical models for order-sorted first-order theories
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• On complexity bounds and confluence of parallel term rewriting
• Speeding up the Constraint-Based Method in Difference Logic
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Hyper-arc consistency of polynomial constraints over finite domains using the modified Bernstein form
• raSAT: An SMT Solver for Polynomial Constraints
• SAT Modulo Differential Equation Simulations

Uses Software

• SMT-LIB
• REDLOG
• cvc3
• z3
• AProVE
• MU-TERM

This page was built for publication: SAT modulo linear arithmetic for solving polynomial constraints

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