Performance issue with unsatisfiable models

Question

I'm using Z3 to construct a bounded model-checker. I'm running into a strange performance problem when trying to implement a completeness test. The completeness test has to make sure that all states that every path contains each state at most once. If there are still paths which fulfill this property, Z3 is quick with an answer, however in the case where all paths have been considered, Z3 seems to be exponentially slow.

I've reduced my test-case to the following:

; Set the problem size (length of path)
(define-fun sz () Int 5)

; Used to define valid states
(define-fun limit ((s Int)) Bool
  (and (>= s 0)
       (<= s sz)))

; Constructs a path of a given length
(define-fun path-of-len ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int))
          (=> (and (>= i 0)
                   (< i len))
          (limit (select path i)))))

; Asserts that a given path only contains unique states
(define-fun loop-free ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int) (j Int))
          (=> (and (>= i 0)
                   (>= j 0)
                   (< i len)
                   (< j len)
                   (not (= i j)))
              (not (= (select path i) (select path j))))))

; Construct a unique path of a given length
(define-fun path ((path (Array Int Int)) (len Int)) Bool
  (and (path-of-len path len)
       (loop-free path len)))

; Declare a concrete path
(declare-const tpath (Array Int Int))

; Assert that the path is loop free
(assert (path tpath (+ sz 2)))

(check-sat)

On my computer this results in the following running times (depending on path length):

• 3: 0.057s
• 4: 0.561s
• 5: 42.602s
• 6: >15m (aborted)

If I switch from Int to bitvectors of size 64, the performance gets a little better, but still seems exponential:

• 3: 0.035s
• 4: 0.053s
• 5: 0.061s
• 6: 0.106s
• 7: 0.467s
• 8: 1.809s
• 9: 2m49.074s

Strangely enough, for a length of 10 it only takes 2m34.197s. If I switch to bitvectors of smaller size, the performance gets a little better, but is still exponential.

So my question is: Is this to be expected? Is there a better way to formulate this "loop-free" constraint?

Answer 1

Your formula is essentially encoding the “pigeon-hole” problem. You have sz+1 holes (the values 0, 1, …, sz) and sz+2 pigeons (the array cells (select tpath 0), …, (select tpath (+ sz 1))). You first quantifier is stating that each pigeon should be put in one of the holes. The second is stating that two different pigeons should not be in the same hole.

There is no polynomial size resolution proof for the “pigeon-hole” problem. So, the exponential growth in run time is expected. Note that any SAT solver based on resolution, DPLL, or CDCL will perform badly on the pigeon-hole problem..

You get better performance when using bit-vectors because Z3 reduces them to propositional logic and case analysis is much more efficient at that level.

BTW, you are using quantifiers for encoding parametric problems. That is an elegant solution, but it is not the most efficient approach for Z3. For Z3, in general, it is better to assert the 'expanded' quantifier free problem. However, for the problem described in your question, it will not make a big difference, since you will still experience the exponential growth.

Answer 2

Just like what Leonardo said, since the pigeon-hole problem is exponential in nature, the performance will go bad eventually whatsoever. The only thing you could probably do is to postpone the time the performance goes bad. Since you have tried bit-vector, my suggestions are try converting the problem into quantifier-free problem as suggested by Leonardo, given that the problem size is pre-defined, and try using some tactics.