Почему этот код 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 основанный подход заставляет Z3 сдаться намного раньше, чем он может реально достичь, если мы исправим m и повторить себя. В случае нелинейной задачи ожидать чего-либо быстрее / лучше было бы слишком сложно для универсального SMT-решателя.