Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure

By M. Fränzle, Christian Herde, Tino Teige, Stefan Ratschan, Tobias Schubert. Journal on Satisfiability, Boolean Modeling and Computation, 2006

352 citations recorded by the source corpus.

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with interval-based arithmetic constraint solving. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than delegating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving carry over smoothly to the rich domain of non-linear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combinations of multiple thousand arithmetic constraints over some thousands of variables.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/d5e854c0b5b0f0a85a41f59b25f705fead0e505b

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Networks and Communications

Citations in the corpus

Solving non-linear arithmetic (2012, methodology): “We compare the new solver to the following solvers that have been reported to perform reasonably well on fragments of nonlinear arithmetic: the z3 3.2 [14], cvc3 2.4.1 [2], and MiniSmt 0.3 [51] SMT solvers; the quantifier elimination based solvers Mathematica 8.0 [42,41], QEPCAD 1.65 [6], Redlog-CAD”
dReal: An SMT Solver for Nonlinear Theories over the Reals (2013, methodology): “Examples of numerical algorithms that have been exploited include optimization algorithms [4,18], interval-based algorithms [8,7,12], Bernstein polynomials [17], and linearization algorithms [9].”
Challenging SMT solvers to verify neural networks (2012, positive): “To these, we have added also H Y SAT [17] which was our solver of choice in [31].”
Flow*: An Analyzer for Non-linear Hybrid Systems (2013, methodology): “A few notable non-linear analysis tools include KeYmaera [8], Ariadne [9] and HySAT/iSAT [10].”
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (2010, methodology): “We implemented the above ideas in the tool NEVER (for Neural networks Verifier) [9] which leverages HYSAT [ 6 ] to verify abstract networks and the SHARK library [10] to provide MLP infrastructure, including representation and support for evaluation and repairing.”