Solving Non-Linear Arithmetic

  • Dejan Jovanovic ,
  • Leonardo de Moura

MSR-TR-2012-20 |

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.