哪种编码更适合使用 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

您还可以尝试特殊关系的内置功能。 至少他们改进了实例化的二次开销 偏序公理。内置的偏序关系是自反的， 因此，如果您想要一个非反身版本，请定义一个排除的宏 反射性案例。(_ 偏序 0( 是一个关系，它接受两个相同类型的参数并返回一个布尔值。(_ 偏序 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等。