在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)