Simple Solver for Boolean Satisfiability

This module implements the Davis-Putnam-Logemann-Loveland (DPLL) algorithm that computes satisfying assignments for Boolean formulas. It is written in a way that supports the use of Pandoc for rendering.


> {-# OPTIONS_GHC -XTypeFamilies #-}
>
> module Control.Monad.Constraint.Boolean (
>
> Boolean, booleanVar, true, false, neg,
> (.&&.), (.||.), (.==>.), (.<==.), (.==.), (./=.),
>
> DPLL, guardB, substitution
>
> ) where
>
> import Data.List ( partition, sortBy )
> import Data.Maybe ( mapMaybe, fromJust )
>
> import Control.Monad.State
> import Control.Monad.Writer
> import Control.Monad.Constraint
>
> infixr 4 .==>., .<==., .==., ./=.
> infixr 3 .&&.
> infixr 2 .||.

Boolean Formulas and Partial Evaluation

Boolean values are parameterized over the type of variable names.


> data Boolean v
> = Var v | Yes | No
> | Not (Boolean v)
> | Boolean v :&&: Boolean v
> | Boolean v :||: Boolean v
> deriving (Eq, Show)

Apart from variables, we define the primitive booleans Yes and No (to avoid a name clash with Prelude.True and Prelude.False) and compound booleans, viz., for negation, conjunction and disjunction.


> evalPrim :: Boolean v -> Boolean v
> evalPrim = asLongAsPossible elim
> where
> elim (Not Yes) = Just No
> elim (Not No) = Just Yes
> elim (No :&&: _) = Just No
> elim (Yes :&&: x) = Just x
> elim (_ :&&: No) = Just No
> elim (x :&&: Yes) = Just x
> elim (Yes :||: _) = Just Yes
> elim (No :||: x) = Just x
> elim (_ :||: Yes) = Just Yes
> elim (x :||: No) = Just x
> elim _ = Nothing

We can partially evaluate formulas by eliminating primitive booleans (i.e. Yes and No) from compound formulas. The result after this step will be a primive boolean or a compound formula without primitive booleans.

The function makes use of an auxiliary function that applies a given transformation as long as it does not yield Nothing everywhere in a Boolean formula. The given transformation will yield Nothing on every subexpression of the result.


> asLongAsPossible :: (Boolean v -> Maybe (Boolean v)) -> Boolean v -> Boolean v
> asLongAsPossible f = everywhere g
> where g x = maybe x (everywhere g) (f x)
>
> everywhere :: (Boolean v -> Boolean v) -> Boolean v -> Boolean v
> everywhere f = f . atChildren (everywhere f)
>
> atChildren :: (Boolean v -> Boolean v) -> Boolean v -> Boolean v
> atChildren f (Not x) = Not (f x)
> atChildren f (x:&&:y) = f x :&&: f y
> atChildren f (x:||:y) = f x :||: f y
> atChildren _ x = x

Conversion to CNF

As the DPLL algorithm expects Boolean formulas in conjunctive normal form (CNF), we need to transform arbitrary formulas into a conjunction of disjunctions of literals.


> type CNF v = Conjunction (Clause v)
> type Clause v = Disjunction (Literal v)
> type Conjunction a = PQ a
> type Disjunction a = [a]
> data Literal v = Pos v | Neg v
> deriving (Eq, Show)
>
> litVar :: Literal v -> v
> litVar (Pos x) = x
> litVar (Neg x) = x
>
> inv :: Literal v -> Literal v
> inv (Pos x) = Neg x
> inv (Neg x) = Pos x
>
> isPos :: Literal v -> Bool
> isPos (Pos _) = True
> isPos _ = False
>
> insertClause :: Clause v -> CNF v -> CNF v
> insertClause clause = insertQ (length clause) clause
>
> singleClause :: Clause v -> CNF v
> singleClause clause = singletonQ (length clause) clause
>
> cnf :: Eq v => Boolean v -> CNF v
> cnf Yes = EmptyQ
> cnf No = singleClause []
> cnf formula
> = mergeQs
> . map (singleClause . map literal . flatDisjunction)
> . flatConjunction
> . asLongAsPossible distribute
> . asLongAsPossible pushNots
> $ formula
> where
> pushNots (Not (Not x)) = Just x
> pushNots (Not (x:&&:y)) = Just (Not x :||: Not y)
> pushNots (Not (x:||:y)) = Just (Not x :&&: Not y)
> pushNots _ = Nothing
>
> distribute (x:||:(y:&&:z)) = Just ((x:||:y):&&:(x:||:z))
> distribute ((x:&&:y):||:z) = Just ((x:||:z):&&:(y:||:z))
> distribute _ = Nothing
>
> literal (Var x) = Pos x
> literal (Not (Var x)) = Neg x

First, we push down negations to variables according to de-Morgan's rules and then use distributivity to eliminate disjunctions of conjunctions. Finally, we flatten conjunctions and disjunctions and use literal notation for variables and negated variables.

The following two functions flatten conjunctions and disjunctions.


> flatConjunction :: Boolean v -> [Boolean v]
> flatConjunction b = flat b []
> where flat (x:&&:y) = flat x . flat y
> flat x = (x:)
>
> flatDisjunction :: Boolean v -> [Boolean v]
> flatDisjunction b = flat b []
> where flat (x:||:y) = flat x . flat y
> flat x = (x:)

The Constraint Store

Now we are ready to define a constraint store for Boolean constraints. Unlike the original formulation of the DPLL algorithm, we are not restricted to backtracking but can search in an arbitrary instance of MonadPlus. We obtain backtracking if we use the list monad. Usually, backtracking is sufficient, because the search space is finite if we only consider Boolean formulas. However, if we want to combine the solver for Boolean constraints with another solver with a possibly infinite search space then we should resort to a fair search algorithm in order to obtain all possible solutions.


> newtype DPLL (m :: * -> *) v = DPLL (CNF v)
>
> instance (MonadPlus m, Eq v) => CStore (DPLL m v)
> where
> type Constraint (DPLL m v) = Boolean v
> type Solver (DPLL m v) = WriterT [(v,Bool)] m
>
> noConstraints = DPLL EmptyQ
> assert formula = liftDPLL (updCNF formula)
> labeling = liftDPLL solveCNF
>
> liftDPLL action = do
> DPLL clauses <- get
> newClauses <- lift (action clauses)
> put (DPLL newClauses)

The constraint store for implementing the DPLL algorithm processes constraints of type Boolean v for some variable representation v that supports an equality check. During constraint solving we want to compute satisfying substitutions and we use the writer monad transformer to do so in the background.

The operations assert and labeling simply lift corresponding operations that are defined in the following.


> updCNF :: (MonadPlus m, Eq v)
> => Boolean v -> CNF v -> WriterT [(v,Bool)] m (CNF v)
> updCNF formula clauses = propDet (mergeQ (cnf (evalPrim formula)) clauses)

In order to add a Boolean formula to the constraint store, we convert it to CNF, add the resulting clauses to the store and propagate deterministic information in the constraint store.

The DPLL algorithm employs two different operations to propagate deterministic information:

Unit propagation looks for clauses that contain only a single literal, deterministically assigns a value to the corresponding variable and propagates this information to the other clauses.

Pure literal assignment looks for variables that occur either always positive or always negative and deterministically assign them a value. For example, if a variable occurs always positive, it is assigned the value true and all clauses that contain it are eliminated. However, there might also be solutions if we assign the value false. For example, in the following formula both variables occur always positive:

Var 'x' :||: Var 'y'

However, the formula is still satisfiable, if we assign false to either of the variables. In order to obtain all possible solutions, we do not assign pure literals.

Unit Propagation

When it is possible to propagate deterministic information, the we do so even when asserting constraints -- not only when solving them.


> propDet :: (MonadPlus m, Eq v) => CNF v -> WriterT [(v,Bool)] m (CNF v)
> propDet EmptyQ = return EmptyQ
> propDet clauses = do
> let (n,c) = headQ clauses
> guard (n>0)
> if n == 1 then propagate (head c) clauses >>= propDet
> else return clauses
>
> propagate :: (MonadPlus m, Eq v)
> => Literal v -> CNF v -> WriterT [(v,Bool)] m (CNF v)
> propagate lit clauses = do
> tell [(litVar lit, isPos lit)]
> return (foldQ prop clauses)
> where
> prop c | lit `elem` c = id
> | otherwise = insertClause (filter (inv lit/=) c)

To eliminate a literal, we eliminate all clauses that contain it and eliminate all inverse occurrences from the remaining clauses.

After propagating deterministic information, we need to perform search.


> solveCNF :: (MonadPlus m, Eq v) => CNF v -> WriterT [(v,Bool)] m (CNF v)
> solveCNF EmptyQ = return EmptyQ
> solveCNF clauses = do
> let var = selectBranchVar clauses
> proceed (Pos var) `mplus` proceed (Neg var)
> where
> proceed lit = propagate lit clauses >>= propDet >>= solveCNF

We choose a variable, split the search space by assigning it true or false non-deterministically, propagate this binding, simplify the resulting clauses by propagating unit literals, and continue to solve the remaining clauses.


> selectBranchVar :: Eq v => CNF v -> v
> selectBranchVar clauses
> = fst . head
> . sortBy (\ (_,n) (_,m) -> compare m n)
> $ foldr count [] vars
> where
> (n,c):ncs = queueToList clauses
> vars = map litVar (c ++ concatMap snd (takeWhile ((n==).fst) ncs))
>
> count x [] = [(x,1)]
> count x ((y,n):yns)
> | x == y = (y,n+1) : yns
> | otherwise = (y,n) : count x yns

We choose a variable that occurs most frequently in the shortest clauses hoping to produce many unit clauses.


> guardB :: (MonadPlus m, Eq v) => Boolean v -> Constr (DPLL m v) ()
> guardB = guardC
>
> substitution :: (MonadPlus m, Eq v) => Boolean v -> m [(v,Bool)]
> substitution formula = execWriterT $
> evalStateT (solution (guardB formula) >> labeling) noConstraints

Finally, we define a specialized version of the guardC function and use it to compute satisfying substitutions for Boolean formulas in an arbitrary instance of MonadPlus.

Syntactic Sugar

We define auxiliary functions for constructing Boolean expressions in order to be able to make the data type abstract.


> booleanVar :: v -> Boolean v
> booleanVar x = Var x
>
> true, false :: Boolean v
> true = Yes; false = No
>
> neg :: Boolean v -> Boolean v
> neg x = Not x
>
> (.&&.), (.||.) :: Boolean v -> Boolean v -> Boolean v
>
> (.&&.) = (:&&:); (.||.) = (:||:)

We also define shortcuts for other Boolean operators.


> (.==>.), (.<==.), (.==.), (./=.) :: Boolean v -> Boolean v -> Boolean v
>
> x .==>. y = neg x .||. y
> x .<==. y = y .==>. x
> x .==. y = x .==>. y .&&. y .==>. x
> x ./=. y = (x .||. y) .&&. (neg x .||. neg y)

Priority Queues

We store clauses in a priority queue implemented as pairing heaps (cf. Okasaki) in order to be able to choose the shortest clause efficiently.


> data PQ a = EmptyQ | PQ Int a [PQ a]
>
> headQ :: PQ a -> (Int,a)
> headQ (PQ n x _) = (n,x)
>
> singletonQ :: Int -> a -> PQ a
> singletonQ n x = PQ n x []
>
> insertQ :: Int -> a -> PQ a -> PQ a
> insertQ n x = mergeQ (singletonQ n x)
>
> mergeQ :: PQ a -> PQ a -> PQ a
> mergeQ EmptyQ q = q; mergeQ q EmptyQ = q
> mergeQ p q | key p <= key q = join p q
> | otherwise = join q p
> where
> key (PQ n _ _) = n
> join (PQ n x qs) q = PQ n x (q:qs)
>
> queueFromList :: (a -> Int) -> [a] -> PQ a
> queueFromList priority = mergeQs . map (\x -> singletonQ (priority x) x)
>
> queueToList :: PQ a -> [(Int,a)]
> queueToList EmptyQ = []
> queueToList (PQ n x qs) = (n,x) : queueToList (mergeQs qs)
>
> mergeQs :: [PQ a] -> PQ a
> mergeQs [] = EmptyQ
> mergeQs [q] = q
> mergeQs (p:q:qs) = mergeQ (mergeQ p q) (mergeQs qs)
>
> foldQ :: (a -> PQ a -> PQ a) -> PQ a -> PQ a
> foldQ _ EmptyQ = EmptyQ
> foldQ cons (PQ _ x qs) = cons x (mergeQs (map (foldQ cons) qs))