Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure1
Martin Fränzle, Christian Herde, Tino Teige, Stefan Ratschan, Tobias Schubert · Journal on Satisfiability Boolean Modeling and Computation · 2007
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 constr