z3

How to check for 1000+ variables having no duplicate values?


I am new to Z3 and for an open source program I want to use the z3 solver to enhance the efficiency.

I have about 1000+ values of

(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const a4 Int)
...

which result to

(declare-const x1 Int)
(declare-const x2 Int)
...
(assert (=  (+ a1 a2) x1) // in reality its not "plus" but more sophisticated
(assert (=  (+ a3 a4) x2) // however for simplicity lets keep it at that here.
...

Now I want to ensure that all the x1 to x500+ variables have different values and that there are no duplicates.

of course I could do

(assert (not (= x1 x2)))
(assert (not (= x1 x3)))
(assert (not (= x1 x4)))
...
(assert (not (= x2 x3)))
(assert (not (= x2 x4)))
...
(assert (not (= x718 719)))

and that would work - but is there a better solution?

Thanks a lot!


Solution

  • You can use distinct (see this example):

    (assert (distinct x1 ... x500))
    

    AFAIK, this is normally internally expanded in a sequence of inequalities, just like the one you presented in your example.


    Discussion: What follows is a purely theoretical discussion about the efficiency of this encoding; z3 is quite an efficient SMT solver, so you may not need to try anything more sophisticated than simply running the tool.

    The negation of an equality (e.g. (not (= x y))) is generally split in a pair of inequalities:

    x < y \/ x > y
    

    Let's say x < y and x > y are renamed B1 and B2 respectively, the following clause is fed to the SAT engine:

    B1 \/ B2
    

    Now, given your problem, you get hundreds of these clauses. These are all related to each other at the Linear Arithmetic level, but not at the Boolean level at which the SAT engine operates. Thus, the SAT engine is likely to generate a (significant) number of inconsistent partial truth assignments, that generally violate the transitivity property of the < operator, e.g.

     x < y /\ y < z /\ z < x
    

    These conflicts are going to be revealed by the Theory Solver for LRA during early pruning calls, and resolved at the Boolean level by learning a conflict clause blocking the invalid assignment.

    What you can try:


    EDIT:

    If the set of values that can be assigned to the variables x_i is finite and somewhat limited in size, you can try counting the number of variables x_i with a certain value using the non-standard z3 extension for defining cardinality constraints, e.g.

    (assert
        ((_ at-most 1)
         (= x1 0)
         (= x2 0)
         ...
         (= x500 0)
        )
    )
    ...
    % repeat for all possible values 
    ...
    

    I am uncertain about the performance impact of this change. In normal circumstances it would positively affect the performance, because it reveals conflicting assignments earlier on (see, e.g., [1]). However, you are dealing with a pretty large number of variables and a large domain of candidate values for the variables x_i, so flattening the search at the Boolean level may be an overkill.