haskell - Monad 的应用

Question

下面的代码用于测试 2-SAT bool 公式(仅包含 X v Y 形式的子句的公式)的可满足性。尽管存在其他算法(关联蕴涵图的强连接组件、通过 SLUR 进行文字赋值)，但该程序通过递归应用解析直到找到空子句(即发现隐含矛盾)来实现此目的。我已经注释了代码来解释它是如何工作的(以防万一)

尽管代码可以编译/运行，但我还是忍不住觉得它有点“hacky”，并且可以通过使用 Monads 让它变得更像 Haskell。

-- Literals are numbered and are identified by their integer number X; -X represents a negated integer 
-- A 2-CNF clause X v Y  is represented by a tuple of a 2 integers (X,Y)  
-- 0 represents a empty space (i.e. a non existing literal). So (X,0) or (0,X) is a unit clause and (0,0) represents an empty clause

isEmptyClause :: (Int,Int) -> Bool
isEmptyClause c = (fst c == 0) && (snd c == 0) -- c denotes a clause. (0,0) is an empty clause

isUnitClause :: (Int,Int) -> Bool
isUnitClause c = not (c `isEmptyClause`) && (fst c ==0 || snd c == 0 || uncurry (==) c ) -- c denotes a clause. A unit clause has one literal. Three cases : (X,0)=(0,X)=(X,X)

isTautological :: (Int,Int) -> Bool
isTautological c = not (c `isEmptyClause`) && (fst c == - snd c) -- c denotes a clause. (X,-X) is a tautological clause as it is always true, thus meaningless

isSamePair :: (Int,Int) -> (Int,Int) -> Bool
isSamePair p p' = fst p == fst p' && snd p==snd p' || fst p==snd p' && snd p==fst p' -- p and p' denote a pair of integers, each in a tuple. NB : 2 cases (X,Y)=(X,Y)=(Y,X)

isIdentical :: (Int,Int) -> (Int,Int) -> Bool
isIdentical c d = c' `isSamePair` d' -- c and d denote clauses to be compared.
                where c' = checkHiddenUnitClause c ; d' = checkHiddenUnitClause d -- making sure that (X,X) => (X,0) for clauses c and d 

containsClause :: [(Int,Int)]-> (Int,Int) -> Bool
containsClause s c = any (isIdentical c) s -- s denotes a set of clauses and c denotes an individual clause

derivedClause :: (Int,Int) -> (Int,Int) -> (Int,Int) -- derived through resolution
derivedClause c c' -- c and c' denote clauses to be potentially resolved. resolution : AvB,-BvC => AvC. Four possible cases
    | fst c /=0 && fst c == - fst c' = (snd c,snd c') -- (X,Y), (-X,Z) => (Y,Z)
    | fst c /=0 &&fst c == - snd c' = (snd c,fst c') -- (X,Y), (Z,-X) => (Y,Z)
    | snd c /=0 && snd c == - fst c' = (fst c,snd c') -- (Y,X), (-X,Z) => (Y,Z)
    | snd c /=0 && snd c == - snd c' = (fst c,fst c') -- (Y,X), (Z,-X) => (Y,Z)
    | otherwise = (1,-1) -- this results in a tautological clause, and is thus harmless/meaningless. will be filtered out

derivedClauses :: (Int,Int) -> [(Int,Int)] -> [(Int,Int)] -- takes a clause and see if there are any resulting derived clauses by applying resolution to a set of clauses
derivedClauses c s = filter (not.isTautological) s' -- Any derivation that results in a tautological clause is filtered out of the derived set
                    where s' = map (derivedClause c) s -- c is a clause and s being a set of existing resulting clauses. the result s' is a derived set of clauses (from applying resolution)

-- Potentially a clause in the original clause set or any subsequently derived clause can be of the form (X,X), however because X v X => X : (X,X) => (X,0). 
-- getting clauses to the form (X,0) or (0,X) is essential if we ever want to find the empty clause (0,0) through resolution. Thus the clause may need to be rewritten as (X,0)
checkHiddenUnitClause :: (Int,Int)-> (Int,Int)
checkHiddenUnitClause c -- c denotes a clause.  
    | not (c `isUnitClause`) = c -- returns just the clause c if it is not a unit clause
    | fst c == 0 = c -- returns (0,X) if the unit clause is of the form (0,X)
    | otherwise = (fst c, 0) -- returns the unit clause in the form (X,0)

-- The following function expands the set of clauses by finding derived clauses (through resolution)
-- This recursive function does so by establishing a stack of existing clauses and a set of of resulting clauses
-- By "popping" the stack, clauses are assessed one by one and matched up against each of the resulting clauses for a possible derivation of a new clause (through resolution) 
-- The newly derived clauses are placed on the clause stack
-- The "popped" clause is added to the set of resulting clauses
-- the recursion terminates and unwinds, when the clause stack is emptied or when an empty clause is found in the clause stack (in which case the function results in an empty set)
expandClauseSet :: ([(Int,Int)],[(Int,Int)]) -> ([(Int,Int)], [(Int,Int)]) -- establishes a clause stack and a seperate set of resulting clauses
expandClauseSet ([],s) = ([], s) -- s is the set of resulting clauses. If the end of the clause stack is reached, the function returns the set of resulting clauses
expandClauseSet (c:cs,s) -- cs is the clause stack and c is the clause popped off the clause stack. s is the set of resulting clauses
    | (c `isEmptyClause`) = ([],[]) -- if an empty clause is found, return an empty clause stack and an empty set of resulting clauses
    | (c `isTautological`) || (s `containsClause` c') = expandClauseSet (cs, s) -- ignore the popped clause if it is tautological or already exists in the set of resulting clauses
    | otherwise = expandClauseSet (cs ++ derivedClauses c' s, c':s) -- add derived clauses to to the claus stack and add the popped clause to the set of resulting clauses
    where c' = checkHiddenUnitClause c -- this is to verify that the popped clauses is not actually a hidden unit clause. if so, modify it to a regular unit clause c'

expandedClauseSet :: [(Int,Int)] -> [(Int,Int)]
expandedClauseSet [] = []
expandedClauseSet s = snd (expandClauseSet (s,[])) -- s denotes a set of clauses

isSatisfiable :: [(Int,Int)] -> Bool
isSatisfiable s = expandedClauseSet s /= [] -- s denotes a set of clauses to be checked for satifiability

我可能会看到三个领域出现这种情况，并且可以使用 Monad:

1. 如果没有要应用的解决方案，衍生子句函数将返回一个同义反复子句；这看起来有点像黑客。返回 Nothing 可能会更好。这是否意味着我应该用 Maybe monad 重写 (Int,Int) 元组的所有实例，还是应该是一个 Monoid(仍然在与 monad 斗争)？

2. 每个子句都由表示子句中两个文字的(Int,Int)元组表示。这很好，但也许拥有我自己的定义会更好(也许我想要一些其他的文字定义而不是 Int)。我正在尝试获取我自己类型的声明，例如:

   data Clause = Clause {literal ::Int, otherLiteral :: Int)
   

   原则上这应该可行，对吗？然而，在重构其余代码时，我遇到了很多类型错误。也许我只是错过了一些东西。这是否值得追求，或者它的方式更清晰？另外，我想这与上一点有关，如果不存在的文字或空白可以用 Nothing 而不是数字 0 来表示不是更好吗？

3. expandClauseSet 递归函数处理其堆栈和结果列表的方式在我看来也非常像 State monad(结果列表是状态)。我的想法是否正确，或者这是否让单子(monad)走得太远了？

Answer 1

我将从(2)开始:您的数据表示似乎不能很好地表示您在问题陈述中描述的数据。你总是有两个整数，即使你实际上只意味着一个或根本没有。因此，您必须到处进行大量检查，以确定您实际上应该注意多少个整数。并且正数和负数之间存在这种特殊关系，这种关系没有反射(reflect)在类型中。

相反，就像 Haskell 中经常发生的那样，从每个域对象的 data 定义开始，并为您想要建模的每个单独的“案例”提供构造函数。对该域进行建模的一种直接方法是

data Variable = Variable Int deriving Eq

data Literal = LitTrue Variable
             | LitFalse Variable
   deriving Eq

data Clause = Contradiction
            | Tautology
            | Unit Literal
            | Disjunction Literal Literal

data Formula = Conjunction [Clause]

真的，我会做更多，比如参数化 Literal 类型，而不是将其固定为 Int，但这已经是一个很大的改进。您编写的许多函数甚至不再需要存在:模式匹配已经做到了。

但是当然，您仍然需要某个地方的函数来执行逻辑，例如“x0 ∨ Øx0”子句会导致同义反复。该函数可能如下所示:

negateLit :: Literal -> Literal
negateLit (LitTrue x) = LitFalse x
negateLit (LitFalse x) = LitTrue x

clause :: Literal -> Literal -> Clause
clause x y | x == y = Unit x
           | x == negateLit y = Tautology
           | otherwise = Disjunction x y

衍生子句是一个仍然需要存在的函数，并且涉及低级表示，所以我想我会展示它在新表示中的外观。您需要几个额外的子句来解决单位子句不再伪装成两期子句的事实。另一方面，您不必再检查事物是否为 0，因为没有任何东西是这样表示的。

derivedClause :: Clause -> Clause -> Clause
derivedClause l@(Unit _) r@(Disjunction _ _) = derivedClause r l
derivedClause (Disjunction x y) (Unit u)
  | x == u' = Unit y
  | y == u' = Unit x
  where u' = negateLit u
derivedClause (Disjunction x y) (Disjunction p q) 
  | x == p' = clause y q
  | x == q' = clause y p
  | y == p' = clause x q
  | y == q' = clause x p
  where p' = negateLit p
        q' = negateLit q
derivedClause _ _ = Tautology

我也同意你的(1):衍生子句应该真正返回一个Maybe Clause，而不是返回一个可能有用或可能没用的子句。但您不必为此重写整个程序:只需 providedClause 的直接客户端即可。

至于(3)和你的标题，我没有看到任何令人信服的理由在这里使用任何单子(monad)机制。没有什么非常有状态的事情发生:您只是有一个从公式到公式的函数，您可以对其进行迭代，直到您对结果感到满意为止。