在 Haskell 中使用 Logic Monad

Question

最近，我在 Haskell 中实现了一个幼稚的 DPLL Sat Solver，改编自 John Harrison 的 Handbook of Practical Logic and Automated Reasoning。

DPLL 是多种回溯搜索，所以我想尝试使用来自Oleg Kiselyov et al 的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 ]

Answer 1

好的，将您的代码更改为使用Logic 原来是完全微不足道的。我经历并重写了所有内容以使用普通的Set 函数而不是Set monad，因为你并没有真正以统一的方式使用Set monadically，当然也不是为了回溯逻辑。 monad 理解也更清楚地写成映射和过滤器等。这不需要发生，但它确实帮助我理清了正在发生的事情，而且它确实清楚地表明，用于回溯的真正剩余的 monad 只是 Maybe。

在任何情况下，您都可以将pureRule、oneRule 和dpll 的类型签名推广到不仅可以操作Maybe，还可以操作任何带有约束m 的m。

那么，在pureRule 中，你的类型将不匹配，因为你明确地构造了Maybes，所以去修改一下吧：

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 的性能。 在我的测试中，我随机构造了 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 monad 的dpll 求解似乎在n 中以线性时间运行，而使用Logic monad 会产生额外的开销。似乎开销导致平台期结束。

这是用于生成这些测试的Main.hs 文件。希望重现这些基准的人可能希望查看Haskell's notes on profiling：

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)