Implementation of Davis, Putnam, Logemann, Loveland (DPLL) theorem proving (Davis, Logemann, and Loveland 1962,Davis and Putnam (1960)) for propositional logic. The implementation uses discrimination trees or tries, following (Zhang and Stickel 2000).
> module DPLL
>
> where
>
> import Data.ListIf we let variables be represented by their indices, with the convention that positive indices represent positive literals and the negation of an index represents the negation of the variable, then clauses can be represented as integer lists, and clause sets as lists of integer lists.
> type Clause = [Integer]
> type ClauseSet = [Clause]A valuation is simply a list of integers:
> type Valuation = [Integer]Reorder the literals in a clause to make sure that lowest variable indices are listed first. Also, throw out duplicate literals from clauses and duplicate clauses from clause sets.
> rSort :: ClauseSet -> ClauseSet
> rSort = (srt1.nub) . (map (srt2. nub))
> where srt1 = sortBy cmp
> cmp [] (_:_) = LT
> cmp [] [] = EQ
> cmp (_:_) [] = GT
> cmp (x:xs) (y:ys) | (abs x) < (abs y) = LT
> | (abs x) > (abs y) = GT
> | (abs x) == (abs y) = cmp xs ys
> srt2 = sortBy (\ x y -> compare (abs x) (abs y))A clause is trivial if the clause contains both positive and negative occurrences of some literal.
> trivialC :: Clause -> Bool
> trivialC [] = False
> trivialC (i:is) = elem (-i) is || trivialC isThe function clsNub removes trivial clauses from a clause set.
> clsNub :: ClauseSet -> ClauseSet
> clsNub = filter (not.trivialC) The datatype of discrimination trees.
> data Trie = Nil | End | Tr Integer Trie Trie Trie deriving (Eq,Show)Nil is the empty clause set, End a marker for a clause end.
In a trie of the form \((\text{Tr}, v, P, N, R)\), \(P\) encodes a clause set \(\{ P_1, \ldots, P_n \}\) representing \(\{ v \lor P_1, \ldots, v \lor P_n \}\), \(N\) a clause set \(\{ N_1, \ldots, N_m \}\) representing \(\{ \neg v \lor N_1, \ldots, \neg v \lor N_m \}\), and \(R\) a clause set \(\{ R_1, \ldots , R_k \}\) with none of the \(R_i\) containing occurrences of \(v\).
If the clause set corresponding to \(P\) equals \(\Box\), and the clause set corresponding to \(N\) equals \(\Box\), this means that both \(\{ v \}\) and \(\{ \neg v \}\) occur in the clause set, i.e., that the clause set is a contradiction (equals \(\Box\)).
If the clause sets corresponding to \(P\) and \(Q\) are both empty, this means that \(v\) does not occur (positively or negatively) in the clause set.
If the clause set corresponding to \(R\) equals \(\Box\), this means that the whole clause set equals \(\Box\). If the clause set corresponding to \(R\) is empty, this means that the clause set does not contain clauses without positive or negative occurrences of \(v\).
Bearing this in mind, the following operation can be used to perform some simplifications.
> nubT :: Trie -> Trie
> nubT (Tr v p n End) = End
> nubT (Tr v End End r) = End
> nubT (Tr v Nil Nil r) = r
> nubT tr = trThe trie merge operation (conjunction of the corresponding clause sets):
> trieMerge :: Trie -> Trie -> Trie
> trieMerge End _ = End
> trieMerge _ End = End
> trieMerge t1 Nil = t1
> trieMerge Nil t2 = t2
> trieMerge t1@(Tr v1 p1 n1 r1) t2@(Tr v2 p2 n2 r2)
> | v1 == v2 = (Tr
> v1
> (trieMerge p1 p2)
> (trieMerge n1 n2)
> (trieMerge r1 r2)
> )
> | v1 < v2 = (Tr
> v1
> p1
> n1
> (trieMerge r1 t2)
> )
> | v1 > v2 = (Tr
> v2
> p2
> n2
> (trieMerge r2 t1)
> )Assuming clauses are r-sorted, mapping clause sets into ordered tries is done as follows:
> cls2trie :: ClauseSet -> Trie
> cls2trie [] = Nil
> cls2trie ([]:_) = End
> cls2trie cls@((i:is):_) =
> let j = abs i in
> (Tr
> j
> (cls2trie [ filter (/= j) cl | cl <- cls, elem j cl ])
> (cls2trie [ filter (/= -j) cl | cl <- cls, elem (-j) cl ])
> (cls2trie [ cl | cl <- cls, notElem j cl, notElem (-j) cl ])
> )Tries are mapped back into clause sets by:
> trie2cls :: Trie -> ClauseSet
> trie2cls Nil = []
> trie2cls End = [[]]
> trie2cls (Tr i p n r) =
> [ i:rest | rest <- trie2cls p ]
> ++
> [ (-i):rest | rest <- trie2cls n ]
> ++
> trie2cls rUnit clause detection in the trie format; the following function finds all unit clauses:
> units :: Trie -> [Integer]
> units Nil = []
> units End = []
> units (Tr i End n r) = i : units r
> units (Tr i p End r) = -i: units r
> units (Tr i p n r) = units rUnit propagation:
> unitProp :: (Valuation,Trie) -> (Valuation,Trie)
> unitProp (val,tr) = (nub (val ++ val'), unitPr val' tr)
> where
> val' = units tr
> unitPr :: Valuation -> Trie -> Trie
> unitPr [] tr = tr
> unitPr (i:is) tr = unitPr is (unitSR i tr) Unit subsumption and resolution.
> unitSR :: Integer -> Trie -> Trie
> unitSR i = (unitR pol j) . (unitS pol j)
> where pol = i>0
> j = abs iUnit subsumption: delete every clause containing the literal. The literal is encoded as (pol,i), where pol gives the sign and i is a positive integer giving the index of the variable.
> unitS :: Bool -> Integer -> Trie -> Trie
> unitS pol i Nil = Nil
> unitS pol i End = End
> unitS pol i tr@(Tr j p n r) | i == j = if pol
> then nubT (Tr j Nil n r)
> else nubT (Tr j p Nil r)
> | i < j = tr
> | i > j = nubT (Tr
> j
> (unitS pol i p)
> (unitS pol i n)
> (unitS pol i r)
> )Unit resolution: delete the mate of the literal from every clause containing it.
> unitR :: Bool -> Integer -> Trie -> Trie
> unitR pol i Nil = Nil
> unitR pol i End = End
> unitR pol i tr@(Tr j p n r) | i == j = if pol
> then
> nubT (Tr
> j
> p
> Nil
> (trieMerge n r)
> )
> else
> nubT (Tr
> j
> Nil
> n
> (trieMerge p r)
> )
> | i < j = tr
> | i > j = nubT (Tr
> j
> (unitR pol i p)
> (unitR pol i n)
> (unitR pol i r)
> )To treat splitting, we need functions for setting variables to true and false, respectively. Setting a variable to true is done by:
> setTrue :: Integer -> Trie -> Trie
> setTrue i Nil = Nil
> setTrue i End = End
> setTrue i tr@(Tr j p n r) | i == j = trieMerge n r
> | i < j = tr
> | i > j = (Tr
> j
> (setTrue i p)
> (setTrue i n)
> (setTrue i r)
> )Setting a variable to false is done similarly:
> setFalse :: Integer -> Trie -> Trie
> setFalse i Nil = Nil
> setFalse i End = End
> setFalse i tr@(Tr j p n r) | i == j = trieMerge p r
> | i < j = tr
> | i > j = (Tr
> j
> (setFalse i p)
> (setFalse i n)
> (setFalse i r)
> )Always split on the first variable:
> split :: (Valuation,Trie) -> [(Valuation,Trie)]
> split (v,Nil) = [(v,Nil)]
> split (v,End) = []
> split (v, tr@(Tr i p n r)) = [(v++[i], setTrue i tr),
> (v++[-i],setFalse i tr)]Davis, Putnam, Loveland, Longeman (DPLL): keep splitting after unit propagation.
> dpll :: (Valuation,Trie) -> [(Valuation,Trie)]
> dpll (val,Nil) = [(val,Nil)]
> dpll (val,End) = []
> dpll (val,tr) =
> concat [ dpll vt | vt <- (split.unitProp) (val,tr) ]Wrap it all up:
> dp :: ClauseSet -> [(Valuation,Trie)]
> dp cls = dpll ([], (cls2trie . rSort) (clsNub cls))Davis, M., and H. Putnam. 1960. “A Computing Procedure for Quantification Theory.” Journal of the ACM 7 (3): 201–15.
Davis, M., G. Logemann, and D. Loveland. 1962. “A Machine Program for Theorem Proving.” Communications of the ACM 5 (7): 394–97.
Zhang, Hantao, and Mark E. Stickel. 2000. “Implementing the Davis-Putnam Method.” Journal of Automated Reasoning 24 (1/2): 277–96.