Блог

Допустим, у меня есть ограничения: x < 2 , x > 3 и x > 5 , как мне заставить z3 создавать минимальные решения, например x = [1, 6] ?

Я полагаю, что могу реализовать это с помощью Or и блокировать решаемое условие для каждого решения, но это не гарантирует, что оно создаст минимальный набор.

Мое другое решение состоит в том, чтобы решать каждое условие индивидуально и собирать как можно больше результатов, и иметь алгоритм для выбора перекрывающегося результата для каждого условия.

Есть идея?

Такого рода ограничения «отслеживания» возникают часто. Хотя может быть несколько решений, я думаю, что лучшим решением является явное добавление переменных отслеживания и повторение до тех пор, пока не будут выполнены все ограничения. Для этой цели вы должны использовать оптимизирующий решатель, максимизирующий количество ограничений, которые снимаются при каждом вызове. Таким образом, вы гарантируете, что количество решений остается минимальным.

Основываясь на этой стратегии, я бы создал переменную отслеживания pN для каждого ограничения и связал их с импликацией. Тогда я бы максимизировал количество pN , которое должно быть удовлетворено. Вот возможная кодировка:

 from z3 import *

x = Int('x')

p1, p2, p3 = Bools('p1 p2 p3')
constraints = [(p1, x < 2), (p2, x > 3), (p3, x > 5)]

solutions = []
while constraints:
    o = Optimize()

    s = 0
    for (tracker, condition) in constraints:
        o.add(Implies(tracker, condition))
        s = s   If(tracker, 1, 0)
    o.maximize(s)

    remaining = []
    r = o.check()
    if r == sat:
        m = o.model()
        solutions.append(m[x])
        print("Candidate: %s" % m[x])
        for (tracker, condition) in constraints:
            if(m[tracker]):
                print("  Constraint: %s satisfied, skipping." % condition.sexpr())
            else:
                print("  Constraint: %s is not yet satisfied, adding." % condition.sexpr())
                remaining.append((tracker, condition))
    else:
        print("Call returned: %s" % r)
        exit(-1)

    constraints = remaining

print("Solution: %s" % solutions)
  

При запуске выводится:

 Candidate: 6
  Constraint: (< x 2) is not yet satisfied, adding.
  Constraint: (> x 3) satisfied, skipping.
  Constraint: (> x 5) satisfied, skipping.
Candidate: 0
  Constraint: (< x 2) satisfied, skipping.
Solution: [6, 0]
  

Итак, это вычисляет решение [6, 0] . Вы изначально хотели [1, 6] , но я считаю, что это тоже правильное решение.

Если вы также хотите получить более жесткие границы, вы также можете добавить условия в оптимизирующий решатель (с помощью вызовов минимизации / максимизации). Однако это, вероятно, приведет к проблемам: например, для вашего исходного набора ограничений нет минимального / максимального значения x , которое удовлетворяло бы им однозначно, поэтому вы можете столкнуться с ситуациями, когда оптимизатор потерпит неудачу. Если вы знаете, что все ваши переменные ограничены, вы можете пойти по этому маршруту. В противном случае вы можете попробовать вызвать оптимизатор, и если он не возвращает фиксированный результат, перейдите к результату sat вызова, как я сделал выше. Конечно, все это зависит от конкретных ограничений, которые у вас есть, но в остальном не имеет отношения к z3.

Я думаю, что x <2, x> 3 и x> 5 не имеют решений. Вы можете найти первое решение, а затем добавить его в условие. Например

 from z3 import *
solver = Solver()
x = Int('x')

constraints = [
    x < 5
]

for i in constraints:
    solver.add(i)
print(solver.check())
while solver.check() == sat:
    print(solver.model()[x])
    solver.add(x < solver.model()[x])

Output:
sat
4
0
-1
-2
-3
-4
-5
-6
-7
....
-to minus infinity
  

Второе решение

  from z3 import *
import itertools
solver = Solver()
x = BitVec('x', 64)

combinations = [
    x < 2,
    x > 3,
    x > 5
]

#I create a list of all possible combinations of conditions
stuff = [0, 1, 2]
conditionLst = []
for L in range(0, len(stuff) 1):
    for subset in itertools.combinations(stuff, L):
        conditionLst.append(subset)
print(conditionLst)


#for every combination I am looking for solutions
for cond in conditionLst:
    solver = Solver()
    for i in cond:
        solver.add(combinations[i])
    solver.check()
    if solver.check() == sat:
        for j in cond:
            print(combinations[j], end=", ")
        print(solver.model())
    elif solver.check() == unsat:
        for j in cond:
            print(combinations[j], end=", ")
        print(solver.check())
    del solver


x < 2, [x = 1]
x > 3, [x = 4]
x > 5, [x = 6]
x < 2, x > 3, unsat
x < 2, x > 5, unsat
x > 3, x > 5, [x = 6]
x < 2, x > 3, x > 5, unsat
  

Если нет решения для всех комбинаций сразу, перейдите на уровень ниже. Если есть решения для 2 условий, то посмотрите, есть ли решения для третьего. Вы можете создать алгоритм для этого.