Z3py 计算 row/column 的元素直到达到特定条件

Question

我正在为学校项目的游戏 0h_n0 使用 Z3py 开发 SMT 求解器。（游戏可以在这里找到 0h_n0）。如果您不熟悉该游戏，它涉及网格上的蓝点和红点，给定的蓝点具有 1-[grid-size] 的整数值。具有数字值的蓝点必须在其行和列中“看到”与其数字值完全一样多的蓝点。蓝点无法“看到”过去的红点，因此相对于所讨论的蓝点，红点后面的任何蓝点都不应计入其“看到”值。

我无法准确计算给定蓝点可以看到多少个其他蓝点。我有一组变量定义为：

X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(DIMENSION) ]
    for i in range(DIMENSION) ]

和一个看起来像这样的实例：

instance = ((-1, -1, -1, 1, -1),
            (2, -1, 5, 0, -1),
            (-1, 3, 4, -1, 3),
            (1, -1, -1, 0, -1),
            (3, -1, -1, -1, 0))

空白单元格由 -1 表示，红点由 0 表示，蓝点由对应于它应该“看到”的蓝点数的正整数表示

我有一些函数可以准确地确定给定 X[行][列] 的行或列中存在的蓝点总数，但是，它们不考虑“阻挡给定 X[行][列] 的视图”。

下面是一些输出，显示与上述实例的每个单元格相同的列中的蓝点总数：

 [[3, 1, 2, 0, 1],
 [2, 1, 1, 1, 1],
 [3, 0, 1, 1, 0],
 [2, 1, 2, 1, 1],
 [2, 1, 2, 1, 1]]

注意：点不能“看到”自己

因此，例如，我希望能够做这样的事情，看看在给定的 X[行][列] 下方可以看到多少个蓝点，并且没有被红点遮挡：

def sum_bottom(element, i, j):
        count = Sum(0, 0)
        for c in range (i+1, DIMENSION):
            if ((X[c][j])/(X[c][j]) == 0):
                break
            else:
                count = Sum(count, (X[c][j])/(X[c][j]))
        return count

然而，问题是 if ((X[c][j])/(X[c][j]) == 0) 从未真正令人满意，因为（据我所知）(X[c][j])/(X[c][j]) 只是一个符号而不是具体值。

任何关于如何在 Z3py 中编写此约束的建议都将不胜感激。让我知道是否有任何不清楚的地方，或者显示更多我的代码是否有帮助，我会根据需要提供。干杯！

Answer 1

有趣的示例，非常适合 SMT 求解器！

在符号编程中，您还需要符号化地执行条件。也就是说，使用 z3py 的 If 而不是 Python 的 if。这是一个让您入门的更简单的示例。假设我们的数组 X 只是一维的，我们只能看到“右边”。（即，每个蓝色单元格计算它右边的那些，而不是左边的。）一些预备知识：

from z3 import *

N = 5
X = [Int("x_%d" % i) for i in range(N)]

s = Solver()

RED = -1

在上面，我用 -1 表示 RED，因为你需要能够告诉一个 BLUE 单元格，用 0 看不到任何其他东西。当然，您也可以安排一些其他设置。另外，我刚刚声明了一个包含 5 个单元格的一维网格。此外，我从 0 开始计数，这使编程更容易，但如果您愿意，也可以从 1 开始计数。

现在，计数的想法是检查一个单元格是否被阻塞并停止计数，或者以其他方式添加单元格直到被阻塞。除了，我们必须象征性地继续使用条件而不是停止：

def value(i):
  count     = 0
  isBlocked = False
  for c in range(i+1, N):
    count = If(isBlocked, count, If(X[c] >= 0, count+1, count))
    isBlocked = Or(isBlocked, X[c] == RED)

  return count

注意我们如何使用 If 和 Or 函数来查看计数应该如何递增，以及我们是否应该被阻止。否则，for 循环从位置 i+1 开始运行整个序列长度。如果愿意，您可以在总结所有可能的配置时考虑这一点。

现在你可以问 z3py value 的某些值是什么：

>>> value(4)
0
>>> value(3)
If(False, 0, If(x_4 >= 0, 1, 0))
>>> value(2)
If(Or(False, x_3 == -1),
   If(False, 0, If(x_3 >= 0, 1, 0)),
   If(x_4 >= 0,
      If(False, 0, If(x_3 >= 0, 1, 0)) + 1,
      If(False, 0, If(x_3 >= 0, 1, 0))))

我将省略 value(1) 和 value(0) 的输出，因为它们相当大。但是研究这个输出并说服自己这是正确的做法是有益的。（还要记住，我实施的规则与您原来的游戏不同；所以它更简单一些。您必须相应地进行修改。）

你如何使用它？首先，我们需要告诉 z3 一个单元格是 RED 或者其中的值等于 value 函数计算的值：

s = Solver()
for c in range(N):
  s.add(Or(X[c] == RED, X[c] == value(c)))

为了让它有点有趣，我们还假设我们希望 X[3] 成为一个 BLUE 单元格，它只能看到右侧的 1 个蓝色单元格：

s.add(X[3] == 1)

现在我们可以计算：

>>> print(s.check())
sat
>>> m = s.model()
>>> print([m.eval(X[i], model_completion=True) for i in range(N)])
[-1, -1, 2, 1, 0]

所以，z3 说一个令人满意的配置是：

RED RED BLUE(2) BLUE(1) BLUE(0)

事实上，这遵循了我们在上面实施的（修改后的）规则和约束。

一旦您对此进行了试验并熟悉了 z3 中的符号编程，看看您是否可以将其扩展到二维并通过实现原始规则从那里获取它。玩得开心！

Z3py 计算 row/column 的元素直到达到特定条件

Z3py counting elements of a row/column up until a certain condition

python

z3

z3py