我正在考虑对偏序关系进行编码以提供 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 具有更多的属性。
那么通常应该首选哪种编码来编码部分订单?是否有我应该考虑的其他参数,或者我可以配置的策略来帮助解决此类问题?