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

Abstract

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