使用 ATS 求解所有有效输入

Question

假设您有一个纯表达式系统，例如，

(bi0, bi1, bi2, ai0, ai1, ai2) := inputs
b0 := bi0 && bi1
a1 := b0 ? ai0 : cbrt(ai0)
a2 := bi2 ? a1 : ai1
output := a2 > ai2

# prove:
output == True

可以对自动定理证明器进行编程吗？不仅要查找 output 为 true 的一些 input，还要查找所有 output可能的输入对于哪些情况是正确的？

Answer 1

SMT 求解器非常擅长解决此类约束，并且有很多可供选择。请参阅 https://smtlib.cs.uiowa.edu 了解概述。

一种实现是 Microsoft 的 z3，它可以轻松处理您提出的查询： https://github.com/Z3Prover /z3

SMT 求解器可以使用所谓的 SMTLib 语法进行编程（请参阅上面的第一个链接），或者它们提供多种语言的 API 供您进行编程；包括 C/C++/Java/Python/Haskell 等。此外，现在大多数定理证明器（包括 Isabelle/HOL）都采用了在幕后使用这些证明器的策略；如此多的集成是可能的。

正如我提到的，z3 可以用多种语言进行编程，值得回顾的一篇很好的论文是 https:/ /theory.stanford.edu/~nikolaj/programmingz3.html，它使用 Python 来执行此操作。

在 Haskell 中使用 Z3 的解决方案

对于您的特定问题，以下是如何在 Haskell 中使用 z3 解决它，使用 SBV 层（http://leventerkok.github.io/sbv/)：

import Data.SBV

problem :: IO AllSatResult
problem = allSatWith z3{allSatPrintAlong = True} $ do
            [bi0, bi1, bi2] <- sBools ["bi0", "bi1", "bi2"]
            [ai0, ai1, ai2] <- sReals ["ai0", "ai1", "ai2"]

            cbrt_ai0 <- sReal "cbrt_ai0"
            let cube x = x * x * x
            constrain $ cube cbrt_ai0 .== ai0

            let b0 = bi0 .&& bi1
                a1 = ite b0  ai0 cbrt_ai0
                a2 = ite bi2 a1  ai1

            pure $ a2 .> ai2

当我运行这个时，我得到：

*Main> problem
Solution #1:
  bi0      = False :: Bool
  bi1      = False :: Bool
  bi2      = False :: Bool
  ai0      = 0.125 :: Real
  ai1      =  -0.5 :: Real
  ai2      =  -2.0 :: Real
  cbrt_ai0 =   0.5 :: Real
Solution #2:
  bi0      = True :: Bool
  bi1      = True :: Bool
  bi2      = True :: Bool
  ai0      =  0.0 :: Real
  ai1      =  0.0 :: Real
  ai2      = -1.0 :: Real
  cbrt_ai0 =  0.0 :: Real
Solution #3:
  bi0      =  True :: Bool
  bi1      = False :: Bool
  bi2      =  True :: Bool
  ai0      =   0.0 :: Real
  ai1      =   0.0 :: Real
  ai2      =  -1.0 :: Real
  cbrt_ai0 =   0.0 :: Real

...[many more lines deleted...]

我中断了输出，因为似乎有很多作业（通过查看问题的结构可能是无限的）。

在 Python 中使用 Z3 的解决方案

另一种流行的选择是使用 Python 进行编程。在这种情况下，代码比 Haskell 更冗长一些，有一些样板来获取所有解决方案和其他 Python 陷阱，但在其他方面遵循类似的路径：

from z3 import *

s = Solver()

bi0, bi1, bi2 = Bools('bi0 bi1 bi2')
ai0, ai1, ai2 = Reals('ai0 ai1 ai2')

cbrt_ai0 = Real('cbrt_ai0')

def cube(x):
    return x*x*x

s.add(cube(cbrt_ai0) == ai0)

b0 = And(bi0, bi1)
a1 = If(b0, ai0, cbrt_ai0)
a2 = If(bi2, a1, ai1)

s.add(a2  > ai2)

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()...
    yield from all_smt_rec(list(initial_terms))

for model in all_smt(s, [ai0, ai1, ai2, bi0, bi1, bi2]):
    print(model)

再次，当运行时不断地吐出解决方案。