在Haskell中使用Logic Monad

Question

最近,我在Haskell中实现了一个天真的DPLL Sat解算器,改编自John Harrison的实用逻辑和自动推理手册.

DPLL是各种回溯搜索的,所以想要使用所述实验逻辑单子从奥列格Kiselyov等.但是,我真的不明白我需要改变什么.

这是我得到的代码.

• 使用Logic monad需要更改哪些代码？
• 额外奖励:使用Logic monad有什么具体的性能优势吗？

---

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

好的,改变你使用的代码Logic结果是完全无足轻重的.我通过重写所有内容来使用普通Set函数而不是Setmonad,因为你并没有真正Set以统一的方式使用monadically,当然也不是为了回溯逻辑.monad理解也更清楚地写成地图和过滤器等.这不需要发生,但它确实帮助我理解正在发生的事情,并且它肯定显而易见的是,用于回溯的一个真正剩余的monad就是Maybe.

在任何情况下,你可以概括的类型签名pureRule,oneRule和dpll超过不仅仅是操作Maybe,但任何m有约束MonadPlus m =>.

然后,在pureRule你的类型将不匹配,因为你Maybe明确地构造s,所以去改变它:

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

变

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

并且oneRule,同样地将使用更改为listToMaybe显式匹配

   x <- (listToMaybe . toList) singletons

变

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

并且,在类型签名更改之外,dpll根本不需要更改!

现在,你的代码工作在两个 Maybe 及 Logic!

要运行Logic代码,您可以使用如下函数:

dpllLogic s = observe $ dpll' s

您可以使用observeAll等来查看更多结果.

供参考,这是完整的工作代码:

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

使用Logic monad有什么具体的性能优势吗？

TL; DR:不是我能找到的; 它看起来Maybe表现优异,Logic因为它的开销较小.

我决定实施一个简单的基准来检查Logic对比的性能Maybe.在我的测试中,我随机构造了带有n子句的5000个CNF ,每个子句包含三个文字.随着条款数量的n变化,评估绩效.

在我的代码中,我修改dpllLogic如下:

dpllLogic s = listToMaybe $ observeMany 1 $ dpll s

我还测试了修正dpll与公平分离,如下所示:

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'

我则利用测试Maybe,Logic和Logic公平脱节.

以下是此测试的基准测试结果:

我们可以看到,Logic在这种情况下,无论有没有公平分离,都没有区别.dpll使用Maybemonad 的求解似乎在线性时间内运行n,而使用Logicmonad会产生额外的开销.似乎开销导致了高原.

这是Main.hs用于生成这些测试的文件.希望重现这些基准的人可能希望查看Haskell关于分析的说明:

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)