在Haskell中使用逻辑Monad

Question

最近，我在Haskell中实现了一个朴素的DPLL Sat Solver，参考自John Harrison的Handbook of Practical Logic and Automated Reasoning。

DPLL是一种回溯搜索算法，因此我想尝试使用Oleg Kiselyov等人的Logic monad进行实验。然而，我并不真正理解需要改变什么。

这是我目前的代码。

• 我需要更改哪些代码才能使用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 ]

- Matt W-D

---

@DanielWagner：真的吗？做回溯的部分是msum，我认为我只需要修改dpll'…？ - Matt W-D

Answer 1

好的，将您的代码更改为使用Logic完全是微不足道的。我重写了所有内容，使用普通的Set函数而不是Set单子，因为您并没有以统一的方式真正使用Set单子，当然也没有用于回溯逻辑。单子理解还可以更清晰地写成映射和过滤器等。这不是必须发生的，但它确实帮助我整理了正在发生的事情，并且肯定表明了仅剩的一个真正的单子，用于回溯，只是Maybe。

无论如何，您可以将pureRule、oneRule和dpll的类型签名概括为不仅适用于Maybe，而且适用于任何具有约束条件MonadPlus m =>的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 不需要任何更改！

现在，您的代码可以处理 同时存在的 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

- sclv

Answer 2

有没有使用Logic Monad有具体的性能优势？

简短回答：根据我的发现，好像没有；因为它的开销更小，所以可能性能更高。

我决定实现一个简单的基准测试来检查Logic与Maybe的性能。在我的测试中，我随机构建了5000个含有n个子句（每个子句都包含三个文字）的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没有区别。使用Maybe单子运行的dpll求解似乎在n中以线性时间运行，而使用Logic单子会产生额外的开销。它似乎产生的开销趋于平稳。

这是用于生成这些测试的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)

- Matt W-D