Z3中的多值逻辑答案

【问题标题】：Multi-valued logic in Z3Z3中的多值逻辑
【发布时间】：2016-05-03 01:00:51
【问题描述】：

我研究了一个 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这个。

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

【问题讨论】：

标签： logic z3

【解决方案1】：

我建议使用以下编码。正如 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)

请注意，对于每个原子命题/变量 X，您需要添加 (assert (bvult X #b101))。

【讨论】：

【解决方案2】：

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

【讨论】：