1

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

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

我有额外的约束，我可以用偏序来改进解决方案，形式为 if variable 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 具有更多的属性。

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

4

2 回答 2

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)
于 2019-12-08T13:08:09.237 回答
1

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

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

于 2019-12-03T18:54:06.323 回答