Ver el código de «Comparaciones de algoritmos de SAT»

<source lang="haskell">
-- SAT_DP_Clique.hs
-- Comparación de algoritmos de satisfacibilidad.
-- José A. Alonso Jiménez
-- Sevilla, 6 de febrero de 2020
-- ---------------------------------------------------------------------

import SAT
import SAT_DavisPutnam
import SAT_Clique

ejemploSAT, ejemploUNSAT :: Int -> FNC
ejemploSAT   k = [[-n,n+1] | n <- [1..k]]
ejemploUNSAT k = [[-n,n+1] | n <- [1..k]] ++ [[1],[-(k+1)]]

-- Comparaciones:
--    λ> esSatisfacible (ejemploSAT 12) 
--    True
--    (0.01 secs, 115,664 bytes)
--    λ> esSatisfaciblePorDP (ejemploSAT 12) 
--    True
--    (0.01 secs, 169,240 bytes)
--    λ> esSatisfaciblePorClique (ejemploSAT 12) 
--    True
--    (16.08 secs, 4,709,712,560 bytes)
--    
--    λ> esSatisfacible (ejemploSAT 2000) 
--    True
--    (0.02 secs, 2,358,672 bytes)
--    λ> esSatisfaciblePorDP (ejemploSAT 2000) 
--    True
--    (1.16 secs, 997,415,248 bytes)
--    
--    λ> esSatisfacible (ejemploUNSAT 9)
--    False
--    (0.03 secs, 3,880,952 bytes)
--    λ> esSatisfaciblePorDP (ejemploUNSAT 9)
--    False
--    (0.01 secs, 153,144 bytes)
--    λ> esSatisfaciblePorClique (ejemploUNSAT 9)
--    False
--    (5.36 secs, 1,621,747,704 bytes)
--    
--    λ> esSatisfacible (ejemploUNSAT 20)
--    False
--    (9.40 secs, 7,734,421,008 bytes)
--    λ> esSatisfaciblePorDP (ejemploUNSAT 20)
--    False
--    (0.01 secs, 271,552 bytes)
</source>