Все-за исключением ограничений в Z3 - PullRequest
Новая
       89

Все-за исключением ограничений в Z3

1 голос
/ 20 марта 2020

Есть ли способ сгенерировать все-иное, кроме ограничения в Z3 только с O (n) операторами? Я знаю, что XCSP3 предлагает это.

В настоящее время это можно сделать так с помощью операторов O (n ^ 2): 

for i in range(len(G) - 1):
    s.add( [ Or(G[i] == 0, G[i] != G[j]) for j in range(i + 1, len(G)) ] )

Если это имеет значение, я интересует сравнение битовых векторов.

1 Ответ

2 голосов
/ 21 марта 2020

Z3 имеет предикат Distinct, который гарантирует, что все элементы различны, но, насколько мне известно, нет встроенного distinct-except.

Для кодирования такого рода ограничения, Я бы использовал массив для отслеживания мощности вставленных элементов. Примерно так: 

from z3 import *

def distinct_except(G, ignored):
   if len(G) < 2:
       return BoolSort().cast(True)

   A = K(G[0].sort(), 0);
   for i in range(len(G)):
       A = Store(A, G[i], If(G[i] == ignored, 0, 1 + Select(A, G[i])))

   res = True
   for i in range(len(G)):
       res = And(res, Select(A, G[i]) <= 1)

   return res

Мы просто вставляем элементы в массив, увеличивая счет на 1, если элемент не игнорируется, в противном случае добавляем 0. Это позволяет избежать дорогостоящих узлов if-then-else как массив построен линейно. Затем мы снова пройдемся по списку и убедимся, что никогда не сохранили ничего больше 1.

. Размеры выражений res и A останутся линейными, и z3 сможет справиться с этим. довольно эффективно. Я хотел бы услышать, если вы найдете иначе.

Вот несколько тестов, чтобы увидеть его в действии: 

# Test: Create four variables, assert they are distinct in the above sense
a, b, c, d = BitVecs('a b c d', 32)
s = Solver()
s.add(distinct_except([a, b, c, d], 0))

# Clearly sat:
print s.check()
print s.model()

# Add a constraint that a and b are equal
# Still SAT, because we can make a and b 0
s.add(a == b)
print s.check()
print s.model()

# Force a to be non-zero
s.add(a != 0)

# Now we have unsat:
print s.check()

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

sat
[b = 1024, a = 16, c = 1, d = 536870912]
sat
[c = 33554432, a = 0, d = 32768, b = 0]
unsat

Обратите внимание, что вы всегда можете использовать print s.sexpr(), чтобы увидеть выражения, которые вы строите, прежде чем вызывать s.check(), чтобы увидеть, как они растут по мере увеличения ваших входных списков.

...