Pourquoi ce code SBV s'arrête-t-il avant d'avoir atteint la limite que j'ai fixée?

Question

J'ai ce théorème (je ne sais pas si c'est le bon mot), et je veux obtenir toutes les solutions.

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]] 

Cette tente de résoudre le problème:

Il y a des paires infinies d'entiers (m, n) tel que m^3 = n^2 et m + n est un carré parfait. Quelle est la paire avec le plus grand m moins de 1000?

Je sais la réponse réelle, juste par le forçage brutal, mais je veux faire avec SBV.

Cependant, quand j'exécuter le code, il ne donne que les valeurs suivantes (sous la forme [m, n, a]): [[9,27,6], [64,512,24], []]

Cependant, il existe plusieurs autres solutions avec une valeur m inférieure à 1000 qui ne sont pas incluses.

Answer 1

Il est toujours bon de donner un programme complet:

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

Quand je cours, je reçois:

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 

note finale Unknown.

Essentiellement, SBV interrogé Z3 et eu 6 solutions; quand SBV a demandé le 7ème, Z3 a dit "je ne sais pas s'il y a une autre solution." Avec l'arithmétique non linéaire, ce comportement est attendu.

Pour répondre à la question initiale (c.-à-trouver le max m), j'ai changé la contrainte à lire:

constrain $ m .== limit 

et couplé avec le "conducteur:" suivant

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

Après courant environ 50 minutes sur ma machine, Z3 produit:

(576,13824,-120) 

Ainsi, clairement le 01 L'approche basée surfait en sorte que Z3 abandonne plus tôt que ce qu'elle peut réellement accomplir si nous fixons m et que nous nous répétons. Avec un problème non linéaire, s'attendre à quelque chose de plus rapide/mieux serait trop demander à un solveur SMT généraliste.