用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为真的output，而且是为了找到所有可能的inputs？

Answer 1

SMT求解器非常擅长于解决这类约束，有很多可供选择。有关概述，请参见https://smtlib.cs.uiowa.edu。

一个实现是微软的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的一种解决方案

对于您的特定问题，下面是如何使用z3在Haskell中使用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)

同样，当运行时，这会不断地吐出解决方案。