4
$\begingroup$

I was looking at this tutorial: https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb#scrollTo=4yuA2Fry68Y6&line=4&uniqifier=1 .

It says "Proof = Exhaustively Not Finding Counterexamples".

At the same time, the link is an example of "ask z3 to prove a bound" on the "Babylonian Square Root Method". How do I reconcile these? Is it a proof that would convince a mathematician (as a constructive proof using dependent types would)? Is it possible for Z3 to "prove" something that actually has a counterexample (maybe some kind of sharp discontinuity)?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ My guess is yes. Z3 is an SMT solver meaning it does first order logic in a number of different theories. One of those theories is likely something like the first order theory of the reals with (+,*,<,0,1), a.k.a. the theory of real closed fields. This theory is decidable meaning a computer given enough time can decide if any statement is true or false. But I personally don’t know the specifics of Z3 to give you a more concrete answer. $\endgroup$
    – Jason Rute
    Commented May 24, 2023 at 10:16

3 Answers 3

Reset to default
3
$\begingroup$

SMT is exhaustively searching in the S (SAT), not necessarily in the MT (theory).

Let's dig a little deeper into what an SMT solver actually is: SAT-modulo-theories. That means, it can solve boolean formulas, but instead of just containing boolean variables, there are logical predicates over some theory (e.g. the reals with $\le$ and some operations).

So an SMT solver contains two parts: a SAT solver and a theory solver. It's the SAT solver that is working exhaustively. The theory solvers work in a number of ways, depending on which theory you're using.

To solve an SMT formula, the solver takes each logical statement in the theory and replaces it with a boolean variable, giving a pure SAT problem. It passes that off to the SAT solver, and either gets UNSAT in which case there's no solution regardless of the theory, or it gets a T/F assignment for each variable.

Then, we make a single statement in the theory that is the conjunction of all of the statements that were given True in the above step, and the negation of all the ones that were False in the above step, pass it off to the theory solver, and see if it can find values for the variables that satisfy the statement. Critically, there is no disjunction in the statement: it's not an arbitrary logical formula, it's just a sequence of formulas in the theory.

Then, the theory solver either gives SAT or UNSAT. If it gives SAT, you win, you've found a satisfying assignment. If it gives UNSAT, then you've learned something new: that particular combination of predicates is not possible in the theory. So you take the boolean version of your formula, negate it, and add that to your problem, since you've learned something from your theory.

You repeat until either you get boolean UNSAT or the theory solver gives you SAT.

So SMT is just a way to take a theory solver that can't handle disjunctions and turning it into one that can. Things get more complicated with advanced features like datatypes, quantifiers, etc. But that's the basic idea.

The theory solver isn't searching exhaustively. For reals it's probably doing simplex or something similar. But it is classical, in the sense that we assume every statement in the theory is either true or false. That said, as @MevenLennon-Bertrand says in the comments, it is still complete: if there is a solution, it will find it. It's just not finding it by checking one by one.

Improve this answer
$\endgroup$
4
  • 3
    $\begingroup$ Maybe to make this answer clearer: the theory solver is not exhaustive in the sense that it does not try every value one by one (be it only because the domain is often infinite, as for reals), but it is still complete, in the sense that if it answers UNSAT there is no solution for this particular problem. To give a very simple, concrete example, you don't need to look at reals one by one to know that $x < 0 \wedge x \geq 1$ is unsatisfiable, because the properties of the order on reals tells you so, so you can answer UNSAT in that case. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 25, 2023 at 14:17
  • $\begingroup$ Thanks, this makes a lot more sense! Where does the SAT hand off to the theory solver? For example, given x * y > 0 do we pass (x > 0 and y > 0) and (x < 0 and y < 0) into the theory solver, or do we pass (x * y > 0) into the theory solver directly? (My guess is that latter, with the SAT solver being maximally ignorant of the theory?) $\endgroup$
    – llllvvuu
    Commented May 25, 2023 at 22:38
  • 1
    $\begingroup$ EDIT: I went down the Google rabbit hole and apparently the type of constraint in my above comment is "nonlinear arithmetic" which needs a kind of theory solver like nlsat $\endgroup$
    – llllvvuu
    Commented May 25, 2023 at 22:56
  • 1
    $\begingroup$ In general, the SAT solver knows only about the "logical" part (ie conjunction, disjunction, negation, etc.), but nothing about the content of individual atomic formulae, and it is the job of the theory solver to handle these. So in your case, the SAT solver would hand x*y > 0 to the theory solver, and the theory solver would be the one to deconstruct this into (x > 0 and y > 0) if it pleases. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented May 26, 2023 at 8:24
3
$\begingroup$

It does not "exhaustively search" real numbers by checking them one by one (obviously). Instead it uses sophisticated algorithms that use lots of algebra to do it.

Let me give a simple example. Suppose you want to know whether $\exists x \in \mathbb{R} . a x^2 + b x + c = 0$. We know from kindergarten that this statement is equivalent to $b^2 - 4 a c \geq 0$, which is a lot easier. Given concrete values of $a$, $b$ and $c$, we simply calculate the discriminant $b^2 - 4 a c$ and compare it with $0$.

Now imagine the same thing, but a lot fancier.

Improve this answer
$\endgroup$
1
$\begingroup$

This is the area of decision-procedures; a field with tons of research and a huge literature. To put it shortly, z3 (or any other SMT solver) does not exhaustively go over all possible inputs, neither when it's a finite domain (such as bit-vectors), nor when they are infinite (such as reals or integers, which is of course not possible).

Instead, they use so called "decision procedures" to determine if the given assertions are satisfiable or not.

Not all theories have decision procedures (cf. Hilbert's 10th problem), nor these procedures are necessarily cheap to run even when they exists. In addition, when theories are mixed-and-matched, you may or may not be able to combine the decision procedures for them. (Underlying theories need to be convex, but that's beyond our current discussion.)

However, most problems that arise in practice fall well within the reach of existing techniques. For instance, theory of real-closed field is decidable, due to Tarski. (See https://math.stackexchange.com/questions/151000/tarskis-decidability-proof-on-real-closed-field-and-peano-arithmetic), and most theories can be combined using the Nelson-Oppen theory combination technique (http://gauss.ececs.uc.edu/Courses/c626/lectures/SMT/nelson-oppen.pdf).

Here're some other references to get started with:

Improve this answer
$\endgroup$
6
  • $\begingroup$ I could be mistaken, but I think the OP’s question is if Z3 is formally proving the fact that there are no counter example. I take it from your your answer that the answer to the OP’s question is “yes”, assuming there are no bugs in Z3’s implementation of this subject matter, which is certainly not guaranteed. In other words if no bugs, then Z3 performs a rigorous and exhaustive search. (But also the proof that Z3 produces isn't something that one can access, but there are similar tools which produce proofs that can be checked elsewhere.) $\endgroup$
    – Jason Rute
    Commented May 24, 2023 at 17:51
  • $\begingroup$ Correct. SMT solvers use decision procedures; i.e., if they say unsat, then you can rest assured that it exhaustively established that there are no satisfying values. (Modulo bugs, of course.) $\endgroup$
    – alias
    Commented May 24, 2023 at 22:45
  • $\begingroup$ Right, my confusion was even more elementary, i.e. what "exhaustively" means for the reals (clearly not searching 0.1, 0.01, 0.001, etc). It sounds like I need to learn about first-order logic. I can imagine (handwavy guess) the statement can be broken down into bools where each bool is an inequality on one variable, then after you solve SAT on the boolean part, you check all the SAT solutions by intersecting intervals. The reality seems more complex than this, but tl;dr it seems like the answer to my OP is "yes". It's interesting that no certificate is printed out by this particular software. $\endgroup$
    – llllvvuu
    Commented May 25, 2023 at 1:28
  • $\begingroup$ Now that I read it again, the tutorial did actually mention that the "exhaustive" refers to the SAT part and not the "theory" part, although I had forgotten by the time I got to the "Takeaways" section which doesn't recap the "modulo theories" part $\endgroup$
    – llllvvuu
    Commented May 25, 2023 at 1:31
  • $\begingroup$ (I suppose it seems pointless to print out a proof since the list of things exhaustively searched would be as long as the runtime of exhaustively searching) $\endgroup$
    – llllvvuu
    Commented May 25, 2023 at 1:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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