Max of a list of vectors of Boolean using z3 for resolution of SAT problem

Question

I am working on a Sat project, one of my subtasks is to compute the max of a list of a vectors of boolean, each of them is a number. An example of the vector is [False,True,True,False], it represents the number 2^2 + 2^1 = 6. In this resolution I cannot use the Int data of z3, but I must use only the Bool data of z3. To solve this problem I tried to use the following code, but it doesn't work.

from z3 import *
def greater(vec1, vec2, name):
   
    constraints = []
    gt = [Bool(f"gt_{name}{i}") for i in range(len(vec1))]
    
    constraints.append(
                And(
                    [
                    Implies(Not(vec1[0]), Not(vec2[0])),
                    Implies(And(vec1[0], Not(vec2[0])), gt[0]),
                    Implies(Not(Xor(vec1[0], vec2[0])), Not(gt[0]))]
                )
            )
    

    for i in range(1, len(vec1)):
        constraints.append(
            And(
            Or(gt[i-1], 
                And(
                [
                Implies(Not(vec1[i]), Not(vec2[i])),
                Implies(And(vec1[i], Not(vec2[i])), gt[i]),
                Implies(Not(Xor(vec1[i], vec2[i])), Not(gt[i]))]
                )    
            ),
            Implies(gt[i-1], gt[i])
        )
    )     
    return And(constraints)



def max_of_bin_int(values, max_values):

    constraints = []
    len_bits = len(values[0])
    constraints.append(
        And([max_values[0][j] == values[0][j] for j in range(len_bits)]),
    )

    for i in range(0, len(values)-1):
        constraints.append(
            If(greater(max_values[i], values[i+1], f"max{i}"), 
                And([max_values[i+1][j] == max_values[i][j] for j in range(len_bits)]),
                And([max_values[i+1][j] == values[i+1][j] for j in range(len_bits)])
        )
       )
    return And(constraints)


# Testing 
values = [ [True,True,True,False],
       [True,True,False,False],
        [True,True,False,False]
]

s = Solver()
max_values = [[Bool(f"x_{i}_{j}") for j in range(len(values[0]))] for i in range(len(values)) ]
s.add(max_of_bin_int(values, max_values))
print(s.check())
m = s.model()

print([m.evaluate(max_values[-1][j]) for j in range(len(values[0]))] )

The result that returns the function is [True, True, False, False] but it should be [True,True,True,False]. Can someone helps me?
Important:
I cannot use Int data of z3 only Bool data.

I am expecting a function that returns the constraints to find the maximum value of list of Boolean vectors to be used in a solver.

score 2 · Answer 1 · answered Apr 30 '23 at 22:23

First some preliminaries:

from z3 import *
from functools import *

s = Solver()

Comparing two boolean-vectors, when interpreted as unsigned numbers, amounts to lexicographic (i.e., dictionary) order. So, let's first write a predicate that walks down two equal-length lists and determines if the first is greater-than-or-equal to the second:

def gte(xs, ys):
    if not xs:
        return BoolVal(True)
    else:
        return If(xs[0] == ys[0], gte(xs[1:], ys[1:]), xs[0])

Now that we have a method that compares two bit-vectors, let's write another one that returns the greater one of two given vectors. We do this by declaring a fresh-variable so we can save the result of the comparison, ensuring the comparison result is shared for efficiency purposes:

def greater(xs, ys):
    comp = FreshBool()
    s.add(comp == gte(xs, ys))
    return [If(comp, i, j) for i, j in zip(xs, ys)]

With these two pieces put together, all we need is to reduce a set of vectors, returning the greatest element. To do this, we use the reduce function from functools:

def max_vectors(vss):
    return reduce(greater, vss)

And here's your testing code, adopted to work with these definitions:

values = [ [True, True, True,  False]
         , [True, True, False, False]
         , [True, True, False, False]
         ]

res = [Bool(f"res_{i}") for i in range(len(values[0]))]
for r, i in zip(res, max_vectors(values)):
    s.add(r == i)

print(s.check())
m = s.model()
print([m.evaluate(b, model_completion = True) for b in res])

This prints:

sat
[True, True, True, False]

which is what you were expecting.

Axel Kemper · Accepted Answer · 2023-04-30T19:48:07.190

The following variant of your code works for me:

from z3 import *

def greater(vec1, vec2):
    """
    cf. https://en.wikipedia.org/wiki/Digital_comparator
    """
    bits = len(vec1)
    msb = bits-1
    gt = And(vec1[msb], Not(vec2[msb]))    
    x = (vec1[msb] == vec2[msb])

    for i in reversed(range(msb)):
        gt = Or(gt, And(x, vec1[i], Not(vec2[i])))
        x = And(x, (vec1[i] == vec2[i]))

    return gt


def max_of_bin_int(values, max_values):
    rBits = range(len(values[0]))
    constraints = [max_values[0][j] == values[0][j] for j in rBits]

    for i in range(1, len(values)):
        gt = greater(max_values[i-1], values[i])
        constraints.append(
           And([max_values[i][j] == If(gt, max_values[i-1][j], values[i][j]) for j in rBits])
        )
 
    return And(constraints)


# Testing 
values = [[True,True,True,False],
          [True,True,False,False],
          [True,True,True,True],
          [True,True,False,False]
]

s = Solver()
rColumns = range(len(values[0]))
rRows = range(len(values))
max_values = [[Bool(f"x_{row}_{col}") for col in rColumns] for row in rRows]
s.add(max_of_bin_int(values, max_values))
print(s.check())
m = s.model()

print([m.evaluate(max_values[-1][col]) for col in rColumns] )

I've changed the vector comparator logic inspired by Wikipedia. Your greater function does not return a proper condition to control the If() function. It performs the comparison in the wrong bit-order. A digital comparator starts at the most-significant-bit (msb) and descends to the least-significant-bit. I am using reversed(range()) to get the order right.

Max of a list of vectors of Boolean using z3 for resolution of SAT problem

2 Answers2