时间戳

首页 > 解决方案 > z3py：按字典顺序破坏对称性约束

z3 - z3py：按字典顺序破坏对称性约束

问题描述

我有两个整数变量数组（它们代表二维空间坐标），一个是另一个的对称配置。为了打破对称性，我想检查第一个数组（我们称之为 P）描述的找到的解决方案相对于对称解决方案是否按字典顺序排列（所以我可以丢弃对称解决方案）。无论如何，我在编写一个检查字典顺序的函数时遇到了麻烦：

到目前为止（但它是不正确的），我想出了这个：

from z3 import *
from math import ceil

width = 8
blocks = 4
x = [3, 3, 5, 5]
y = [3, 5, 3, 5]

# [blocks x 2] list of integer variables
P = [[Int("x_%s" % (i + 1)), Int("y_%s" % (i + 1))]
     for i in range(blocks)]

# value/ domain constraint
values = [And(0 <= P[i][0], P[i][0] + x[i] <= width, 0 <= P[i][1])  # , P[i][1] + y[i] <= height)
          for i in range(blocks)]

# no overlap constraint
no_overlap = [Or(i == j,  # indices must be different
                 Or(P[j][0] + x[j] <= P[i][0],  # left
                    P[j][0] >= P[i][0] + x[i],  # right
                    P[j][1] + y[j] <= P[i][1],  # down
                    P[j][1] >= P[i][1] + y[i]  # up
                    ))
              for j in range(blocks) for i in range(blocks)]


# Return maximum of a vector; error if empty
def symMax(vs):
    maximum = vs[0]
    for value in vs[1:]:
        maximum = If(value > maximum, value, maximum)
    return maximum


obj = symMax([P[i][1] + y[i] for i in range(blocks)])


def symmetric(on_x, on_y):
    if on_x and on_y:
        return [[width - P[block][0] - x[block], obj - P[block][1] - y[block]] for block in range(blocks)]
    elif on_x:
        return [[width - P[block][0] - x[block], P[block][1]] for block in range(blocks)]
    elif on_y:
        return [[P[block][0], obj - P[block][1] - y[block]] for block in range(blocks)]

#function I want to emulate
def lexicographic_order(a1, a2):
    for a, b in zip(a1, a2):
        if a < b:
            return True
        if a > b:
            return False
    return True

# my attempt: raise error "Z3 AST expected"
def lexSymb(a1, a2):
    for a, b in zip(a1, a2):
        tmp = If(a < b, True, False)
    if tmp.eq(True):
        return True
    tmp = If(a > b, False, True)
    if tmp.eq(False):
        return False
return True

lex_x = lexSymb1(P, symmetric(True, False))
lex_y = lexSymb1(P, symmetric(False, True))
lex_xy = lexSymb1(P, symmetric(True, True))

board_problem = values + no_overlap + lex_x + lex_y + lex_xy

o = Optimize()
o.add(board_problem)
o.minimize(obj)

if o.check() == sat:
    print("Solved")

elif o.check() == unsat:
    print("The problem is unsatisfiable")
else:
    print("Unexpected behaviour")

让我知道是否可以以与符号表达式一起使用的方式修改“lexicographic_order()”，或者是否有另一种我没见过的方法。

标签： z3smtz3pylexicographiclexicographic-ordering

解决方案

你说你想要一个符号版本：

def lexicographic_order(a1, a2):
    for a, b in zip(a1, a2):
        if a < b:
            return True
        if a > b:
            return False
    return True

我不认为这是你想要的。为什么？请注意，在 Python 中，return立即退出该函数。所以，这只会比较这些列表的第一个元素（假设它们是非空的），并立即返回。我不认为这是你想要的。

字典顺序通常意味着您必须比较整个列表。这就是您象征性地编码的方式：

# Does a1 come before a2 lexicographically?
# We assume a1 != a2. If same, the algorithm will produce True.
def precedes(a1, a2):
    if not a1:
        return True
    if not a2:
        return False
    return Or(a1[0] < a2[0], And(a1[0] == a2[0], precedes(a1[1:], a2[1:])))

看看这个函数是如何工作的是很有启发性的。首先是一个具体的价值：

> print(precedes([1,2,3],[4,5,6]))
Or(True,
   And(False,
       Or(True, And(False, Or(True, And(False, True))))))

请注意，如果第一个列表按字典顺序排列在第二个之前，我们会构建“计算”的 AST。上面的表达式简化True为您可以轻松验证自己，但我们不计算 True，我们构建其值为 的表达式True。当我们在符号值上运行它时，这种结构的重要性变得显而易见：

> print(precedes([Int('a'), Int('b')], [Int('c'), Int('d')]))
Or(a < c, And(a == c, Or(b < d, And(b == d, True))))

现在你看到了这个值是如何“象征性地”计算出来的，并且做了你想要它做的事情：它会True准确地计算出第一个列表在字典上排在第二个之前的时间。当您向求解器断言这是一个事实时，它将对该模型施加该约束。

希望这能让你继续前进。您需要考虑“构建”符号表达式，因此 Python 的内部if-then-else不是您可以使用的，因为它不能正确处理符号值。

推荐阅读