3

I'm a total newbie with Z3 (started today). So far liking it a lot. Great tool. Unfortunately the syntax confuses me a bit.

I want to prove that if:

a^3 = xyz = m ( with a, x, y, z, m (0..1) )

then:

3a <= (x+y+z)

I do so by trying to find a model satisfying that:

3a > (x+y+z)

Here is the Z3 code:

(declare-const a Real)
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(declare-const m Real)

(assert (> a 0))
(assert (< a 1))
(assert (> x 0))
(assert (< x 1))
(assert (> y 0))
(assert (< y 1))
(assert (> z 0))
(assert (< z 1))
(assert (> m 0))
(assert (< m 1))

(assert (= (* (* a a) a) m))
(assert (= (* (* x y) z) m))
(assert (> (* 3.0 a) (+ (+ z y) x) ))
(check-sat)

The model is unsatisfied.

Have I successfully proved what I wanted? As I said, the syntax confuses me since I'm a total newbie.

El Marce
  • 3,144
  • 1
  • 26
  • 40

2 Answers2

3

I think that your solution is correct. Let me explain a bit about using Z3 to prove validity of a statement A. The key idea is that, in the classical logic, e.g., propositional logic and predicate logic:

  • A is Valid iff negation(A) is Unsatisfiable.

This is a pretty well-known result. You can find it in many textbooks and materials, for example, in page 4 of this slide. So, validity of P -> Q can be proved via checking for unsatisfiability of its negation: P /\ negation(Q).

In particular, for your example,

(a^3 = x*y*z = m) -> (3a <= x+y+z) is Valid,

iff

(a^3 = m) /\ (x*y*z = m) /\ (3a > x+y+z) is Unsatifiable.

Trung Ta
  • 1,582
  • 1
  • 16
  • 25
  • 1
    Thanks so much for your detailed answer @Trung Ta,is well written and clear. I have upvoted it already :D . My question is however more in the line of the syntax and semantics of Z3 rather than the mathematical proof. Since I haven´t used Z3 more than a couple hours I want to know if the program I wrote is correct and actually represents the mathematical proof. Could you expand on this? A simple "your program seems correct" would be fine – El Marce Aug 21 '16 at 19:26
  • 2
    @Trung I like this general explanation of the relationship between validity and satisfiability. I posted another answer -- I suspect that people with a mathematical background are going to be more satisfied with what you wrote, while someone with a software engineering or programming background might be more likely to catch the idea from what I wrote. – Douglas B. Staple Aug 22 '16 at 13:47
  • 1
    @ElMarce Yes, your program is correct. You can refer to the detailed answer given by @ Douglas B. Staple. It explains more about your code. – Trung Ta Aug 22 '16 at 15:10
3

Your solution is correct.

Explanation: What you wrote is equivalent to:

0 < x < 1
0 < y < 1
0 < z < 1
0 < m < 1
a * a * a = m
x * y * z = m
3 * a > x + y + z

Z3 says this is unsatisfiable. Thus, if

a^3 = xyz = m ( with a, x, y, z, m (0..1) )

then it cannot be the case that:

3a > (x+y+z)

because, if this did occur, then the SMT problem you posed would be satisfiable, which would be a contradiction with the claim by Z3 that the SMT problem is unsatisfiable. If it cannot be the case that 3a > (x+y+z), then it must be the case that 3a <= (x+y+z), which is the statement you originally wanted to prove.

Douglas B. Staple
  • 10,510
  • 8
  • 31
  • 58