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