SAT modulo linear arithmetic for solving polynomial constraints

DOI10.1007/s10817-010-9196-8zbMath1243.68210OpenAlexW1974368544MaRDI QIDQ438576

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

zbMATH Keywords

terminationconstraint solvingnon-linear arithmeticpolynomial constraintsSAT modulo theoriessystem verification

Mathematics Subject Classification ID

Related Items (7)

Hyper-arc consistency of polynomial constraints over finite domains using the modified Bernstein form ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Speeding up the Constraint-Based Method in Difference Logic ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\)
• Mechanically proving termination using polynomial interpretations
• Semidefinite programming relaxations for semialgebraic problems
• Constructing invariants for hybrid systems
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Proving Termination Properties with mu-term
• Non-linear loop invariant generation using Gröbner bases
• 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
• Computer Aided Verification
• Algorithms in real algebraic geometry

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