haskell - 在 Haskell 中使用 Logic Monad

Question

最近，我在Haskell中实现了一个朴素的DPLL Sat Solver，改编自 John Harrison 的实用逻辑和自动推理手册。

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 ]

Answer 1

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

在任何情况下，您都可以概括, 和的类型签名pureRule，不仅可以对 进行操作，还可以对任何带有约束的进行操作。oneRuledpllMaybemMonadPlus m =>

然后， in pureRule，您的类型将不匹配，因为您Maybe显式构造了 s，因此请稍作更改：

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

变成

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

在 中oneRule，同样将 of 的用法更改为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因为它的开销更少。

---

我决定实施一个简单的基准来检查Logicvs的性能Maybe。在我的测试中，我随机构造了 5000 个带有n子句的 CNF，每个子句包含三个文字。随着子句数量的n变化，评估性能。

在我的代码中，我修改dpllLogic如下：

dpllLogic s = listToMaybe $ observeMany 1 $ dpll s

我还dpll用fair disjunction测试了修改，如下所示：

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'

然后我用公平的分离测试了 using Maybe, Logic, and 。Logic

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

正如我们所看到的，Logic在这种情况下，无论是否公平分离都没有区别。使用 monad的dpll求解Maybe似乎在 中以线性时间运行n，而使用Logicmonad 会产生额外的开销。似乎开销导致平台期结束。

这是Main.hs用于生成这些测试的文件。希望重现这些基准的人可能希望查看Haskell 关于 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)