Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Solving Non-Linear Arithmetic

Dejan Jovanovic and Leonardo de Moura


We present a new algorithm for deciding satisfiability of non-linear arithmetic constraints. The algorithm performs a Conflict-Driven Clause Learning (CDCL)-style search for a feasible assignment, while using projection operators adapted from cylindrical algebraic decomposition to guide the search away from the conflicting states.


Publication typeTechReport
> Publications > Solving Non-Linear Arithmetic