Usando la Lógica Monad en Haskell

Question

Recientemente, implementé una ingenua DPLL Sat Solver en Haskell, adaptada de John Harrison's Handbook of Practical Logic and Automated Reasoning.

DPLL es una variedad de búsqueda de retroceso, por lo que quiero experimentar con el uso del Logic monad desde Oleg Kiselyov et al. Sin embargo, realmente no entiendo lo que necesito cambiar.

Aquí está el código que tengo.

• ¿Qué código debo cambiar para usar la mónada de Logic?
• Bonificación: ¿Hay algún beneficio concreto en el rendimiento al usar la mónada Logic?

---

{-# LANGUAGE MonadComprehensions #-} 
module DPLL where 
import Prelude hiding (foldr) 
import Control.Monad (join,mplus,mzero,guard,msum) 
import Data.Set.Monad (Set, (\\), member, partition, toList, foldr) 
import Data.Maybe (listToMaybe) 

-- "Literal" propositions are either true or false 
data Lit p = T p | F p deriving (Show,Ord,Eq) 

neg :: Lit p -> Lit p 
neg (T p) = F p 
neg (F p) = T p 

-- We model DPLL like a sequent calculus 
-- LHS: a set of assumptions/partial model (set of literals) 
-- RHS: a set of goals 
data Sequent p = (Set (Lit p)) :|-: Set (Set (Lit p)) deriving Show 

{- --------------------------- Goal Reduction Rules -------------------------- -} 
{- "Unit Propogation" takes literal x and A :|-: B to A,x :|-: B', 
- where B' has no clauses with x, 
- and all instances of -x are deleted -} 
unitP :: Ord p => Lit p -> Sequent p -> Sequent p 
unitP x (assms :|-: clauses) = (assms' :|-: clauses') 
    where 
    assms' = (return x) `mplus` assms 
    clauses_ = [ c | c <- clauses, not (x `member` c) ] 
    clauses' = [ [ u | u <- c, u /= neg x] | c <- clauses_ ] 

{- Find literals that only occur positively or negatively 
- and perform unit propogation on these -} 
pureRule :: Ord p => Sequent p -> Maybe (Sequent p) 
pureRule sequent@(_ :|-: clauses) = 
    let 
    sign (T _) = True 
    sign (F _) = False 
    -- Partition the positive and negative formulae 
    (positive,negative) = partition sign (join clauses) 
    -- Compute the literals that are purely positive/negative 
    purePositive = positive \\ (fmap neg negative) 
    pureNegative = negative \\ (fmap neg positive) 
    pure = purePositive `mplus` pureNegative 
    -- Unit Propagate the pure literals 
    sequent' = foldr unitP sequent pure 
    in if (pure /= mzero) then Just sequent' 
    else Nothing 

{- Add any singleton clauses to the assumptions 
- and simplify the clauses -} 
oneRule :: Ord p => Sequent p -> Maybe (Sequent p) 
oneRule sequent@(_ :|-: clauses) = 
    do 
    -- Extract literals that occur alone and choose one 
    let singletons = join [ c | c <- clauses, isSingle c ] 
    x <- (listToMaybe . toList) singletons 
    -- Return the new simplified problem 
    return $ unitP x sequent 
    where 
    isSingle c = case (toList c) of { [a] -> True ; _ -> False } 

{- ------------------------------ DPLL Algorithm ----------------------------- -} 
dpll :: Ord p => Set (Set (Lit p)) -> Maybe (Set (Lit p)) 
dpll goalClauses = dpll' $ mzero :|-: goalClauses 
    where 
    dpll' sequent@(assms :|-: clauses) = do 
     -- Fail early if falsum is a subgoal 
     guard $ not (mzero `member` clauses) 
     case (toList . join) $ clauses of 
     -- Return the assumptions if there are no subgoals left 
     [] -> return assms 
     -- Otherwise try various tactics for resolving goals 
     x:_ -> dpll' =<< msum [ pureRule sequent 
           , oneRule sequent 
           , return $ unitP x sequent 
           , return $ unitP (neg x) sequent ] 

Answer 1

Ok, cambiar su código para utilizar Logic resultó ser completamente trivial. Revisé todo y reescribí todo para usar las funciones simples Set en lugar de la mónada Set, porque realmente no estás usando Set monádicamente de una manera uniforme, y ciertamente no para la lógica de retroceso. Las mónadas de comprensión también fueron escritas más claramente como mapas y filtros y cosas por el estilo. No era necesario que esto sucediera, pero sí me ayudó a ordenar lo que estaba sucediendo, y ciertamente dejó en claro que la única mónada real, que se usaba para retroceder, era solo Maybe.

En cualquier caso, sólo puede generalizar la firma tipo de pureRule, oneRule y dpll para operar sobre no sólo Maybe, pero cualquier m con la restricción MonadPlus m =>.

Luego, en pureRule, sus tipos no coincidirá debido a que la construcción de Maybe s explícita, así que ve y cambia un poco:

in if (pure /= mzero) then Just sequent' 
    else Nothing 

convierte

in if (not $ S.null pure) then return sequent' else mzero 

Y en oneRule, de manera similar cambie el uso de listToMaybe a una coincidencia explícita para

x <- (listToMaybe . toList) singletons 

convierte

case singletons of 
    x:_ -> return $ unitP x sequent -- Return the new simplified problem 
    [] -> mzero 

Y, fuera del tipo de cambio de la firma, dpll necesidades no hay cambios en absoluto!

Ahora, el código funciona sobre tantoMaybe y Logic!

para ejecutar el código Logic, se puede utilizar una función como la siguiente:

dpllLogic s = observe $ dpll' s 

Puede utilizar observeAll o similar para ver más resultados.no

{-# LANGUAGE MonadComprehensions #-} 
module DPLL where 
import Prelude hiding (foldr) 
import Control.Monad (join,mplus,mzero,guard,msum) 
import Data.Set (Set, (\\), member, partition, toList, foldr) 
import qualified Data.Set as S 
import Data.Maybe (listToMaybe) 
import Control.Monad.Logic 

-- "Literal" propositions are either true or false 
data Lit p = T p | F p deriving (Show,Ord,Eq) 

neg :: Lit p -> Lit p 
neg (T p) = F p 
neg (F p) = T p 

-- We model DPLL like a sequent calculus 
-- LHS: a set of assumptions/partial model (set of literals) 
-- RHS: a set of goals 
data Sequent p = (Set (Lit p)) :|-: Set (Set (Lit p)) --deriving Show 

{- --------------------------- Goal Reduction Rules -------------------------- -} 
{- "Unit Propogation" takes literal x and A :|-: B to A,x :|-: B', 
- where B' has no clauses with x, 
- and all instances of -x are deleted -} 
unitP :: Ord p => Lit p -> Sequent p -> Sequent p 
unitP x (assms :|-: clauses) = (assms' :|-: clauses') 
    where 
    assms' = S.insert x assms 
    clauses_ = S.filter (not . (x `member`)) clauses 
    clauses' = S.map (S.filter (/= neg x)) clauses_ 

{- Find literals that only occur positively or negatively 
- and perform unit propogation on these -} 
pureRule sequent@(_ :|-: clauses) = 
    let 
    sign (T _) = True 
    sign (F _) = False 
    -- Partition the positive and negative formulae 
    (positive,negative) = partition sign (S.unions . S.toList $ clauses) 
    -- Compute the literals that are purely positive/negative 
    purePositive = positive \\ (S.map neg negative) 
    pureNegative = negative \\ (S.map neg positive) 
    pure = purePositive `S.union` pureNegative 
    -- Unit Propagate the pure literals 
    sequent' = foldr unitP sequent pure 
    in if (not $ S.null pure) then return sequent' 
    else mzero 

{- Add any singleton clauses to the assumptions 
- and simplify the clauses -} 
oneRule sequent@(_ :|-: clauses) = 
    do 
    -- Extract literals that occur alone and choose one 
    let singletons = concatMap toList . filter isSingle $ S.toList clauses 
    case singletons of 
    x:_ -> return $ unitP x sequent -- Return the new simplified problem 
    [] -> mzero 
    where 
    isSingle c = case (toList c) of { [a] -> True ; _ -> False } 

{- ------------------------------ DPLL Algorithm ----------------------------- -} 
dpll goalClauses = dpll' $ S.empty :|-: goalClauses 
    where 
    dpll' sequent@(assms :|-: clauses) = do 
     -- Fail early if falsum is a subgoal 
     guard $ not (S.empty `member` clauses) 
     case concatMap S.toList $ S.toList clauses of 
     -- Return the assumptions if there are no subgoals left 
     [] -> return assms 
     -- Otherwise try various tactics for resolving goals 
     x:_ -> dpll' =<< msum [ pureRule sequent 
           , oneRule sequent 
           , return $ unitP x sequent 
           , return $ unitP (neg x) sequent ] 

dpllLogic s = observe $ dpll s 

Answer 2

algún beneficio concreto para el rendimiento mediante la mónada Lógica:

Para referencia, aquí está el código completo de trabajo?

TL; DR: No es que me encuentro; parece que Maybe supera a Logic ya que tiene menos sobrecarga.

---

I decidió aplicar una referencia sencilla para comprobar el rendimiento de Logic frente Maybe. En mi prueba, construyo al azar 5000 CNF con n cláusulas, cada cláusula contiene tres literales. El rendimiento se evalúa ya que el número de cláusulas n es variado.

En mi código, he modificado dpllLogic de la siguiente manera:

dpllLogic s = listToMaybe $ observeMany 1 $ dpll s 

También he probado la modificación dpll con disyunción justo, así:

dpll goalClauses = dpll' $ S.empty :|-: goalClauses 
    where 
    dpll' sequent@(assms :|-: clauses) = do 
     -- Fail early if falsum is a subgoal 
     guard $ not (S.empty `member` clauses) 
     case concatMap S.toList $ S.toList clauses of 
     -- Return the assumptions if there are no subgoals left 
     [] -> return assms 
     -- Otherwise try various tactics for resolving goals 
     x:_ -> msum [ pureRule sequent 
        , oneRule sequent 
        , return $ unitP x sequent 
        , return $ unitP (neg x) sequent ] 
       >>- dpll' 

entonces probaron el uso de Maybe, Logic y Logic con una disyunción justa.

Éstos son los resultados de referencia para estas pruebas:

Como podemos ver, Logic con o sin disyunción justo en este caso no hay diferencia. El dpll resolver utilizando la mónada Maybe parece ejecutarse en tiempo lineal en n, mientras que el uso de la mónada Logic genera una sobrecarga adicional. Parece que la sobrecarga incurrió en mesetas apagadas.

Aquí está el archivo Main.hs utilizado para generar estas pruebas. Alguien que desee reproducir estos puntos de referencia podría querer revisar Haskell's notes on profiling:

module Main where 
import DPLL 
import System.Environment (getArgs) 
import System.Random 
import Control.Monad (replicateM) 
import Data.Set (fromList) 

randLit = do let clauses = [ T p | p <- ['a'..'f'] ] 
         ++ [ F p | p <- ['a'..'f'] ] 
      r <- randomRIO (0, (length clauses) - 1) 
      return $ clauses !! r 

randClause n = fmap fromList $ replicateM n $ fmap fromList $ replicateM 3 randLit 

main = do args <- getArgs 
      let n = read (args !! 0) :: Int 
      clauses <- replicateM 5000 $ randClause n 
      -- To use the Maybe monad 
      --let satisfiable = filter (/= Nothing) $ map dpll clauses 
      let satisfiable = filter (/= Nothing) $ map dpllLogic clauses 
      putStrLn $ (show $ length satisfiable) ++ " satisfiable out of " 
        ++ (show $ length clauses)