哪种编码更适合使用 Z3 来解决偏序理论？

Question

我正在考虑对偏序关系进行编码以提供 Z3 的多种方法。

问题已经以各种方式受到限制，并使用 QF_ 逻辑变体（主要是 LIA 或 LRA）。

我有额外的约束，我可以用偏序来优化解决方案，形式为，如果变量ei>0 => a0 precedes ai，其中ei 是我的问题的一个变量，而ai 变量是新的，并表示“先于”偏序约束。

因此，这种偏序将以多种方式限制根据 ei 获得的解。

一个解决方案可能是使用未解释的函数，例如这个例子： https://rise4fun.com/Z3/fZQc

; Coding a partial order precedes relation with UF
(declare-sort A)
(declare-fun pre (A A) Bool)
; non reflexive
(assert (forall ((x A)) (not (pre x x))))
; transitive
(assert (forall ((x A) (y A) (z A))
          (=> (and (pre x y) (pre y z)) 
              (pre x z)))) 
; anti symetric
(assert (forall ((x A) (y A))
          (=> (pre x y)  
              (not (pre y x)))))
; an UNSAT example
(declare-const a0 A)
(declare-const a1 A)
(declare-const a2 A)
(assert (pre a0 a1))
(assert (pre a1 a2))
(assert (pre a2 a0))
(check-sat)

这正是我想要表达的，但这也引入了一个新的量词逻辑。

另一种选择是将我的元素放入一个具体的域中，例如 Real 或 Int ： https://rise4fun.com/Z3/U0Hp

; Coding a partial order precedes relation with Real
; an UNSAT example
(declare-const a0 Real)
(declare-const a1 Real)
(declare-const a2 Real)
(assert (< a0 a1))
(assert (< a1 a2))
(assert (< a2 a0))
(check-sat)

代码更简单并且不使用量词，但它迫使（也许？）求解器过度思考，因为 Real 比第一个版本中的抽象域 A 具有更多的属性。

那么通常应该首选哪种编码来编码部分订单？ 是否有我应该考虑的其他参数，或者我可以配置哪些策略来帮助解决此类问题？

Answer 1

您还可以尝试特殊关系的内置功能。 至少他们改进了实例化的二次开销 偏序公理。内置的偏序关系是自反的， 所以如果你想要一个反身版本，那么定义一个排除的宏 反身案例。 (_ partial-order 0) 是一个关系，它接受两个相同类型的参数并返回一个布尔值。 (_ partial-order 1) 将是不同的关系，因此您可以使用参数索引不同的偏序。

(declare-sort A)
(define-fun pre ((x A) (y A)) Bool (and (not (= x y)) ((_ partial-order 0) x y)))
; an UNSAT example
(declare-const a0 A)
(declare-const a1 A)
(declare-const a2 A)
(assert (pre a0 a1))
(assert (pre a1 a2))
(assert (pre a2 a0))
(check-sat)

Answer 2

尽可能避免使用量词。 SMT 求解器对它们并不擅长，尤其是在理论组合方面。如果你能坚持Int 或Real，那就太好了。如果您可以使用位向量，那就更好了，因为即使存在非线性函数，逻辑也将保持可判定性。

如果您的模型确实需要量词，我认为 SMT 求解器根本不适合。在这种情况下，请查看 Isabelle、Coq、HOL 等半自动化系统。