最近,我在Haskell中实现了朴素的DPLL Sat Solver,改编自John Harrison的Handbook of Practical Logic and Automated Reasoning

DPLL是各种回溯搜索,因此我想尝试使用Logic monad中的Oleg Kiselyov et al。但是,我不太了解需要更改什么。

这是我得到的代码。

  • 使用逻辑单子(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 ]
    

    最佳答案

    好的,更改代码以使用Logic完全是微不足道的。我仔细阅读并重写了所有内容,以使用普通的Set函数而不是Set monad,因为您并不是真正地以统一的方式单字使用Set,当然也不是为了回溯逻辑。 monad的理解也更清楚地写为 map 和过滤器等。不需要发生这种情况,但是它确实帮助我对发生的事情进行了分类,并且可以肯定地证明,用于回溯的一个真正剩余的monad只是Maybe

    在任何情况下,您都可以泛化pureRuleoneRuledpll的类型签名,以不仅对Maybe进行操作,还可以对任何具有m约束的MonadPlus m =>进行操作。

    然后,在pureRule中,您的类型将不匹配,因为您显式构造了Maybe,因此请对其进行一些更改:

    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根本不需要更改!

    现在,您的代码可以同时在MaybeLogic上运行!

    要运行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
    

    关于haskell - 在Haskell中使用Logic Monad,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/11695961/

    10-11 22:34
    查看更多