performance - Z3:if-then-else 与命题逻辑的性能对比

Question

在 Z3 中，有(至少)两种表达 if-then-else 的方式——使用 ite 表达式和使用命题逻辑:

(ite X Y Z)

(and (=> X Y) (=> (not X) Z))

第二个表达式的缺点是它重复了 X。如果 X 非常大(或者我们有很多这样的表达式)，这可能会显着增加项的大小。我们可以通过引入一个新变量来缓解这种情况，例如 X_is_true:

(and (= X_is_true X) (=> X_is_true Y) (=> (not X_is_true) Z))

我的问题是:ite 本质上是这些编码之一之上的语法糖吗？如果不是，它的时间/空间效率与这些编码相比如何？

Answer 1

My question is this: is ite essentially syntactic sugar on top of one of these encodings?

一般不会。在您的示例中，Y 和 Z 不需要是 Bool 类型。例如

(declare-fun a () Float64)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Bool)
(assert (= c (ite d a b)))
(check-sat)

您的转换在这里不起作用，因为 a 和 b 属于 Float64 而不是 Bool。从技术上讲，如果像这样将 ite 提升到 = 运算符之外，则可以应用您的转换

(declare-fun a () Float64)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Bool)
(assert (ite d (= c a) (= c b)))
(check-sat)

但是我不确定这样的转换是否总是可能的，而且您有时必须应用语义保留转换这一事实意味着您的转换不是语法糖。

编辑

how does its time/space efficiency compare with these encodings?

这很难回答，因为答案取决于您使用的逻辑和使用的解决方法。我也不太了解 Z3 的实现，无法给您一个好的答案。

然而，作为您调查的起点，您可以看看如果您尝试应用 Tseitin 变换会发生什么。这是急切地将问题转化为 SAT 时经常使用的步骤。但是请注意，这不是 Z3 将要执行的操作(它应用其 smt 策略，但工作方式不同)。

原创

(declare-const X Bool)
(declare-const Y Bool)
(declare-const Z Bool)
(assert (ite X Y Z))
(apply (and-then tseitin-cnf))

Z3 响应

(goals
(goal
  (or (not X) Y)
  (or X Z)
  :precision precise :depth 1)
)

编码1

(declare-const X Bool)
(declare-const Y Bool)
(declare-const Z Bool)
(assert (and (=> X Y) (=> (not X) Z)))
(apply (and-then tseitin-cnf))

Z3 响应

(goals
(goal
  (or (not X) Y)
  (or X Z)
  :precision precise :depth 2)
)

编码2

(declare-const X Bool)
(declare-const Y Bool)
(declare-const Z Bool)
(declare-const X_is_true Bool)
(assert (and (=> X_is_true Y) (=> (not X_is_true) Z)))
(assert (= X X_is_true))
(apply (and-then tseitin-cnf))

Z3 响应

(goals
(goal
  (or (not X_is_true) Y)
  (or X_is_true Z)
  (or X (not X_is_true))
  (or (not X) X_is_true)
  :precision precise :depth 2)
)