Макс. список векторов логических значений с использованием z3 для решения проблемы SAT

У меня работает следующий вариант вашего кода:

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] )

Я изменил логику векторного компаратора, вдохновленную Википедией. Ваша функция greater не возвращает правильное условие для управления функцией If(). Он выполняет сравнение в неправильном порядке битов. Цифровой компаратор начинает со старшего бита (MSB) и спускается к младшему биту. Я использую reversed(range()), чтобы сделать заказ правильно.

Сначала некоторые предварительные сведения:

from z3 import *
from functools import *

s = Solver()

Сравнение двух логических векторов, интерпретируемых как числа без знака, равнозначно лексикографическому (то есть словарному) порядку. Итак, давайте сначала напишем предикат, который проходит по двум спискам одинаковой длины и определяет, является ли первый большим или равным второму:

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

Теперь, когда у нас есть метод, который сравнивает два битовых вектора, давайте напишем еще один, который возвращает больший из двух заданных векторов. Мы делаем это, объявляя переменную fresh, чтобы мы могли сохранить результат сравнения, гарантируя, что результат сравнения будет общим для целей эффективности:

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

Собрав эти две части вместе, все, что нам нужно, — это уменьшить набор векторов, вернув наибольший элемент. Для этого воспользуемся функцией reduce из functools:

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

И вот ваш тестовый код, адаптированный для работы с этими определениями:

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])

Это печатает:

sat
[True, True, True, False]

чего вы и ожидали.