haskell logic backtracking

Usando la lógica mónada en Haskell



logic backtracking (2)

¿Hay algún beneficio concreto en el rendimiento al usar la mónada Logic?

TL; DR : No es que yo pueda encontrar; parece que Maybe supera a Logic ya que tiene menos gastos generales.

Decidí implementar un punto de referencia simple para verificar el rendimiento de Logic versus Maybe . En mi prueba, construyo al azar 5000 CNF con n cláusulas, cada cláusula contenía tres literales. El rendimiento se evalúa a medida que el número de cláusulas n varía.

En mi código, modifiqué dpllLogic siguiente manera:

dpllLogic s = listToMaybe $ observeMany 1 $ dpll s

También probé la modificación de dpll con disyunción justa , 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''

Luego probé el uso de Maybe , Logic y Logic con una separación justa.

Aquí están los resultados de referencia para esta prueba:

Como podemos ver, la Logic con o sin disyunción justa en este caso no hace ninguna diferencia. La solución dpll utilizando la mónada Maybe parece que se ejecuta en tiempo lineal en n , mientras que la mónada Logic genera una sobrecarga adicional. Parece que los gastos generales incurridos mesetas fuera.

Aquí está el archivo Main.hs utilizado para generar estas pruebas. Alguien que desee reproducir estos puntos de referencia podría revisar las notas de Haskell sobre el perfil :

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)

Recientemente, implementé un ingenuo DPLL Sat Solver en Haskell , adaptado del Manual de lógica práctica y razonamiento automatizado de John Harrison.

DPLL es una variedad de búsqueda de retroceso, por lo que quiero experimentar utilizando la mónada Logic de Oleg Kiselyov et al . Sin embargo, realmente no entiendo lo que necesito cambiar.

Aquí está el código que tengo.

  • ¿Qué código necesito cambiar para usar la mónada 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 ]


Ok, cambiar tu código para usar Logic resultó ser completamente trivial. Revisé y reescribí todo para usar las funciones de Set simples en lugar de la mónada de Set , porque en realidad no lo estamos usando de manera uniforme, y ciertamente no para la lógica de retroceso. Las comprensiones de la mónada también se escribieron más claramente como mapas, filtros y similares. Esto no tenía que suceder, pero sí me ayudó a resolver lo que estaba sucediendo, y ciertamente hizo evidente que la única mónada real que se usaba para retroceder, era simplemente Maybe .

En cualquier caso, puede simplemente generalizar la firma de tipo de pureRule , oneRule y dpll para operar no solo en Maybe , sino en cualquier m con la restricción MonadPlus m => .

Luego, en pureRule , sus tipos no coincidirán porque usted construye Maybe s explícitamente, así que vaya y cámbielo un poco:

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

se convierte en

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

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

x <- (listToMaybe . toList) singletons

se convierte en

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

Y, fuera del tipo de cambio de firma, ¡ dpll no necesita ningún cambio!

¡Ahora, su código opera sobre Maybe y Logic !

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

dpllLogic s = observe $ dpll'' s

Puedes usar observeAll o similares para ver más resultados.

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

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