使用Z3解决偏序理论时，哪种编码更可取？

Question

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

该问题已经以各种方式受到约束，并使用QF_逻辑变体(主要是LIA或LRA )。

我有额外的约束，我可以用偏序来表示，以if变量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

尽可能避免使用量词。SMT求解器并不擅长使用它们，特别是在理论的组合中。如果你能坚持使用Int或Real，那就太好了。如果你可以使用位向量，那就更好了，因为即使在非线性函数存在的情况下，逻辑仍然是可判定的。

如果您的模型确实需要量词，我认为SMT求解器根本不是一个很好的匹配。在这种情况下，可以看看半自动系统，如Isabelle、Coq、HOL等。

Answer 2

你也可以尝试特殊关系的内置功能。至少它们改善了实例化偏序公理的二次开销。内置的偏序关系是自反的，所以如果你想要一个无自反的版本，那么定义一个宏来排除自反的情况。(_ 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)