为什么这个SBV代码在达到我设定的限制之前就停止了？

Question

我有这个定理(不确定这是否是正确的词),我想得到所有的解决方案.

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的解决方案,不包括在内.

Answer 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基于这种方法的原因是,如果我们自己修复m和迭代,Z3会比实际实现的方式更早地放弃.对于非线性问题,期望任何更快/更好的东西对于通用SMT求解器来说太过分了.