AVACS » isat3

iSAT3 is a satisfiability checker for Boolean combinations of arithmetic constraints over real- and integer-valued variables. Those constraints may contain linear and non-linear arithmetic as well as transcendental functions. iSAT3 is the third implementation of the iSAT algorithm. All three implementations (with HySAT and iSAT being the first two) share the same major core principles of tightly integrating ICP into the CDCL framework. But while the core solvers of HySAT and iSAT operate on simple bounds, the core of iSAT3 uses literals and additionally utilizes an ASG for more advanced formula preprocessing. iSAT3 understands the same input file format as HySAT and iSAT. So you may use the iSAT example benchmarks as well.

Since version 0.03 iSAT3 supports accurate reasoning for floating-point arithmetic as well as fixed-width and bitwise integer operations.

iSAT3 is available for research and evaluation purposes only. It cannot be used in a commercial environment, particularly as part of a commercial product, without written permission. iSAT3 is provided as is, without any warranty.

Downloads: iSAT3 0.01, iSAT3 0.02, iSAT3 0.03, iSAT3 0.04

Supplemental material for: FMCAD 2014, FMCAD 2016