Solving Non-Linear Arithmetic

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.

nonlinear.pdf
PDF file

Details

TypeTechReport
NumberMSR-TR-2012-20
> Publications > Solving Non-Linear Arithmetic