HySAT is a satisfiability checker for Boolean combinations of arithmetic constraints over real- and integer-valued variables which can also be used as a bounded model checker for hybrid (discrete-continuous) systems. A pecularity of HySAT, which sets it apart from many other solvers, is that it is not limited to linear arithmetic, but can also deal with nonlinear constraints involving transcendental functions.

The algorithmic core of HySAT is the iSAT algorithm, a tight integration of recent SAT solving techniques with interval-based arithmetic constraint solving. For technical details see [FHR+07]. HySAT is the successor tool and shares the name of the solver described in [FH06]. Do not mix up the two.

The development of HySAT has been partially supported by the German Research Council (DFG) as part of the Collaborative Research Center "Automatic Verification and Analysis of Complex Systems" (SFB/TR 14 AVACS).

Please note that the successor tool of HySAT is available now. Apart from bug-fixes, HySAT will be no longer maintained.