4

I have a question about Quantifiers.

Suppose that I have an array and I want to calculate array index 0, 1 and 2 for this array -

(declare-const cpuA (Array Int Int))
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1)))

Or otherwise I can specify the same using forall construct as -

(assert (forall ((x Int)) (=> (and (>= x 0) (<= x 2)) (or (= (select cpuA x) 0) (= (select cpuA x) 1)))))

Now I would like to understand the difference between two of them. The first method executes quickly and gives a simple and readable model. In contrast the code size with second option is very less, but the program takes time to execute. And also the solution is complex.

I would like to use the second method as my code will become smaller. However, I want to find a readable simple model.

Raj
  • 3,300
  • 8
  • 39
  • 67

1 Answers1

4

Quantifier reasoning is usually very expensive. In your example, the quantified formula is equivalent to the three assertions you provided. However, that is not how Z3 decides/solves your formula. Z3 solves your formula using a technique called Model-Based Quantifier Instantiation (MBQI). This technique can decide many fragments (see http://rise4fun.com/Z3/tutorial/guide). It is mainly effective on the fragments described in this guide. It supports uninterpreted functions, arithmetic and bit-vector theories. It also has limited support for arrays and datatypes. This is sufficient for solving your example. The model produced by Z3 seems more complicated because the same engine is used to decide more complicated fragments. The model should be seem as a small functional program. You can find more information on how this approach works in the following articles:

Note that, array theory is mainly useful for representing/modeling unbounded or big arrays. That is, the actual size of the array is not known or is too big. By big, I mean the number of array accesses (i.e., selects) in your formula is much smaller than the actual size of the array. We should ask ourselves : "do we really need arrays for modeling/solving problem X?". You may consider the following alternatives:

  • (Uninterpreted) functions instead of arrays. Your example can be encoded also as:

    (declare-fun cpuA (Int) Int)

    (assert (or (= (cpuA 0) 0) (= (cpuA 0) 1)))
    (assert (or (= (cpuA 1) 0) (= (cpuA 1) 1)))
    (assert (or (= (cpuA 2) 0) (= (cpuA 2) 1)))

  • Programmatic API. We've seen many examples where arrays (and functions) are used to provide a compact encoding. A compact and elegant encoding is not necessarily easier to solve. Actually, it is usually the other way around. You can achieve the best of both worlds (performance and compactness) using a programmatic API for Z3. In the following link, I encoded your example using one "variable" for each position of the "array". Macros/functions are used to encode constraints such as: an expression is a 0 or 1. http://rise4fun.com/Z3Py/JF

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Dear Leonardo, I am coming back to same question again. I am trying to optimize the code for sat solver. Could you please tell me when it is good to use constants and when it is good to use uninterpreted functions. For example, I have around 30-40 uninterpreted functions in my code. When I replace some functions to multiple constants for example (xA 0) replaced by xA0 and so on, I get reduction in runtime, but for others I don't get. What is the key-rule to choose between them? Is it dependent on how much you use them in the code? – Raj May 31 '12 at 08:44
  • Fluctuations is performance are very common. We observe fluctuations even when we make small modifications such as reordering the assertions. Any minor modification may change the order Z3 traverses the search space. As a rule of thumb, we should avoid quantifiers whenever possible. If we can encode a problem using a single theory, we will usually get better performance. Of course, we always have exceptions. What kind of performance fluctuation are you observing? It is on the order of 2x, 10x, 100x? – Leonardo de Moura May 31 '12 at 18:41