Solving non-linear arithmetic

By Dejan Jovanovic, Leonardo de Moura. ACCA, 2012

324 citations recorded by the source corpus.

We propose a new decision procedure for the existential theory of the reals. It performs a backtracking search for a model in R, where the backtracking is powered by a novel conflict resolution procedure based on cylindrical algebraic decomposition. The initial experimental results are very encouraging. The full article has been accepted at the 6th International Joint Conference on Automated Reasoning (IJCAR 2012).

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/45e1afe506801695eb00b350a4b5188d9a90cd98

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Edmund M. Clarke
2. Soonho Kong
3. Sicun Gao
4. Tim King
5. Armando Solar-Lezama

In Computational Theory and Mathematics

1. Sicun Gao
2. Edmund M. Clarke
3. Soonho Kong
4. Tim King
5. Armando Solar-Lezama
6. Daniel Kroening

Citations in the corpus

• Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, methodology): “Jovanović and de Moura recently gave an effective method for quantifier-free non-linear real arithmetic based on a combination of the Model-Constructing Calculus [40] and partial Cylindrical Algebraic Decomposition [70].”
• dReal: An SMT Solver for Nonlinear Theories over the Reals (2013, methodology): “Besides solving the standard benchmarks [16] (data shown on the tool website), we managed to solve many challenging nonlinear benchmarks from the Flyspeck”