A Nonlinear Real Arithmetic Fragment | SRI International
This is an archived website. Go to the current SRI website

Toggle Menu

A Nonlinear Real Arithmetic Fragment

July, 2014

Tiwari, A., & Lincoln, P. (2014, 18-22 July). A nonlinear real arithmetic fragment. Paper presented at the International Conference on Computer Aided Verification (CAV'14), Vienna, Austria.


We present a new procedure for testing satisability (over the reals) of a conjunction of polynomial equations. There are three possible return values for our procedure: it either returns a model for the input formula, or it says that the input is unsatisfiable, or it fails because the applicability condition for the procedure, called the eigen-condition, is violated. For the class of constraints where the eigen-condition holds, our procedure is a decision procedure. We describe satisability-preserving transformations that can potentially convert problems into a form where eigen-condition holds. We experimentally evaluate the procedure and discuss applicability.

In Proceedings
Search Publications
Browse by Sectors
E.g., 2020-08-10
E.g., 2020-08-10