Z3 bool 变量的算术运算

【问题标题】：Arithmetic operation on Z3 bool variableZ3 bool 变量的算术运算
【发布时间】：2015-10-28 22:24:31
【问题描述】：

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

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

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

【问题讨论】：

【解决方案1】：

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

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

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

【讨论】：

您好 Nikolai，感谢您的回复。你能更具体一点吗？我不太明白这个。
if 表达式将第一个参数作为条件求值。如果条件为真，则表达式返回第二个参数。如果条件为假，则返回第三个参数。在 SMT 语法中，这称为 ITE 或 if-then-else 运算符。 If 表达式允许从布尔到整数的优雅转换。基数约束定义了有多少变量必须评估为真。它可以是 at-least-k、at-most-k、exactly-k 或 between-n-and-m 类型。