Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable
摘要
In this paper, we recount the story of iSAT, one of the tools we developed and explored during our doctoral studies. iSAT is a solver that builds on a synthesis of DPLL SAT solving and interval constraint solving, leveraging the algorithmic commonalities between these two techniques to create a unified approach. It addresses Boolean combinations of theory atoms from the undecidable theory of nonlinear arithmetic constraints over the reals and integers, including transcendental functions. What distinguishes iSAT is that, unlike many other academic tools that end up shelved after serving their research purpose, it has evolved from its academic origins 20 years ago to become one of the backend engines of a commercial software product for the automated testing and verification of embedded systems. Over the years, we developed and investigated various algorithmic enhancements to the solver core and explored multiple extensions. Notably, we added native support for handling ordinary differential equations and extended iSAT to handle stochastic constraint systems involving stochastic quantifiers. We developed iSAT while working under the guidance of our doctoral advisor, Martin Fränzle, in whose honor we are writing this paper for his 60th birthday. Thus, this story is also a reflection of the years we spent with Martin, a time we remember fondly.