Satisfiability Modulo Theory

Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality.

SMT problems are solved by Satisfiability Modulo Theory algorithms. SMT algorithms are becoming increasing popular due to the richer way of representing optimization problems and their power (build on SAT algorithms).

The SMT format is described in detail here.

Satalia solves SMT problems. Simply upload your SMT files (with extension .smt) to our SolveEngine using our API or Web-Poral, and let Satalia do the solving.