为什么此 SBV 代码在达到我设置的限制之前停止？答案

【问题标题】：Why does this SBV code stop before hitting the limit I set?为什么此 SBV 代码在达到我设置的限制之前停止？
【发布时间】：2015-12-08 18:01:15
【问题描述】：

我有这个定理（不确定这是否是正确的词），我想得到所有的解决方案。

pairCube limit = do
    m <- natural exists "m"
    n <- natural exists "n"
    a <- natural exists "a"
    constrain $ m^3 .== n^2
    constrain $ m .< limit
    return $ m + n .== a^2

res <- allSat (pairCube 1000)

-- Run from ghci
extractModels res :: [[Integer]]

这是试图解决问题：

有无穷多对整数 (m, n) 使得 m^3 = n^2 并且 m + n 是一个完美的正方形。最大 m 小于 1000 的对是什么？

我知道实际答案，只是通过暴力破解，但我想使用 SBV。

但是，当我运行代码时，它只给出以下值（形式为 [m, n, a]）： [[9,27,6],[64,512,24],[]]

但是，还有其他几个 m 值小于 1000 的解决方案不包括在内。

【问题讨论】：

@ThomasM.DuBuisson 另外，如果我将限制更改为 4097，我会得到 m 为 225 和 576 的解决方案，但如果是 4096，则不会显示。

标签： haskell symbolic-math proof sbv

【解决方案1】：

给出一个完整的程序总是好的：

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

pairCube :: SInteger -> Symbolic SBool
pairCube limit = do
        (m :: SInteger) <- exists "m"
        (n :: SInteger) <- exists "n"
        (a :: SInteger) <- exists "a"
        constrain $ m^(3::Integer) .== n^(2::Integer)
        constrain $ m .< limit
        return $ m + n .== a^(2::Integer)

main :: IO ()
main = print =<< allSat (pairCube 1000)

当我运行它时，我得到：

Main> main
Solution #1:
  m = 0 :: Integer
  n = 0 :: Integer
  a = 0 :: Integer
Solution #2:
  m =  9 :: Integer
  n = 27 :: Integer
  a = -6 :: Integer
Solution #3:
  m =  1 :: Integer
  n = -1 :: Integer
  a =  0 :: Integer
Solution #4:
  m =  9 :: Integer
  n = 27 :: Integer
  a =  6 :: Integer
Solution #5:
  m =  64 :: Integer
  n = 512 :: Integer
  a = -24 :: Integer
Solution #6:
  m =  64 :: Integer
  n = 512 :: Integer
  a =  24 :: Integer
Unknown

注意最后的Unknown.

本质上，SBV查询了Z3，得到了6个解；当SBV问7号时，Z3说“不知道有没有其他办法”。使用非线性算术，这种行为是预期的。

为了回答原始问题（即找到最大值m），我将约束更改为：

constrain $ m .== limit

并将其与以下“驱动程序”耦合：

main :: IO ()
main = loop 1000
  where loop (-1) = putStrLn "Can't find the largest m!"
        loop m    = do putStrLn $ "Trying: " ++ show m
                       mbModel <- extractModel `fmap` sat (pairCube m)
                       case mbModel of
                         Nothing -> loop (m-1)
                         Just r  -> print (r :: (Integer, Integer, Integer))

在我的机器上运行了大约 50 分钟后，Z3 产生了：

(576,13824,-120)

因此，显然基于allSat 的方法导致Z3 放弃的方式比我们修复m 并迭代自己所能实际实现的要早。对于非线性问题，对于通用 SMT 求解器而言，期望任何更快/更好的东西都太过分了..

【讨论】：