Почему этот код 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]] 

Это пытается решить эту проблему:

Есть бесконечные пары целых чисел (т, п), что т^3 = п^2 и т + п является квадратом. Какая пара с наибольшим м менее 1000?

Я знаю фактический ответ, только через грубое форсирование, но я хочу сделать с SBV.

Однако, когда я бегу код это дает только следующие значения (в виде [т, п, а]): [[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.

По существу, ЗСО опрошено 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 общего назначения.