Interior Search for Nonlinear SMT and Application in Verification

Surface-mount technology (SMT) formulas over the real numbers can encode a wide range of problems in theorem proving and formal verification. Currently, constraint solving and verification in nonlinear theories over the reals use strategies that are similar to SAT solving. The current algorithms perform top-down global search in the state space. It starts with loose bounds on all variables, and then proceeds by the following three operations: pruning, branching, and backtracking. One can systematically explore the state space in this way, and always terminate with a delta-solution or proof of unsatisfiability. However, the current direct use of such exterior search methods can not exploit the rich analytic structures of the nonlinear constraints.

We are developing new methods that have the following key steps:

Sample and locally optimize. We can start with random samples in the state space and evaluate the errors with respect to the cost function. We then use stochastic gradient descent to find local minima from those samples. If any of these samples or local solutions satisfy the constraints, we can terminate the solving already.

Collect regions of unsatisfiability. Suppose we do not find solutions from the local optimization phase, we then have a set of points that indicate the regions in the state space that do not contain solutions. We can use local numerical analysis (such as multivariate Taylor expansion in the simplest case) and trust region analysis to produce representations of a set of neighborhoods that are guaranteed to not contain any solution.

Add learned constraints and improve search. Because the reasoning algorithms can handle arbitrary logical combinations (which makes the difference with traditional constraint solving), we can keep adding information about the neighborhoods from the previous step to guide the search. The learned constraints will play a key role similar to the learned clauses in SAT solving problems.