iSAT - an Algorithm for Satisfiability Modulo the Theory of Non-linear Arithmetic

 

 

Tino Teige (University of Oldenburg, Germany)

 

Abstract:

The talk presents an algorithm for the satisfiability problem of
Boolean combinations of non-linear arithmetic constraints, including
transcendental functions like sine, over the reals and integers.
Constraint systems with a non-linear part and a complex Boolean
structure arise naturally in industrial applications as in the safety
analysis of embedded hybrid systems. In spite of undecidability of
that problem class, industrial needs motivate the development of
algorithms able to solve a large number of such constraint
formulae. The approach presented in the talk is a tight integration of
the DPLL procedure (the basis of most modern SAT solvers) and
interval-based arithmetic reasoning.

The first part of the talk introduces the two basic ingredients of
iSAT, the DPLL procedure and its algorithmic improvements, and
interval constraint propagation. We continue by presenting the iSAT
algorithm followed by an extensive example. At the end, we mention
some application domains and topics of current and future research.