z3 - 是否可以解决给定输入和输出的函数运算？

Question

我有一个函数，它接受 2 个整数作为输入，并输出一个整数。

我有一组输入及其已知输出。

是否可以弄清楚该函数对输入应用了哪些操作以得出输出？

我不知道如何开始使用 z3 来模拟这样的问题。任何帮助将不胜感激。

示例数据:

f(1, 1) = 1
f(3, 7) = 28
f(3, 2) = 3
f(4, 6) = 56
f(10, 3) = 55
f(x, y) = f(y, x)

Answer 1

是的，你可以。但无论如何，结果都不会有趣，除非您至少规定了 f 的一些结构。

最明显的方法是将 f 声明为非解释函数，然后查看为其构建的模型。但这将是 f 的基本定义；也就是说，它会以最无趣的方式满足你的公理。您可以这样写:

from z3 import *
f = Function('f', IntSort(), IntSort(), IntSort())

s = Solver()
s.add(f( 1, 1) ==  1)
s.add(f( 3, 7) == 28)
s.add(f( 3, 2) ==  3)
s.add(f( 4, 6) == 56)
s.add(f(10, 3) == 55)
x, y = Ints('x y')
s.add(ForAll([x, y], f(x, y) == f(y, x)))

print(s.check())
print(s.model())

这是 z3 打印的内容:

sat
[f = [else ->
      If(And(Not(Var(0) == 6),
             Not(Var(0) == 4),
             Not(Var(0) == 10),
             Var(0) == 3,
             Not(Var(1) == 6),
             Not(Var(1) == 4),
             Var(1) == 10),
         55,
         If(And(Var(0) == 6, Not(Var(1) == 6), Var(1) == 4),
            56,
            If(And(Not(Var(0) == 6),
                   Not(Var(0) == 4),
                   Not(Var(0) == 10),
                   Not(Var(0) == 3),
                   Not(Var(0) == 1),
                   Var(0) == 2,
                   Not(Var(1) == 6),
                   Not(Var(1) == 4),
                   Not(Var(1) == 10),
                   Var(1) == 3),
               3,
               If(And(Not(Var(0) == 6),
                      Not(Var(0) == 4),
                      Not(Var(0) == 10),
                      Not(Var(0) == 3),
                      Not(Var(0) == 1),
                      Not(Var(0) == 2),
                      Not(Var(1) == 6),
                      Not(Var(1) == 4),
                      Not(Var(1) == 10),
                      Var(1) == 3),
                  28,
                  If(And(Not(Var(0) == 6),
                         Not(Var(0) == 4),
                         Var(0) == 10,
                         Not(Var(1) == 6),
                         Not(Var(1) == 4),
                         Not(Var(1) == 10),
                         Var(1) == 3),
                     55,
                     If(And(Not(Var(0) == 6),
                            Var(0) == 4,
                            Var(1) == 6),
                        56,
                        If(And(Not(Var(0) == 6),
                               Not(Var(0) == 4),
                               Not(Var(0) == 10),
                               Var(0) == 3,
                               Not(Var(1) == 6),
                               Not(Var(1) == 4),
                               Not(Var(1) == 10),
                               Not(Var(1) == 3),
                               Not(Var(1) == 1),
                               Var(1) == 2),
                           3,
                           If(And(Not(Var(0) == 6),
                                  Not(Var(0) == 4),
                                  Not(Var(0) == 10),
                                  Var(0) == 3,
                                  Not(Var(1) == 6),
                                  Not(Var(1) == 4),
                                  Not(Var(1) == 10),
                                  Not(Var(1) == 3),
                                  Not(Var(1) == 1),
                                  Not(Var(1) == 2)),
                              28,
                              If(And(Not(Var(0) == 6),
                                     Not(Var(0) == 4),
                                     Not(Var(0) == 10),
                                     Not(Var(0) == 3),
                                     Var(0) == 1,
                                     Not(Var(1) == 6),
                                     Not(Var(1) == 4),
                                     Not(Var(1) == 10),
                                     Not(Var(1) == 3),
                                     Var(1) == 1),
                                 1,
                                 12)))))))))]]

读取此输出的方法是将 x 替换为 Var(0)，将 y 替换为 Var(1)，并将嵌套的 if-then-elses 作为定义的定义子句。

虽然我没有逐行检查输出，但我确信它是正确的；从某种意义上说，它完全满足您的要求。但我能听到你说“这不是我真正想要的!”事实上，这并不是您想要看到的满足要求的通用/最小函数。按照 SMT 求解器的工作方式，除非您描述 z3 需要填充的一些骨架，否则您永远不会得到最小答案。

请注意，这是一个活跃的研究领域:如何使用(半)自动定理证明器、SMT 求解器等为我们“编写”代码。一般区域称为 SyGus(语法引导合成)。如果您想了解更多信息，请从 https://sygus.org 开始，其中包含问题的一般描述并阅读本文:https://sygus.org/assets/pdf/FMCAD'13_SyGuS.pdf