Automated Theorem Proving, The Davis Putnam Algorithm

by Alex Nelson, 15 February 2015

Introduction

So, finding out if a given formula is satisfiable is…hard. But it’s the core of the program we’re writing. Today, we’ll discuss a method to determine if a formula is satisfiable, namely the Davis-Putnam algorithm.

It consists of three steps:

  1. Transform the input to conjunctive normal form.
  2. Apply Simplification Rules
  3. Splitting.

But look, step 1 (the preprocessing step) blows up exponentially…as we saw last time.

This time, we will figure out how to avoid this problem introducing “Definitional CNF” for the preprocessing step.

Then we will introduce and discuss the Davis-Putnam algorithm. This corresponds to v0.1.2 of the code.

Definitional Conjunctive Normal Form

The basic idea is to introduce new variables corresponding to subformulas. The textbook example is And (Or p (And q (Not r))) s which transforms via the following steps:

And (Or p
        (And q (Not r)))
    s -> And (Iff p1 (And q (Not r))) -- introduce p1
             (And (Or p p1) s)        -- updated formula
      -> And (Iff p1 (And q (Not r)))
             (And (Iff p2 (Or p p1)) -- introduce p2
                  (And p2 s))        -- updated formula
      -> And (Iff p1 (And q (Not r)))
             (And (Iff p2 (Or p p1))
                  (And (Iff p3 (And p2 s)) -- introduce p3
                       p3))                -- our running formula is p3!

This is clearly equisatisfiable (i.e., a choise for p, q, and r will solve both formulas), but since we have these extra variables p1, p2, p3…we have too much freedom in this transformed formula. This extra freedom denies us the ability to say these formulas are equivalent (just choose one of these new variables in the wrong way). Indeed, if we run it through our automated theorem prover, we find:

textbookDefCNFTest :: () -> String
textbookDefCNFTest _ =
  testToStr (Iff (And (Or p (And q (Not r))) s)
                 (And (Iff p1 (And q (Not r)))
                      (And (Iff p2 (Or p p1))
                           (And (Iff p3 (And p2 s))
                                p3))))
  where p = Atom "p"
        q = Atom "q"
        r = Atom "r"
        s = Atom "s"
        p1 = Atom "p1"
        p2 = Atom "p2"
        p3 = Atom "p3"
             
main :: IO ()
main = putStrLn $ textbookDefCNFTest ()
-- prints "[The formula] is false

But they’re equisatisfiable, so it’s safe for this as a preprocessing step for equisatisfiability testing.

We then plug this into the “vanilla” toCNF function (or something similar).

Remark. The notion of “definitional CNF” appears to originate from T. B. de la Tour’s “Minimizing the number of clauses by renaming” (in Stickel, ed., 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, Springer-Verlag, 1990; pages 558–572). But the term “definitional CNF”, as far as I can tell, seems to be coined by John Harrison. (End of Remark)

Implementation

The basic design to convert a formula into definitional conjunctive normal form is to use Trip’s:

-- | A triple tracking the formula to be transformed,
-- definitions made so far (as a dictionary, well 'Data.Map'),
-- and the current variable index counter.
type Trip = (Formula, Map Formula (Formula, Formula), Int)

We transform this triple (transform the formula, augment the definition dictionary, and increment the index counter) in a recursive function mainCNF which calls defstep. This defstep does the real work, and recursively calls mainCNF until the formula is in definition CNF.

-- | Iteratively transform a formula, represented as a 'Trip', into
-- set-based definitional conjunctive normal form.
mainCNF :: Trip -> Trip
mainCNF (trip@(fm, _, _)) = case fm of
  And p q -> defstep And (p, q) trip
  Or p q  -> defstep Or (p, q) trip
  Iff p q -> defstep Iff (p, q) trip
  _       -> trip

This seems like a bad idea, since trampolines are generally “bad form”. Alas, I know no better way to handle this.

-- | Takes a binary connective, an ordered pair of formulas, and a 'Trip'
-- then transforms this into another 'Trip'
defstep :: (Formula -> Formula -> Formula) -> (Formula, Formula) -> Trip -> Trip
defstep op (p, q) (_, defs, n) =
  let (fm1, defs1, n1) = mainCNF (p, defs, n)   --- recur on arguments of 
      (fm2, defs2, n2) = mainCNF (q, defs1, n1) --- the binary connective
      fm' = op fm1 fm2 --- apply op to the transformed arguments
  in case Map.lookup --- lookup
          fm'        --- the formula fm'
          defs2 of   --- in the dictionary from mainCNF called on q
      Just (v, _) -> (v, defs, n2) --- if it's found, return it
      Nothing -> (v, Map.insert fm' (v, Iff v fm') defs2, n3) --- otherwise
        where (v, n3) = makeProp n2 --- add it to the dictionary, return it

The defstep function does quite a bit of work, which basically keeps track of the definitions in the dictionary component of Trip. It updates the running formula to reflect this, and increments the index counter as needed.

We have a brief aside on helper functions. One, maybeRead, gets a string and returns a Maybe gadget — if something went wrong, it’s Nothing; otherwise it’s Just [result]. We use this to figure out the greatest variable index:

-- | Return whichever is larger of the argument n, or all possible m
-- such that the string argument s is pfx followed by the string corresponding
-- to m, if any:
maxVarIndex :: String -> String -> Int -> Int
maxVarIndex pfx s n =
  let m = length pfx
      l = length s
  in if l <= m || take m s /= pfx
     then n
     else let s' = take (l-m) (drop m s)
          in case maybeRead s'
             of Nothing -> n
                Just n' -> max n n'

The subtle details of this function are not terribly important at the moment.

Now, we use mainCNF to transform a Formula to definitional conjunctive normal form, à la set based representation. We slightly generalize the procedure to do this to let us pass in an arbitrary (Trip->Trip) function (why be constrained to one particular choice?).

-- | Transform the clauses to definitional CNF, and return the set-based
-- representation of the given formula.
mkDefCNF :: (Trip -> Trip) -> Formula -> [[Formula]]
mkDefCNF fn fm =
  let fm' = toNENF fm
      n = 1 + foldr (maxVarIndex "p_" . show) 0 (atoms fm')
      (fm'', defs, _) = fn (fm', Map.empty, n)
      --- recall dict entry is something like "(fm', (v, Iff v fm'))"
      deflist = map (snd . snd) --- project out the definitions "Iff v fm'"
                    (Map.toList defs) --- from all dictionary entries
  in Set.unions $ simpCNF fm'' : map simpCNF deflist

Then we use this set-based representation of the definitional CNF to construct the Formula representation:

toDefCNF :: Formula -> Formula
toDefCNF fm = foldlConj             --- turn the list of clauses into a Formula
              $ map foldrDisj       --- turn the clauses into Formulas
              $ mkDefCNF mainCNF fm --- transform to set-based def CNF

This is the vanilla implementation just “following our nose”.

Optimization

But look, do we really need to worry if the formula looks like (And p q)? Naively, it would transform into (And (Iff p1 q) (And (Iff p2 (And p p1)) p2). Why not just go “as far as possible”, and transform only when forced?

That is to say, if we consider the formula

And (And p
         (And q
              (Implies (Or r s)
                       t)))
--- why not just transform (Implies (Or r s) t) ? That is, produce:
--- And (toCNF (Iff p1 (Implies (Or r s) t)))
---     (And (And p
---               (And q p1)))

We have some “pre-preprocessing” steps to avoid needlessly transforming subformulas.

-- apply a (Trip -> Trip) transformation to the subformulas,
-- sharing the definitions 
subCNF :: (Trip -> Trip) -> (Formula -> Formula -> Formula)
          -> (Formula, Formula) -> Trip -> Trip
subCNF subfn op (p, q) (_, defs, n) =
  let (fm1, defs1, n1) = subfn (p, defs, n)
      (fm2, defs2, n2) = subfn (q, defs1, n1)
  in (op fm1 fm2, defs2, n2)

So, what happens? We recursively descend through disjunctions performing the definitional transformation on the disjuncts:

orCNF :: Trip -> Trip
orCNF trip@(fm, _, _) = case fm of
  Or p q -> subCNF orCNF Or (p, q) trip --- recursively call itself
  _      -> mainCNF trip                --- transform the disjuncts

In turn, we recursively descend through conjunctions calling orCNF on the conjuncts

andCNF :: Trip -> Trip
andCNF trip@(fm, _, _) = case fm of
  And p q -> subCNF andCNF And (p, q) trip
  _       -> orCNF trip

Now, we can transform a formula into the set-based definitional CNF clauses by simply using andCNF. Or more precisely:

defCNFClauses :: Formula -> [[Formula]]
defCNFClauses = mkDefCNF andCNF

Then we get a slightly optimized function converting a formula to definitional conjunctive normal form

-- | A slightly optimized way to convert a formula to definitional CNF.
toDefCNF :: Formula -> Formula
toDefCNF = foldlConj . map foldrDisj . defCNFClauses

Exercise for Author: I should probably do a more thorough algorithm analysis of this version, but as I am tight on time at the moment…I leave it as an exercise. But one for the author! (End of exercise)

Davis-Putnam Algorithm

John Harrison points out (both in his lectures linked below, and his Handbook of Practical Logic) there are two Davis-Putnam algorithms: one from Davis and Putnam’s “A Computing Procedure for Quantification Theory” (Journal of the ACM 7 3 (1960) 201-215), the other from Davis, Logemann, and Loveland’s “A Machine Program for Theorem Proving” (Comm. of the ACM 5 7 (1962) 394-397). Following Harrison, we will follow the chronological route, and consider the former paper first.

The basic outline of the procedure is:

  1. Convert the input formula to CNF.
  2. Apply simplification rules
  3. The “resolution” rule.

Remark. For what its worth, the later 1962 algorithm (which merits the name “DPLL”) simply replaced the “resolution” rule with something else. (End of Remark)

As we have already seen how to convert a formula to conjunctive normal form, lets consider the simplifying rules. Davis-Putnam uses the set-based representation of the conjunctive normal form.

The resulting algorithm resembles the basic outline quite a bit.

Satisfiability-Preserving Transformations

There are two transformations on the sets of clauses:

  1. The 1-literal rule (nowadays called “Unit Propagation”),
  2. The affirmitive-negative rule (sometimes called the “Pure Literal rule”).

Unit Propagation

Definition. A “Unit Clause” is a clause that consists of a single literal. (End of definition)

Unit Propagation Algorithm. If one of the clauses is a unit clause, we can eliminate all instances of that literal and its negation without affecting satisfiability. This can be seen easily in CNF, and removing such literals preserves satisfiability. (End of Algorithm)

Example. Consider the list of clauses [Or a b, Or (Not a) c, Or (Not c) d, a]. Look, the last entry is a, a unit clause. Hence we see for this formula to be satisfiable, we need a to be true.

We then eliminate it from every other clause. Why? Because look, Or T x is equivalent to x. Then we can iterate this “unit propagation” and deduce that x must be true. Hence iterating unit propagation in our example, we have the following trace:

    [Or a b, Or (Not a) c, Or (Not c) d, a]
--- swap "T" for "a" and simplify in all but the unit clause
    [     T,            c, Or (Not c) d, a]
--- "c" is now a unit clause, substitute in "T" for "c" and simplify:
    [     T,            c,            d, a]
--- "d" is now a unit-clause, but we're left with unit clauses, so we're done

We see how satisfiability is preserved along the way. (End of Example)

We can test for a unit clause quite simply:

--- in src/DavisPutnam.hs

isUnitClause :: [Formula] -> Bool
isUnitClause (_:t) = null t
isUnitClause _     = False

This is the lazy way to do it. The naive way, check if the length is equal to 1, won’t work since length is O(n). The clever way is to check the tail is empty, and if there is no tail it must be empty input.

Now we implement the one literal rule:

--- in src/DavisPutnam.hs

-- | The one literal rule for the Davis-Putnam algorithm.
oneLiteralRule :: [[Formula]] -> Maybe [[Formula]]
oneLiteralRule clauses = case find isUnitClause clauses of
                          Nothing -> Nothing
                          Just [u] -> Just (Set.image (Set.\\ [u']) clauses')
                            where u' = negate u
                                  clauses' = filter (notElem u) clauses
                          _ -> error "oneLiteralRule reached impossible state"

Too easy, right?

The Affirmative-Negative Rule

Algorithm. If any literal occurs either only positively or only negatively, then it can be removed without affecting satisfiability. So eliminate all clauses containing such a literal.

Step 1. Find all the literals, partition them into two groups pos which appear positively, and neg which appear negatively.

Step 2. For each literal (not p) in neg, transform this list into positive literals neg = map negate neg.

Step 3. Remove literals from pos which also appear in neg, and set the result to posOnly.

Step 4. Remove literals from neg which also appear in pos, and set the result to negOnly.

Step 5. For each clause C in the given clauses, remove literals which appear in posOnly or negOnly. The resulting filtered list of clauses should be returned, and the algorithm terminates. (End of Algorithm)

The implementation is another “follow your nose” approach

--- in src/DavisPutnam.hs

affirmativeNegativeRule :: [[Formula]] -> Maybe [[Formula]]
affirmativeNegativeRule clauses =
  let (neg', pos) = Data.List.partition negative (Set.unions clauses)
      neg = map negate neg'
      posOnly = Set.difference pos neg
      negOnly = Set.difference neg pos
      pure = Set.union posOnly (map negate negOnly) --- pure literals
  in case pure of
      [] -> Nothing
      _ -> Just (filter                      --- filter out the
                 (null . Set.intersect pure) --- clauses not containing pure
                 clauses)                    --- literals

By construction, this will preserve satisfiability.

Resolution

The basic scheme actually can be illustrated in a theorem.

Theorem. Given a literal $p$, separate a set of clauses $S$ into (i) those containing $p$ only positively, (ii) those containing it only negatively, and (iii) those not containing it at all:

\[S = \{C_{i}\lor p\in S\}^{m}_{i=1}\cup\{D_{j}\lor\neg p\in S\}^{n}_{j=1}\cup S_{0}\]

where none of the $C_{i}$ or $D_{j}$ contain $p$ or its negation. (Further, if either $p$ or $\neg p$ occurs in any clause in $S_{0}$, then both $p$ and $\neg p$ occur together.)

THEN $S$ is satisfiable if and only if $S’ = \{C_{i}\lor D_{j}|1\leq i\leq m, 1\leq j\leq n\}$ is satisfiable. (End of Theorem)

Sketch of Proof. Without loss of generality, we may assume $p$ is positive.

In one direction, we have to show any valuation $v$ satisfying $S$ must also satisfy $S’$. We break this up into cases:

Case 1: $v(p) = \bot$ (= false). Then in the $C_{i}\lor p$ clauses, we see $v(C_{i}) = \top$ (= true) for all $i$. So each $C_{i}$ is satisfied, and hence $C_{i}\lor D_{j}$ would be satisfied too, for any $i$ and $j$.

Case 2: $v(p) = \top$ (= True). Then in the $D_{j}\lor (\neg p)$ clauses, we see $v(D_{j})$ must be $\top$ (True) for all $j$. So each $D_{j}$ is satisfied. Hence $C_{i}\lor D_{j}$ is satisfied by $v$ for all $i$ and $j$.

This concludes the proof in one direction.

The other direction requires a bit more work. Mostly it’s the same reasoning in reverse, we have $v$ satisfy $S’$. Then it must satisfy all $C_{i}$ or all $D_{j}$. In the first case, we extend $v$ to be $v(p)=\bot$ (= False); and in the latter case, we extend $v$ to be $v(p) = \top$ (= True). This sketches the other direction. (End of proof)

Resolution Rule Algorithm. Given a set of clauses S and a literal p, produce a new set of clauses S' which do not have p occuring in any clause.

Step 1. Filter out the set Cs which has p occuring positively, and make sure each element Ci in Cs does not have p occuring in it.

Step 2. Filter out the set Ds which has not p occuring, and make sure each element Dj in Ds does not have not p occuring in it.

Step 3. Assemble the set S' = [Or Ci Dj | Ci <- Cs, Dj <- Ds] of all pairs of elements of the sets we obtained from the first two steps. Return it and terminate the algorithm.

Implementation

The implementation is a little sloppy but straightforward:

--- in src/DavisPutnam.hs

resolveOn :: Formula -> [[Formula]] -> [[Formula]]
resolveOn p clauses =
  let p' = negate p
      (pos, notPos) = List.partition (elem p) clauses
      (neg, s0) = List.partition (elem p') notPos
      pos' = map (filter (/= p)) pos  --- the list of C[i]
      neg' = map (filter (/= p')) neg --- the list of D[j]
      res0 = [c `Set.union` d | c <- pos', d <- neg']
  in Set.union s0 (filter (not . trivial) res0)

We tried to be faithful to the notation used in our theorem.

We then have a crude heuristic

--- in src/DavisPutnam.hs

findBlowup :: [[Formula]] -> Formula -> (Int, Formula)
findBlowup cls l = let m = length(filter (elem l) cls)
                       n = length(filter (elem (negate l)) cls)
                   in (m*n - m - n, l)

Where we want to minimize m*n - m - n. The resolution is built with this in mind:

--- in src/DavisPutnam.hs

resolutionRule :: [[Formula]] -> [[Formula]]
resolutionRule clauses =
  let pvs = filter isPositive (Set.unions clauses)
      (_, p) = Data.List.minimum $ map (findBlowup clauses) pvs
  in resolveOn p clauses

The Davis-Putnam Algorithm

We arrive at the center-piece of the Davis-Putnam algorithm, namely, the algorithm itself! What happens? Well, we first iteratively try unit propagation until it won’t work, then we try the affirmative-negative rule and recurse until it won’t work. At last we use the resolution rule, then recursion takes us back to step 1.

We treat the empty clause as True, and the clause containing the empty set as False. These are the “base conditions” when we bail out of recursion.

--- in src/DavisPutnam.hs

dp :: [[Formula]] -> Bool
dp [] = True
dp clauses =
  if [] `elem` clauses
  then False
  else case oneLiteralRule clauses of
        Just clauses' -> dp clauses'
        Nothing -> case affirmativeNegativeRule clauses of
                    Just clauses' -> dp clauses'
                    Nothing -> dp(resolutionRule clauses)

We can then use this to test for satisfiability and validity:

dpSat :: Formula -> Bool
dpSat = dp . defnfs

dpValidity :: Formula -> Bool
dpValidity fm = not $ dpSat (Not fm)

Lo and behold, this turns out to be somewhat better than the naive approach!

The DPLL Algorithm

The DPLL algorithm modifies the resolution rule, opting for a “splitting rule” instead. What happens?

Well, if neither unit propagation nor the affirmative-negative rule can be applied, then some literal p is chosen. We then check if Clauses ++ [p] is satisfiable, or Clauses ++ [(Not p)] is satisfiable…by recursively using the DPLL algorithm on it.

We need some heuristic for picking which literal to use. Again, a quick-and-dirty heuristic might be the literal that shows up the most:

frequencies :: [[Formula]] -> Formula -> (Int, Formula)
frequencies clauses p = let m = length $ filter (elem p) clauses
                            n = length $ filter (elem (Not p)) clauses
                        in (m+n, p)

We sort using m+n as the primary key, then lexicographically on p (an inadvertent artifact). But the DPLL algorithm is just what we had before,

-- | Return all literals that occur in the formula, negated literals are
-- transformed to be positive.
getLiterals :: [[Formula]] -> [Formula]
getLiterals clauses = let (pos,neg) = Data.List.partition isPositive
                                      $ Set.unions clauses
                      in Set.union pos (map negate neg)

dpll :: [[Formula]] -> bool
dpll [] = True
dpll clauses = if [] `elem` clauses then False else
                 case oneLiteralRule clauses of
                  Just clauses' -> dpll clauses'
                  Nothing -> case affirmativeNegativeRule clauses of
                    Just clauses' -> dpll clauses'
                    Nothing -> --- NEW STUFF FOR DPLL!!
                      let pvs = filter isPositive (Set.unions clauses)
                          lcounts = map (frequencies clauses) pvs 
                          (_, p) = List.maximum lcounts
                      in dpll (Set.insert [p] clauses)
                         || dpll (Set.insert [(negate p)] clauses)

In our definitions for isTautology, etc., we can use dpll instead of dp…if we want to use the dpll algorithm instead, that is.

Optimizations

There are two possible optimizations we can make: Conflict-Driven Clause Learning and Backjumping.

Well, there is low hanging fruit in determining better heuristics for splitting. We leave this as an exercise for the reader ;)

Lemma: Iterative DPLL

This isn’t an optimization per se, but it is necessary for many modern optimizations. We could use a trail to keep track of the guesses we make. We introduce some data structure to keep track of what we do:

data TrailMix = Deduced | Guessed deriving (Eq, Ord)

type Trail = (Formula, TrailMix)

--- The following are just for simplifying the code
type Clauses = [[Formula]]
type Clause = [Formula]

--- Return the atom in the literal
litAbs :: Formula -> Formula
litAbs (Not p) = p
litAbs fm = fm

We will keep track of a list of Trail values. Just a warning: for speed, we have a Trail use a companion Map Formula Formula to keep track of which literals we’ve worked with so far (checking membership is O(log N), nice).

We want to filter our clauses to remove literals in the trail. This is a simple map (filter blah) type function:

-- | Updates the clauses to remove negated literals which do not belong to
-- the trail, as specified by the map.
removeTrailedNegLits :: Map.Map Formula Formula -> Clauses -> Clauses
removeTrailedNegLits m = map (filter (not . (`Map.member` m) . negate))

We also want to generate, for each clause, a list [Maybe Formula] which is Nothing if the literal is in the trail, and Just c if it’s not.

-- | Given a 'Map.Map Formula Formula', and a list '[Formula]',
-- for each element in our list, check if it's a member of the map;
-- if so, map it to 'Just fm', otherwise map it to 'Nothing'.
maybeInclude :: Map.Map Formula Formula -> [Formula] -> [Maybe Formula]
maybeInclude m (c:cls) = if Map.member c m
                         then Nothing : maybeInclude m cls
                         else Just c : maybeInclude m cls
maybeInclude _ [] = []

The last thing we’d like to think about are the undefined units, well, the units not in the trail.

-- | Get all the units from the clauses which are undefined according
-- to our dictionary.
undefinedUnits :: Map.Map Formula Formula -> Clauses -> [Formula]
undefinedUnits m = Set.unions . map (catMaybes . maybeInclude m)

We clean up the clauses, “subpropagate” as apparently the literature calls it, to be consistent with the trail. If there are no undefined unit literals, then we’re at the end of the trail.

If we have some undefined literals, we can extend the trail with them. So why not extend the trail as far as possible? This is the task relegated to subpropagation. Indeed, subpropagation returns the updated clauses and trail.

-- | We keep track of the trail history in the @Map.Map Formula Formula@
-- parameter, the given clause is the first parameter, and the @[Trail]@
-- stars as itself.
unitSubpropagate :: (Clauses, Map.Map Formula Formula, [Trail])
                    -> (Clauses, Map.Map Formula Formula, [Trail])
unitSubpropagate (cls, m, trail) =
  let cls' = removeTrailedNegLits m cls
      newunits = undefinedUnits m cls'
  in if null newunits
     then (cls', m, trail)
     else let trail' = foldr (\l t -> (l, Deduced):t) trail newunits
              m' = foldr (\l mp -> Map.insert l l mp) m newunits
          in unitSubpropagate (cls', m', trail') --- recursion very important!!

Now our unit propagation (recall attempts to get rid of all “units”, or single literals) should take advantage of this subpropagation:

-- | Unit propagation using the newfangled 'Trail'.
btUnitPropagation :: (Clauses, [Trail]) -> (Clauses, [Trail])
btUnitPropagation (cls, trail) =
  let m = foldr (\(l,_) mp -> Map.insert l l mp) Map.empty trail
      (cls', _, trail') = unitSubpropagate (cls, m, trail)
  in (cls', trail')

Caution: Generating the m with foldr may actually be expensive time-wise. I’m sure there’s a smarter way to handle this situation, I just don’t know it. (End of Caution, back to recklessness)

The iterative DPLL then takes advantage of this backtracking unit propagator “in the obvious way”. We actually don’t need the affirmative-negative rule, since backtracking handles things quite well.

We have two helper functions, first when we get a “Conflict” or an unsatisfiable result, we can backtrack the trail until we last took a guess. This is simply:

backtrack :: [Trail] -> [Trail]
backtrack ((_, Deduced):tt) = backtrack tt
backtrack tt = tt

But we also have to get all the literals unassigned to the trail, which is simply a set difference:

-- | All the literals in the clauses not yet assigned to the trail yet.
unassigned :: Clauses -> [Trail] -> [Formula]
unassigned cls trail = Set.difference
                       (Set.unions (Set.image (Set.image litAbs) cls))
                       (Set.image (litAbs . fst) trail)

Then the iterative DPLL algorithm becomes a straightforward backtracking algorithm.

-- | The DPLL algorithm with backtracking.
dpli :: Clauses -> [Trail] -> Bool
dpli cls trail =
  let (cls', trail') = btUnitPropagation (cls, trail)
      hasConflict = elem []
  in if hasConflict cls'                          --- if we get the empty clause
     then case backtrack trail of                 --- backtrack until
           (p, Guessed):tt                        --- we guessed last
             -> dpli cls ((negate p, Deduced):tt) --- and guess again!
           _ -> False                             --- unless we can't
     else case unassigned cls trail' of           --- otherwise
           [] -> True   --- it's satisfiable if there are no unassigned literals
           ps -> let (_, p) = Data.List.maximum
                              $ map (frequencies cls') ps
                 in dpli cls ((p, Guessed):trail') --- recur with the next
                                                   --- best guess

Backjumping, Conflict-Driven Clause Learning

The first optimization scheme presents itself: backjumping. The basic problem is we walked too far down the wrong road, but eventually found something important. Our algorithm will exhaustively walk back, until we get back to the right track. That’s a fool’s errand, and a huge waste of time.

Instead, we could jump back immediately with what we’ve got. Well, jump back a few more places than we’d normally allow:

backjump :: Clauses -> Formula -> [Trail] -> [Trail]
backjump cls p trail =
  case backtrack trail of
   (q, Guessed):tt -> let (cls', trail') = btUnitPropagate (cls, (p,Guessed):tt)
                      in if [] `elem` cls'
                         then backjump cls p tt
                         else trail
   _ -> trail

Then we can add a “Conflict Clause” to the overall formula, which is just negating the conjunction of the decision literals in the trail. This trick (adding conflict clauses to our problem) is called “Learning”.

guessedLiterals :: [Trail] -> [Trail]
guessedLiterals ((p, Guessed):tt) = (p, Guessed):guessedLiterals tt
guessedLiterals ((_, Deduced):tt) = guessedLiterals tt
guessedLiterals [] = []

-- | DPLL with backjumping.
dplb :: Clauses -> [Trail] -> Bool
dplb cls trail =
  let (cls', trail') = btUnitPropagation (cls, trail)
      hasConflicts = ([] `elem`)
  in if [] `elem` cls'                             --- if there are conflicts
     then case backtrack trail of 
           (p, Guessed):tt ->                      --- and we can backtrack 
             let trail'' = backjump cls p tt       --- we use our newfangled
                 declits = guessedLiterals trail'' --- backjumping algorithm!
                 conflict = Set.insert (negate p)
                            (Set.image (negate . fst) declits)
             in dplb (conflict:cls) (Set.insert (negate p, Deduced) trail'')
           _ -> False
     else case unassigned cls trail' of            --- otherwise iterate
           [] -> True                              --- exactly like we did
           ps -> let (_,p) = Data.List.maximum     --- before, recursively
                             $ map (frequencies cls') ps
                 in dplb cls ((p, Guessed):trail')

There is a vast literature on this subject, which I do not think I could even hope to scratch.

Conclusion

We have just introduced the definitional CNF, which is a slicker way to get a formula in conjunctive normal form.

Then we introduced the Davis-Putnam algorithm, which recursively transformed a set of clauses until we ended up with either (i) an empty list of clauses, or (ii) a contradictory clause appeared. In the former case, it terminated with True — the given set of clauses are satisfiable; whereas the latter case clearly resulted in False, the clauses are unsatisfiable.

We then introduced a modified version, tweaking only the third step. This is the DPLL algorithm.

Next time, we’ll move on to first order logic (huzzah). We might have some aside on using Binary Decision Diagrams. As far as I can tell (and I may very well be wrong!), Binary Decision Diagrams just present a new presentation of the same problem, but no “big wins”.

For the sake of completeness, I mention there exists a method called Stålmarck’s method, but won’t examine it because it’s patented…and I’m no lawyer (with my luck, I’ll accidentally break some law, and serve time for learning how things work — only in America!).

References

Definitional CNF

Davis-Putnam Algorithm

Changelog

Mar 8, 2015: Fixed typos.

Feb 27, 2015: Added some more explanation in the comments.

Feb 15, 2015: Initial version.