SMTlib 非重叠但互补的位向量答案

【问题标题】：SMTlib non overlapping but complementary BitvectorsSMTlib 非重叠但互补的位向量
【发布时间】：2022-02-01 21:42:03
【问题描述】：

我正在努力尝试在 SMTlib 中生成正确的断言。使用 QV_BV（位向量）理论。我使用 Python 生成temp.smt2 文件，然后使用z3 运行它。目标是在任意数量的向量中断言：

成对连接必须是#b0000000...00，即全为零
总析取必须为#b1111111...11，即全部为1

粗略地说，每个向量代表一个员工的时间表，要求是所有时间表的时段必须一次只能由一名员工占用，但必须占用所有时段。

示例如下：

(1)   |  (2)   |  (3)
      |        |
1010  |  1000  |  1000
1001  |  0100  |  0110
0100  |  0010  |  0001
----  |  ----  |  ----   <--- "disjunction"
1111  |  1110  |  1111
      |        | 
fail  |  fail  |  sat!

示例 1 是 UNSAT，因为尽管所有插槽都已被占用，前两个位向量之间存在冲突

示例 2 是 UNSAT，因为并非所有插槽都已占用。结果的 LSB 为 0。

示例 3 是 SAT，因为所有时隙都已占用且没有冲突。

我尝试了以下方法（N 和 M 是任意数字）：

(set-logic QF_BV)

(declare-const x0 (_ BitVec M))
(declare-const x1 (_ BitVec M))
...
(declare-const xN (_ BitVec M))

(assert (= #b00000...00 (bvand x0 x1 ... xN)))
(assert (= #b11111...11 (bvor x0 x1 ... xN)))

(check-sat)
(get-model)

直到后来我才注意到这是不够的。允许重叠的析取（OR-ing）。然后我考虑了其他的按位运算，我很快就迷路了。例如，对多个项进行异或运算可能是不可预测的，因为：

xor(1, 0, 1, 0, 1) == xor(1, xor(0, xor(1, xor(0, 1)))) == 0
xor(1, 0, 1, 1) == xor(1, xor(0, xor(1, 1))) == 1

我可以使用 Python 在 smt2 文件中生成每个成对断言。但是由于我有任意多个位向量，因此可能会导致高复杂性。例如，给定 100 个位向量，有 4950 对，因此有 4950 个断言。我希望我们能做得更好。

那么什么是可能的解决方案？谢谢！

编辑：请注意，我没有使用 z3py。我正在写入 .smt2 文件

【问题讨论】：

这些是否需要特别是位向量，或者这只是一种方便的分组机制？您所描述的是“最多 k / 精确 k”约束，它对单个布尔变量（即伪布尔求解）进行了很好的研究。对你来说，k=1 并且你通过 at-least-1 + at-most-1 精确地追求 1。 Z3supports such constraints natively。但分组为位向量，据我所知，您只需要“撤消”它并再次处理各个位。

标签： bitwise-operators z3 smt bitvector

【解决方案1】：

最好的办法是保留 NxM 布尔值，而不是 N M 位向量。然后，您要断言设置了每一列中的一个。（请注意，您不再需要 or 他们，因为第一个约束将处理它。）

要断言其中一个为真，您可以使用 z3 支持的PbEq。或者您可以为每个集合布尔值加 1，并断言总和为 1，如果您想要通用的话。

请注意，如果您愿意，您仍然可以使用位向量，如果这有助于解决问题的其他部分。如果是这种情况，还要创建 NxM 布尔值并相应地设置它们。（使用对extract 的调用。）然后您可以同时拥有两种表示形式并使用最合适的表示形式。

PS：你说你没有使用 z3py。如果你这样做了，那肯定会简化你的编码。请注意，您始终可以使用求解器的 sexpr 方法将 z3py 程序转换为简单的 SMTLib。除非你有其他理由不这样做，否则我肯定会这样做。

【讨论】：