爲什麼此SBV代碼在達到我設定的限制之前停止？

我有這個定理（不知道這是否正確的話），我想獲得所有的解決方案。爲什麼此SBV代碼在達到我設定的限制之前停止？

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），使得立方公尺= N^2，m + n爲一個完全平方。什麼是小於1000的最大m值？

我知道實際的答案，只是通過暴力強制，但我想用SBV做。

但是，當我運行代碼時，它只給出以下值（形式爲[m，n，a]）： [[9,27,6]，[64,512,24]，[]]

但是，還有其他一些m值小於1000的解決方案未包括在內。

來源

2015-12-08 Kytuzian

@ ThomasM.DuBuisson另外，如果我將限制更改爲4097，我得到的解決方案是m爲225和576，但如果它是4096，它不會顯示。 – Kytuzian

這是一件好事，給一個完整的程序：

{-# 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)

所以，顯然01如果我們修復了m並迭代我們自己，基於方法正在導致Z3放棄的方式早於它實際可以實現的方式。對於一個非線性的問題，期望任何更快/更好的東西都不足以問一個通用SMT解決方案..

來源

2015-12-08 21:54:41

爲什麼此SBV代碼在達到我設定的限制之前停止？

回答

相關問題