CODEWITHSUNDEEP
z3smt
Samuel Gruetter
Samuel Gruetter

Reputation: 1703

Proving injectivity of two-digit encoding in arbitrary base

I'd like to automatically prove the following statement about arbitrary size integers:

forall base a b c d,
0 <= a < base ->
0 <= b < base ->
0 <= c < base ->
0 <= d < base ->
base * a + b = base * c + d ->
b = d

This should be equivalent to the claim that the following is unsat (assuming that the crazy hacks which generated this are correct):

(declare-const a Int)
(declare-const a0 Int)
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(assert (not (or (not (and (<= 0 a0) (< a0 a)))
              (or (not (and (<= 0 a1) (< a1 a))) 
               (or (not (and (<= 0 a2) (< a2 a))) 
                (or (not (and (<= 0 a3) (< a3 a))) 
                 (or (not (= (+ ( * a a0) a1)
                             (+ ( * a a2) a3))) 
                     (= a1 a3))))))))
(check-sat)

If I feed this to Z3, it returns unknown, even though this looks like a very simple input.

So my question is: What's the right way to prove this automatically? Are there configuration options for Z3 which will make it work? Should I do a different preprocessing? Or does this problem belong to a class of problems outside Z3's "area of expertise" and I should use another tool?

Update: Here's a more readable version of the same query, using (implies A B) instead of (or (not A) B):

(declare-const a Int)
(declare-const a0 Int)
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(assert (not (implies (and (<= 0 a0) (< a0 a))
              (implies (and (<= 0 a1) (< a1 a))
               (implies (and (<= 0 a2) (< a2 a))
                (implies (and (<= 0 a3) (< a3 a))
                 (implies (= (+ ( * a a0) a1) (+ ( * a a2) a3)) (= a1 a3))))))))
(check-sat)

Upvotes: 0

Views: 53

Answers (1)

alias
alias

Reputation: 30525

Since you're doing multiplication, the problem is non-linear; and SMT solvers usually cannot deal with non-linear arithmetic. (Z3 has an nonlinear reasoning engine, but it certainly isn't capable of solving arbitrary problems due to undecidability.)

If you fix base to be given values, z3 can handle your problem rather easily. For instance, adding:

(assert (= a 10))

makes z3 respond unsat in no time.

Also the input looks unnecessarily complicated; remember that SMTLib has an implies operator, instead of (or (not X) Y) you can just write (implies X Y) That would make your code a lot easier to read.

Upvotes: 1

Related Questions