z3 - Z3 bool 变量的算术运算

Question

我在 Z3 中有一堆布尔变量，比如ai,bj和ck, 来制定我的 SAT 问题。但是，在我的问题中，需要考虑三个算术约束：

a1 + a2 + a3 + ... + an = 1
b1 + b2 + b3 + ... + bn = 0
c1 + c2 + c3 + ... + cn <= 1

如何在不更改变量类型的情况下使用 Z3 API 制定这三个算术约束（即，默认情况下都是布尔值）？

Answer 1

您可以将布尔值嵌入到 if 表达式中，例如，您可以编写

  if(a1,1,0) + if(a2,1,2) + ...

作为一个有点特殊用途的功能，此时还可以使用 C、.NET 和 Java API 的内置基数运算符直接输入基数约束，而不是 python 或 Ocaml。此外，lia2pb 策略转换使用 if-then-else 表达式（如上）的目标，并将它们转换为伪布尔约束。