Jalonso: Página creada con « -- SAT_DP_Clique.hs -- Comparación de algoritmos de satisfacibilidad. -- José A. Alonso Jiménez -- Sevilla, 6 de febrero de 2020 -- -------------…»

2020-02-06T10:27:06Z

Página creada con «<source lang="haskell"> -- SAT_DP_Clique.hs -- Comparación de algoritmos de satisfacibilidad. -- José A. Alonso Jiménez -- Sevilla, 6 de febrero de 2020 -- -------------…»

Página nueva

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

Comparaciones de algoritmos de SAT - Historial de revisiones

Jalonso: Página creada con « -- SAT_DP_Clique.hs -- Comparación de algoritmos de satisfacibilidad. -- José A. Alonso Jiménez -- Sevilla, 6 de febrero de 2020 -- -------------…»