Z3 中的地板和天花板功能实现

Question

我已经尝试实现下面定义的 Floor 和 Ceiling 函数 link

https://math.stackexchange.com/questions/3619044/floor-or-ceiling-function-encoding-in-first-order-logic/3619320#3619320

但是Z3查询返回反例。

楼层函数

_X=Real('_X')
_Y=Int('_Y')
_W=Int('_W')
_n=Int('_n')
_Floor=Function('_Floor',RealSort(),IntSort())
..
_s.add(_X>=0)
_s.add(_Y>=0)
_s.add(Implies(_Floor(_X)==_Y,And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W ==_Y,_W<_Y))))))
_s.add(Implies(And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W==_Y,_W<_Y))),_Floor(_X)==_Y))
_s.add(Not(_Floor(0.5)==0))

预期结果 - 不满意

实际结果 - 星期六

上限函数

_X=Real('_X')
_Y=Int('_Y')
_W=Int('_W')
_Ceiling=Function('_Ceiling',RealSort(),IntSort())
..
..
_s.add(_X>=0)
_s.add(_Y>=0)
_s.add(Implies(_Ceiling(_X)==_Y,And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W ==_Y,_Y<_W))))))
_s.add(Implies(And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W==_Y,_Y<_W)))),_Ceiling(_X)==_Y))
_s.add(Not(_Ceilng(0.5)==1))

预期结果 - 不满意

实际结果 - 星期六

Answer 1

[您的编码不会加载到 z3，即使在删除“..”之后它也会出现语法错误，因为您对 Implies 的调用需要一个额外的参数。但我会忽略所有这些。]

简短的回答是，您不能在 SMT 求解器中真正执行此类操作。如果可以，那么您可以求解任意丢番图方程。只需根据 Reals 对其进行转换，解决它（Reals 有一个决策程序），然后通过说 Floor(solution) = solution 添加额外的限制，即结果是一个整数。因此，通过这个论点，您可以看到对此类函数建模将超出 SMT 求解器的能力。

有关详细信息，请参阅此答案：

话虽如此，这不意味着您不能在 Z3 中对此进行编码。这只是意味着它或多或少会毫无用处。以下是我的处理方式：

from z3 import *

s = Solver()

Floor = Function('Floor',RealSort(),IntSort())

r = Real('R')
f = Int('f')
s.add(ForAll([r, f], Implies(And(f <= r, r < f+1), Floor(r) == f)))

现在，如果我这样做：

s.add(Not(Floor(0.5) == 0))
print(s.check())

你会得到 unsat，这是正确的。如果您这样做：

s.add(Not(Floor(0.5) == 1))
print(s.check())

您会看到 z3 会一直循环下去。为了使它有用，您还需要以下内容：

test = Real('test')
s.add(test == 2.4)
result = Int('result')
s.add(Floor(test) == result)
print(s.check())

但是，您会再次看到 z3 一直循环下去。

所以，底线是：是的，您可以对此类构造进行建模，z3 将正确回答最简单的查询。但是对于任何有趣的事情，它都会永远循环下去。（基本上，只要你期望 sat 和大多数 unsat 场景，除非它们可以不断折叠，我希望 z3 简单地循环。）这是有充分理由的，正如我所提到的：这样的理论是不可判定的，并且远远超出了 SMT 求解器可以做的范围。

如果您对此类函数建模感兴趣，最好的办法是使用更传统的定理证明器，例如 Isabelle、Coq、ACL2、HOL、HOL-Light 等。它们更适合处理这类问题。此外，请阅读，因为它深入介绍了如何使用非线性实数算法对此类函数进行建模的其他一些细节。

Z3 中的地板和天花板功能实现

Floor and Ceiling Function implementation in Z3

z3

smt

z3py

floor

ceil