Использование Logic Monad в Haskell

Ответ 1

Хорошо, изменение кода для использования Logic оказалось совершенно тривиальным. Я прошел и переписал все, чтобы использовать обычные функции Set, а не монаду Set, потому что вы на самом деле не используете Set в унифицированном виде, и, конечно же, не для логики обратного отслеживания. Монадские постижения также были более четко написаны как карты, фильтры и тому подобное. Этого не должно было случиться, но это помогло мне разобраться в происходящем, и это, безусловно, показало, что одна настоящая оставшаяся монада, используемая для обратного отсчета, была просто Maybe.

В любом случае вы можете просто обобщить сигнатуру типа pureRule, oneRule и dpll для работы не только Maybe, но и любого m с ограничением MonadPlus 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 [email protected](_ :|-:  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 [email protected](_ :|-:  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' [email protected](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

Ответ 2

Есть ли какое-либо конкретное преимущество в использовании логической монады?

TL; DR: Не то, что я могу найти; кажется, что Maybe превосходит Logic, так как имеет меньше накладных расходов.

Я решил реализовать простой тест, чтобы проверить производительность Logic по сравнению с Maybe. В моем тесте я произвольно строю 5000 CNF с предложениями n, каждая статья содержит три литерала. Производительность оценивается по мере изменения количества предложений n.

В моем коде я изменил dpllLogic следующим образом:

dpllLogic s = listToMaybe $ observeMany 1 $ dpll s

Я также протестировал модификацию dpll с честной дизъюнкцией, например:

dpll goalClauses = dpll' $ S.empty :|-: goalClauses
  where
     dpll' [email protected](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 с или без справедливой дизъюнкции в этом случае не имеет значения. Решение dpll, использующее монаду Maybe, похоже, работает в линейном времени в 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)