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.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Nazier Mosaad, Peter; Fränzle, Martin; Xue, Bai: Model checking delay differential equations against metric interval temporal logic (2017)