z3py 对 Exists 可满足数量的强制约束

Question

我对 z3/z3py 很陌生。

我的目标：

假设我有一个大小为 5 的 IntVector。我有 5 个 Exists(...) 表达式，并且想将 exists expressiosn 是 true 还是 false 作为 1 和 0 存储在相应位置的 IntVector 中。最后，我想将 Sum(IntVector) 的约束设置为一个数字，表示必须有这么多的 Exists 表达式为真，其余为假。我不关心 Exists 表达式是否可满足，我唯一期望的是一定数量的 Exists 表达式是否为真。

我的问题：

我只是使用求解器并将上述所有假设添加到其中以检查可满足性。上面的实现耗时很长returns"unknown"。但是，如果我只检查一个 Exists 表达式而不添加 true Exists 表达式数量的约束，我将在短时间内得到 sat 或 unsat。如果我一起检查所有 Exists 表达式而不添加 true Exists 表达式数量的约束，我将得到不满意的（因为一些 Exists 表达式本质上是不满意的）。我觉得战术和子目标可能会解决我的问题。但是我对它们的了解还不够

我希望我上面的问题是有道理的。有人可以在这里给我一些指示吗？

Answer 1

也许您可以将其视为最大卫星问题。我最近向 Z3 添加了优化功能，它允许您设置软约束。此外，解决 Exists(x1, Fml(x1)) 的可满足性相当于解决 Fml(x1) 的可满足性，其中 x1 是一个自由常数。所以听起来存在闭包是一种矫枉过正。

示例：

 (define-fun f1 ((x Int)) Bool < definition of formula f1 >)
 (define-fun f2 ((x Int)) Bool < definition of formula f2 >)
 (define-fun f3 ((x Int)) Bool < definition of formula f3 >)
 (declare-const x1 Int)
 (declare-const x2 Int)
 (declare-const x3 Int)

 (assert-soft (f1 x1))
 (assert-soft (f2 x2))
 (assert-soft (f3 x3))

 (check-sat)

结果将最大化满足软约束的数量。部分输出是违反软约束的数量。

z3py 对 Exists 可满足数量的强制约束

z3py cast constraint on number satisfiable of Exists

exists

smt

z3

z3py