Solving Non-linear Arithmetic

DOI10.1007/978-3-642-31365-3_27zbMath1358.68257OpenAlexW1493060511MaRDI QIDQ2908506

Leonardo de Moura, Dejan Jovanović

Publication date: 5 September 2012

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

Full work available at URL: https://doi.org/10.1007/978-3-642-31365-3_27

Mathematics Subject Classification ID

Related Items (54)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Learning probabilistic termination proofs ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Recent Advances in Real Geometric Reasoning ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Satisfiability Modulo Theories ⋮ Satisfiability Checking: Theory and Applications ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Verification Modulo theories ⋮ Automated analysis of tethered DNA nanostructures using constraint solving ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ raSAT: an SMT solver for polynomial constraints ⋮ From Polynomial Invariants to Linear Loops ⋮ Automated analysis of cryptographic assumptions in generic group models ⋮ FOSSIL ⋮ Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition ⋮ Levelwise construction of a single cylindrical algebraic cell ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ Computing with Tarski formulas and semi-algebraic sets in a web browser ⋮ Adapting Real Quantifier Elimination Methods for Conflict Set Computation ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ Are Parametric Markov Chains Monotonic? ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ Sequential Convex Programming for the Efficient Verification of Parametric MDPs ⋮ Learning modulo theories for constructive preference elicitation ⋮ Barrier certificates revisited ⋮ Structured learning modulo theories ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Using machine learning to improve cylindrical algebraic decomposition ⋮ Deniable Functional Encryption ⋮ Truth table invariant cylindrical algebraic decomposition ⋮ Cylindrical algebraic decomposition using local projections ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ raSAT: An SMT Solver for Polynomial Constraints ⋮ Speeding up the Constraint-Based Method in Difference Logic ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Symbolic computation of differential equivalences ⋮ Editorial: Symbolic computation and satisfiability checking ⋮ Fully incremental cylindrical algebraic decomposition ⋮ Cylindrical algebraic decomposition with equational constraints ⋮ From simplification to a partial theory solver for non-linear real polynomial constraints ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ Quantitative Abstractions for Collective Adaptive Systems ⋮ Efficient Simplification Techniques for Special Real Quantifier Elimination with Applications to the Synthesis of Optimal Numerical Algorithms ⋮ A Survey of Satisfiability Modulo Theory ⋮ Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition ⋮ Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness ⋮ Constructing a single cell in cylindrical algebraic decomposition ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

This page was built for publication: Solving Non-linear Arithmetic