-2
$\begingroup$

First, an example of a set of constraints which turned out not to be solvable (I don't think):

b < 3 && c + a > 5 && a - b > 2 && c > 1 && b - c > 3

My procedure for solving this is roughly: Okay b is less than 3, and c > 1. 1 + a > 5, so a > 4 in that case. Try 4 - 2 > 2, no that doesn't work, so maybe a is 5, 5 - 2 > 2. Then b - c > 3. 2 - 2 > 3. No, so b must b greater than 3, but we know b is less than 3, so it can't be solved.

Then a simpler example that can be solved.

b < 3 && c + a > 5 && a - b > 2

So say b is 2. Then a - 2 > 2, so say a is 5. Then c + 5 > 5, so say c is 1 as well. Then a = 5, b = 2, c = 1 solves the problem.

In that example, I picked numbers that were close to the boundary, in that they were "just above" the lower bound in the > part. But you could say that a is 100 and c is 100. This is a particularly easy example as well.

My question is, how a constraint solver solves this problem. I have been reading about SAT and SMT, and have yet to read the book on decision procedures. However, I understand that SAT solvers solve systems of boolean equations in two ways: (1) by returning yes/no that the system can be solved, or (2) by assigning valuations to each variable in the system so that it satisfies the constraints. I don't know how they do this though. I also understand that SMT solvers are basically a light layer on top of SAT solvers. They allow you to have richer boolean formulas using different "theories" (such as theory of equality, theory of reals, of integers, of lists, etc.). Then you can optionally define how to merge these theories so you can apply the SAT solver on a complicated expression involving e.g. the reals, integers, equality, booleans, and lists or arrays all at once. To me this seems obvious, why wouldn't the constraint solver just work over arbitrary functions and variables, but I'm probably missing something.

I would like to know how to implement something like z3. I assume that each specific theory (such as the theory of strings) is quite complicated, so I didn't want to ask about how to generically solve all the different kinds of constraints. Instead I wanted to ask a simplified down question using basic integer constraints so I can learn the fundamentals of how an SMT / SAT solver works.

As such, the question is basically just that, how a constraint solver solves the second example above. One or two of the algorithms it might use to do so. Specifically, I would like to know how to give some function a set of constraints, and have it give me back valuations for all of the variables. In that regard, the question also entails how the constraint solver picks or decides on the set of values. I have seen it said that it is random, but I would like to avoid that approach if possible. But either way, when it picks a value, wondering how it knows it got a valid one. If it has to recompute all the constraints every time it makes a guess, or can do some sort of optimization. Basically, just how the SAT / SMT solver works.

To keep it simple, I am not looking for a complete explanation of how all aspects of solving the problem work. Just more a high level introduction to the algorithms and how they go about selecting the values and returning the valuation. Once I understand that then I figure understanding the more complicated theories like the theory of strings will make more sense.

I am asking because I can't tell based on my reading so far if it all really just boils down to apply constraints into a SAT solver, and there are maybe 1 or 2 SAT solving algorithms (DPLL and CDCL I am getting familiar with) for Boolean constraints (plus maybe a few more for generating the test data to solve the constraints). Or am I wrong there, and there is an entire layer of research on top of that (on SMT solvers) where custom decision procedures are the algorithms you want to use, and there are hundreds of them and there's no standard pattern to them. In which case I keep having difficulty imaging how it is possible to solve a constraint system like the one above, or something more complicated with string constraints (matches regex) and other constraints that require complex functions (like something is the reverse or sorted version of something else). If there's that much variability then the idea of solving any constraints seems hard.

Basically what I am looking for is a description of an implementation. I have read many papers so far but they have mostly been too high level to apply it.

$\endgroup$
  • $\begingroup$ This seems very broad to me. Are you asking "how do I implement an SMT solver"? $\endgroup$ – xuq01 Jul 21 '18 at 17:59
  • $\begingroup$ Well ideally that would be cool, but no I am just wondering how the algorithm works. $\endgroup$ – Lance Pollard Jul 21 '18 at 18:00
  • $\begingroup$ Reas about the simplex algorithm and Pugh's Omega test! $\endgroup$ – xuq01 Jul 22 '18 at 4:51
3
$\begingroup$

The Simplex algorithm solves the linear programming problem.

Linear programming is the problem of optimizing a linear function with inputs $x_1, x_2, \dots, x_n$ subject to a system of linear equations:

$$ 0 \leq x_1, \dots, x_n $$

$$ a_{11} x_1 + \dots + a_{1n} x_n \leq b_1 $$ $$ a_{21} x_2 + \dots + a_{2n} x_n \leq b_2 $$ $$ \dots $$ $$ a_{n1} x_1 + \dots + a_{nn} x_n \leq b_n $$

The simplex algorithm produces an assignment to the variables that satisfies all of these linear equations, or responds that no assignment is possible. In practice it does this efficiently, but the worst case time complexity is exponential.

Notice that the Simplex algorithm requires each $x_i$ to be non-negative. If you have signed numbers, you can transform them into two non-negative numbers for the simplex algorithm:

$$ x_i = x_i' - x_i'' \text{ with } 0 \leq x_i', x_i'' $$


Each problem domain in SMT (each "theory") requires a new algorithm for quickly answering satisfiability. These theories can in fact be combined even if they're implemented entirely separately by the Nelson Oppen technique.


If you want to try implementing an SMT solver yourself, I suggest starting with the theory of equality with uninterpreted functions (called QF_UF by SMT-LIB).

This theory involves constraints that look like this:

$$ f(x_1) = x_2 \;\wedge\; f(f(x_2)) = x_3 \;\wedge\; x_1 = x_2 \;\wedge\; x_1 \neq x_3 $$

The above is not satisfiable:

$x_1 = x_2 \implies f(x_1) = f(x_2) = x_2$

$ \implies f(f(x_2)) = f(x_2) = x_2$

$ \implies x_1 = x_2 = x_3 $

yet $x_1 \neq x_3$ is the final constraint.

This can be accomplished using the Union Find data structure with extra bookkeeping to make $f(x) = f(y)$ whenever $x = y$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.