Usando la lógica mónada en Haskell

logic backtracking

Question

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 ]

Answer 1

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

Answer 2

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