在Haskell中使用逻辑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，当然也不是用于回溯逻辑。 monad的理解也更清晰地写成地图和过滤器等等。这并不需要发生，但它确实帮助我对发生的事情进行了排序，并且显然确定了用于回溯的一个真正剩余的monad只是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 

成为

​​

而且，类型签名的变化之外，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

有没有什么具体的性能优势，使用逻辑单子？

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有或没​​有在这种情况下公平脱节没什么区别。使用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)