Z3 中的多值逻辑

Question

我研究了一个 5 值命题逻辑，其中存在五个而不是两个真值，我想使用 Z3 来推理这个逻辑。

为了简单起见，假设真值是集合{0,...,4}的元素（这实际上是一种简化，但应该足以说明我的问题），它配备了自然顺序这些元素。由于此逻辑不再是二进制的，因此显然需要对运算符进行不同的定义。运算符举例如下：

a and b = min{a, b}
a or b = max{a, b}
not a = 4 - a

现在，我想用Z3来推理这个逻辑中的（无量词）公式，比如a or (not b)。但是，我不知道 (a) 最简单和 (b) 最有效的方法是教 Z3 这个。

我想一个简单的解决方案是使用枚举排序（虽然我还没有设法在不出错的情况下定义它们）来模拟真值和宏来定义运营商。那是要走的路吗？

Answer 1

枚举或 FiniteDomain 排序可能会完成这项工作或自定义数据类型。此外，编码为 bit-vectors 是可能的。根据您稍后想要证明的属性，其中一些可能比其他的更适合，但我会直接选择 bit-vectors，因为它们支持许多不同的特性和功能，并且通常可以有效地解决它们，至少对于'simple' 属性。当然，您的里程可能会有所不同。

Answer 2

我建议使用以下编码。正如 Christoph 提到的，QF_BV 对于给定的问题非常有效。

(set-logic QF_BV)
(define-fun myor ((A (_ BitVec 3)) (B (_ BitVec 3))) (_ BitVec 3)
    (ite (bvugt A B) A B))
(define-fun myand ((A (_ BitVec 3)) (B (_ BitVec 3))) (_ BitVec 3)
    (ite (bvult A B) A B))
(define-fun myneg ((A (_ BitVec 3))) (_ BitVec 3)
    (bvsub #b100 A))
(declare-fun a () (_ BitVec 3))
(assert (bvult a #b101))
(declare-fun b () (_ BitVec 3))
(assert (bvult b #b101))
(declare-fun c () (_ BitVec 3))
(assert (bvult c #b101))

;; test:
(define-fun demorgan () Bool
    (= (myand a b) (myneg (myor (myneg a) (myneg b)))))
(assert (not demorgan))

; (apply (then simplify bit-blast))
(check-sat-using (then simplify solve-eqs (repeat bit-blast) sat) :print_model true)

请注意，对于每个原子 proposition/variable X，您需要添加 (assert (bvult X #b101)).

Z3 中的多值逻辑

Multi-valued logic in Z3

logic

z3