SMT Solvers

Satisfiability Modulo Theory problems were introduced in my sphere of interest lately as I need to find a way to check whether a set of constraints remains satisfiable when new constraints are added.

What is an SMTproblem? It is a problem that includes a set of expressions (like inequalities between symbols and numbers) that needs estimation on whether it is satisfiable or not. That means whether there is a set of values for the variables that appear in the expressions that make all the expressions true at the same time. If there is then the set is satisfiable, if not then the set is unsatisfiable.

At this case it would be good to make a distinction between satisfiability and validity. Valid is an expression that is always true independent of the values that its variables will take. An expression is satisfiable when there is at least a combination of the variables that makes it true. It is easy to see that:

P is valid when not P is not satisfiable.

and

P is satisfiable if and only if not P is not valid.

As an SMT solver can check for satisfiability, it can also check for validity by checking the satisfiability of the opposite expression! (It blew my mind when I realized that).

So I was looking for a tool that could do all this maths for me, automatically, for any instance of my problems that I could feed it and thus I searched for an SMT solver. I found many descent ones like the following:

OpenSMT: Is an open SMT solver. It can be integrated with other projects.

STP Contraint solver: Is a constraint solver that has been developed in MIT.

CVC4: Is a solver that seems to be vibrant. There have been previous versions like CVC, CVC Lite, CVC3 but the project claims that despite a successor it is code independent from the previous ones.\

Z3: Is a solver developed by Microsoft Research which by the way seems to be doing great research on automatic theorem proving (for further information you can check the Coq proof assistant that is an advanced theorem proover under development). Although I have no specific criteria yet I chose to work with this one initially because of the support of many platforms (windows and linux (well and OSX but I don’t use it)) and the support of many input formats (more on that later).

Other that I found but had no lack in checking out were:

Yices,SMT-RAT,Mini-SAT and there are plenty more in the wikipedia page for SMT solvers.

A good thing here is to mention the difference on SAT solvers and SMT solvers:

SAT solvers use only boolean expressions in contrast with the SMT that uses integers. The expressions that can be used are either inequalities or equalities between unknown functions. A SMT solver can be implemented as a transformer to a boolean representation of the problem and then a solution using an SAT solver like BASolver. This is actually used by it has its drawbacks thus there are native SMT solvers too.

All these solver get a set of expressions and check whether they are satisfiable or not. This input can be expressed in a variety of ways with the most prominent being the following:

SMT-LIB v1.x – v2.0: Is a library that is being created from 2003 in an attempt to formalize the domain. It seemed to me most satisfactory to use thus I chose to use it.
SATLIB – The Satisfiability Library: Is the equivalent library for SAT problems. It introduces the DIMACS input style.
CVC: It is a style used by the CVC solver (and some others too).

Note: Not all solvers support all available formats.
I found a couple more that I won’t mention as I did not find any documentation on them.

Advertisements