Utilizzo della logica Monad in Haskell

Question

Recentemente, ho implementato un ingenuo DPLL Sat Solver in Haskell, adattato da John Harrison Handbook of Practical Logic and Automated Reasoning.

DPLL è una varietà di ricerca di backtrack, quindi voglio sperimentare l'utilizzo di Logic monad da Oleg Kiselyov et al. Non capisco davvero cosa devo cambiare, comunque.

Ecco il codice che ho.

• Quale codice devo modificare per utilizzare la logica?
• Bonus: C'è un vantaggio prestazionale concreto nell'utilizzo della monade Logica?

---

{-# 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, cambiare il codice per utilizzare Logic si è rivelata del tutto banale. Ho esaminato e riscritto tutto per utilizzare le semplici funzioni Set anziché la monade Set, perché non si utilizza realmente lo Set in modo monodico in modo uniforme, e certamente non per la logica del backtracking. Le comprensioni di monade erano anche più chiaramente scritte come mappe e filtri e simili. Non era necessario che ciò accadesse, ma mi aiutò a capire cosa stava succedendo, e certamente rese evidente che l'unica vera monade rimanente, usata per il backtracking, era solo Maybe.

In ogni caso, si può semplicemente generalizzare la firma tipo di pureRule, oneRule, e dpll per funzionare su non solo Maybe, ma qualsiasi m con il vincolo MonadPlus m =>.

Poi, nel pureRule, i tipi di non corrisponderanno perché si costruisce Maybe s in modo esplicito, in modo da andare a cambiare un po ':

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

diventa

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

E in oneRule, allo stesso modo modificare l'utilizzo di listToMaybe in una corrispondenza esplicita in modo

x <- (listToMaybe . toList) singletons 

diventa

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

E, al di fuori del cambiamento firma tipo, dpll non ha bisogno di modifiche a tutti!

Ora, il codice gestisce oltre siaMaybeeLogic!

Per eseguire il codice Logic, è possibile utilizzare una funzione come la seguente:

dpllLogic s = observe $ dpll' s 

È possibile utilizzare observeAll o simili per vedere più risultati.ci

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

è alcun beneficio concreto per le prestazioni utilizzando la monade Logic:

Per riferimento, ecco il codice di lavoro completo?

TL; DR: Non che io possa trovare; sembra che Maybe superi le prestazioni di Logic in quanto ha un sovraccarico minore.

---

ho deciso di implementare un semplice punto di riferimento per controllare le prestazioni di Logic rispetto Maybe. Nel mio test, costruisco casualmente 5000 CNF con clausole n, ciascuna clausola contenente tre valori letterali. Le prestazioni vengono valutate in base al numero di clausole n variate.

Nel mio codice, ho modificato dpllLogic come segue:

dpllLogic s = listToMaybe $ observeMany 1 $ dpll s 

ho testato anche la modifica dpll con fiera disgiunzione, in questo modo:

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' 

ho poi testato l'utilizzo Maybe, Logic e Logic con una corretta disgiunzione.

Ecco i risultati dei benchmark per questo test:

Come possiamo vedere, Logic con o senza giusta disgiunzione in questo caso non fa differenza. La risoluzione dpll utilizzando il monad Maybe sembra essere eseguita in tempo lineare in n, mentre l'utilizzo della monade Logic comporta un ulteriore sovraccarico. Sembra che l'overhead abbia subito degli altipiani.

Questo è il file Main.hs utilizzato per generare questi test. Qualcuno che desiderano riprodurre questi parametri di riferimento potrebbe desiderare di rivedere 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)