在 SMTLib 中对谓词逻辑进行建模确实是可能的;尽管与 Isabelle/HOL 等常规定理证明器相比,它可能有点麻烦。并且解释结果可能需要相当多的眯眼。
话虽如此,这里是使用 SMTLib 对示例问题的直接编码:
(declare-sort A)
(declare-sort B)
(declare-sort C)
(declare-fun q (A B C) Bool)
(declare-fun p (A B C) Bool)
(assert (forall ((b B))
(exists ((a A))
(exists ((c C)) (or (p a b c) (q a b c))))))
(check-sat)
(get-model)
一些注意事项:
-
declare-sort
创建未解释的排序。它本质上是一组非空值。 (也可以是无限的,除了它不为空的事实之外,没有做出任何基数假设。)对于您的具体问题,这种类型实际上是什么并不重要,因为您没有使用它的任何直接元素。如果这样做,您可能还想尝试“声明”排序,即数据类型声明。这可以是一个枚举,或者更复杂的东西;取决于问题。对于当前提出的问题,未解释的排序就可以了。
-
declare-fun
告诉求解器有一个具有该名称和签名的未解释函数。但除此之外,它既不定义它,也不以任何方式限制它。您可以添加有关它们的“公理”,以更具体地说明它们的行为方式。
-
支持量词,如您所见forall
and exists
在如何你的constraint1
被编码。请注意,SMTLib 不太适合代码重用,通常在更高级别的绑定中进行编程。 (提供了来自 C/C++/Java/Python/Scala/O'Caml/Haskell 等的绑定,具有类似但不同程度的支持和功能。)否则,它应该易于阅读。
-
我们终于发出check-sat
and get-model
,要求求解器创建一个满足所有断言约束的宇宙。如果是这样,它将打印sat
并且会有一个模型。否则,它会打印unsat
如果没有这样的宇宙;或者它也可以打印unknown
(或永远循环!)如果它无法决定。量词的使用对于 SMT 求解器来说是很难处理的,大量使用量词无疑会导致unknown
作为答案。这是一阶谓词演算的半可判定性的固有限制。
当我通过 z3 运行此规范时,我得到:
sat
(
;; universe for A:
;; A!val!1 A!val!0
;; -----------
;; definitions for universe elements:
(declare-fun A!val!1 () A)
(declare-fun A!val!0 () A)
;; cardinality constraint:
(forall ((x A)) (or (= x A!val!1) (= x A!val!0)))
;; -----------
;; universe for B:
;; B!val!0
;; -----------
;; definitions for universe elements:
(declare-fun B!val!0 () B)
;; cardinality constraint:
(forall ((x B)) (= x B!val!0))
;; -----------
;; universe for C:
;; C!val!0 C!val!1
;; -----------
;; definitions for universe elements:
(declare-fun C!val!0 () C)
(declare-fun C!val!1 () C)
;; cardinality constraint:
(forall ((x C)) (or (= x C!val!0) (= x C!val!1)))
;; -----------
(define-fun q ((x!0 A) (x!1 B) (x!2 C)) Bool
(and (= x!0 A!val!0) (= x!2 C!val!0)))
(define-fun p ((x!0 A) (x!1 B) (x!2 C)) Bool
false)
)
这需要眯起眼睛才能完全理解。第一组值告诉您求解器如何为未解释的排序构建模型A
, B
, and C
;具有见证元素和基数约束。尽管它确实包含有用的信息,但大多数情况下您可以忽略这部分。例如,它告诉我们A
是一个包含两个元素的集合(名为A!val!0
and A!val!1
),也是如此C
, and B
只有一个元素。根据您的限制,您将获得不同的元素集。
For p
, 我们看:
(define-fun p ((x!0 A) (x!1 B) (x!2 C)) Bool
false)
这意味着p
总是False
;即,无论传递给它的参数是什么,它都是空集。
For q
we get:
(define-fun q ((x!0 A) (x!1 B) (x!2 C)) Bool
(and (= x!0 A!val!0) (= x!2 C!val!0)))
让我们更简单地重写一下:
q (a, b, c) = a == A0 && c == C0
where A0
and C0
是这样的成员A
and C
分别;请参阅上面的排序声明。所以,它说q
is True
每当a
is A0
, c
is C0
,并且什么都不重要b
is.
您可以让自己相信这个模型确实满足您想要的约束。
总结;在 z3 中对这些问题进行建模确实是可能的,尽管有点笨拙和大量使用量词可能会使求解器永远循环或返回unknown
。解释输出可能有点麻烦,尽管您会意识到模型将遵循类似的模式:首先是未解释的排序,然后是谓词的定义。
边注
正如我提到的,在 SMTLib 中对 z3 进行编程既麻烦又容易出错。这是使用 Python 接口完成的相同程序:
from z3 import *
A = DeclareSort('A')
B = DeclareSort('B')
C = DeclareSort('C')
p = Function('p', A, B, C, BoolSort())
q = Function('q', A, B, C, BoolSort())
dummyA = Const('dummyA', A)
dummyB = Const('dummyB', B)
dummyC = Const('dummyC', C)
def teaches(a, b):
return Exists([dummyC], Or(p(a, b, dummyC), q(a, b, dummyC)))
constraint1 = ForAll([dummyB], Exists([dummyA], teaches(dummyA, dummyB)))
s = Solver()
s.add(constraint1)
print(s.check())
print(s.model())
这也有一些特性,但如果您选择在 Python 中对 z3 进行编程,希望它能为您的探索提供一个起点。这是输出:
sat
[p = [else -> And(Var(0) == A!val!0, Var(2) == C!val!0)],
q = [else -> False]]
它具有与 SMTLib 输出完全相同的信息,但编写方式略有不同。
函数定义风格
请注意,我们定义了teaches
作为常规 Python 函数。这是 z3py 编程中的常见风格,因为它生成的表达式会在调用时被替换。您还可以创建一个 z3 函数,如下所示:
teaches = Function('teaches', A, B, BoolSort())
s.add(ForAll([dummyA, dummyB],
teaches(dummyA, dummyB) == Exists([dummyC], Or(p(dummyA, dummyB, dummyC), q(dummyA, dummyB, dummyC)))))
请注意,这种定义风格将依赖于内部量词实例化,而不是 SMTLib 的通用函数定义工具。因此,您通常应该更喜欢 python 函数风格,因为它可以转换为“更简单”的内部结构。一般来说,它的定义和使用也更容易。
您需要 z3 函数定义样式的一种情况是,如果您定义的函数是递归的并且其终止依赖于符号参数。有关此问题的讨论,请参阅:https://stackoverflow.com/a/68457868/936310 https://stackoverflow.com/a/68457868/936310