iSAT

| project staff | cooperation partners | description | benchmarks | publications |

iSAT has been developed to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions. The core of iSAT is based on a tight integration of recent DPLL-style SAT solving techniques (like lazy clause evaluation, conflict-driven learning, non-chronological backtracking, and restarts) 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. Moreover, iSAT also provides a BMC interface to be able to check properties of hybrid systems. For further information look at http://projects.informatik.uni-freiburg.de/projects/isat/ and http://www.avacs.org/tools/isat/. Final remark: iSAT is the successor of HySAT, and has a successor itself: iSAT3.

The iSAT Quick Start Guide gives a short introduction to the input language of iSAT.