Basics of SMT algorithm

Question

I'm not a computer science student and do not have a great understanding of algorithms or propositional logic. However, I do use SMT solver in a project and would like to get a basic idea of how the algorithm works?

I essentially have a function

f(x)=(p_0)x+(p_1)x^2+(p_2)x^3+...(p_n)^x^n

and a set of equations such as

f(x)>0

f(x)<1

f(x)+f'(x)f(x)<0.5

The SMT solver z3 computes the coefficients p_0,p_1...,p_n by checking for satisfiability of the given constraints over a set of data samples.

Can you in very simple terms help me understand how exactly does this happen? Does it search through the entire sample space of p?

Answer 1

You can think of SMT as one glorious search algorithm, but that would be extremely misleading: It is way smarter and much more sophisticated than that. In particular, it definitely does not search entire sample space, as you put it. (Imagine: SMT solvers can deal with unbounded integers and reals: It would be impossible to search these exhaustively.)

Unfortunately, this is too broad a question to answer in the context of stack-overflow, but you are in luck that there are many excellent references that are well worth taking your time and reading through. Here are two of my favorites:

• The "Decision procedures" book http://www.decision-procedures.org/ is an excellent read, and have many references that can help you guide into the literature. This book tells you all about the algorithms used in SMT-solvers for different logics, and even guides you if you're interested in building one.

• http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf is an excellent article by Leonardo and Nikolaj (principal developers of z3). It provides a great overview and is much easier to read if you are only interested in applications.

I'd recommend starting with the latter and use the references therein to further study the field per your interests. There are many excellent articles, tutorials, and a friendly stack-overflow community to help out should you get stuck!