CIS 552: Advanced ProgrammingUsing QuickCheck to develop a SAT solver
For this module, please edit the file Sat.hs.
The Davis-Putnam-Logemann-Loveland algorithm is a method for deciding the satisfiability of propositional logic formulae. Although the SAT problem is NP-complete, it is still remarkably amenable to automation, and high-performance SAT-solvers are heavily used in modern software verification, constraint solving, and optimization. Your task in this problem is to implement the DPLL algorithm and check your implementation using QuickCheck.
We'll lead you through the main steps, but if you're not already familiar with the basics of SAT solving you will need to do a little reading about the basic ideas in DPLL.
Throughout, try to use library functions to make your code short and elegant. None of the requested function bodies should take much more than a dozen or so lines. Style counts!
In this problem, we will use two data structures from Haskell's standard library, implementing Finite Sets and Maps. The two import declarations below say: (1) import the type Map from the module Data.Map as an unqualified identifier, so that we can use just Map a b as a type; and (2) import everything else from Data.Map as qualified identifiers, written Map.member, etc.
These two data structures are defined in the containers Haskell package (included with GHC). For a short introduction to these data structures, see the containers tutorial documentation.
We will do the same thing with sets.
We will also make other library functions available.
> import Data.List as List
> import Data.Maybe as Maybe
> import Data.Char as Char
> import Data.SemigroupFinally, import definitions for QuickCheck.
If you don't yet have the QuickCheck library installed on your machine, start by doing this:
cabal v1-install QuickCheckThe DPLL algorithm works on formulae that are in Conjunctive Normal Form (CNF), i.e. formulae that consist of a conjunction of clauses, where each clause is a disjunction of literals, i.e. positive or negative propositional variables. For example,
(A \/ B \/ C) /\ (not A) /\ (not B \/ C)is a CNF formula.
> -- | An expression in CNF (conjunctive normal form) is a conjunction
> -- of clauses. We store these clauses in the conjunction in a list.
> newtype CNF = Conj { clauses :: [Clause] } deriving (Eq, Ord, Show)> -- | A clause is a disjunction of a number of literals, again storing
> -- each literal in a list.
> newtype Clause = Disj { lits :: [Lit] } deriving (Eq, Ord, Show)> -- | A literal is either a positive or a negative variable
> data Lit = Lit Bool Var deriving (Eq, Ord, Show)> -- A few variables for test cases
> vA, vB, vC, vD :: Var
> vA = Var 'A'
> vB = Var 'B'
> vC = Var 'C'
> vD = Var 'D'Here's how the formula from above is represented:
> exampleFormula :: CNF
> exampleFormula = Conj [
> Disj [Lit True vA, Lit True vB, Lit True vC],
> Disj [Lit False vA],
> Disj [Lit False vB, Lit True vC]]The next few operations allow us to work with formulae, clauses, literals and variables.
First observe that clauses will extract the list of clauses from a CNF, and lits will extract the list of literals from a Clause.
CNFs and Clauses also form a monoid:
> instance Semigroup CNF where
> Conj c1 <> Conj c2 = Conj (c1 <> c2)
> instance Monoid CNF where
> mempty = Conj mempty
>
> instance Semigroup Clause where
> Disj c1 <> Disj c2 = Disj (c1 <> c2)
> instance Monoid Clause where
> mempty = Disj memptyVariables are enumerable. However, only the first 26 will print nicely.
> instance Enum Var where
> toEnum i = Var (toEnum (i + fromEnum 'A'))
> fromEnum (Var v) = fromEnum v - fromEnum 'A'Sometimes we need to know about all of the variables that appear in a particular formulae. We can use a finite map structure to calculate this information. (You'll need to refer to the documentation for the Data.Map module to complete this part.)
> -- | The number of times each variable appears in the formula
> countVars :: CNF -> Map Var Int
> countVars = undefined> -- | All of the variables that appear anywhere in the formula, in sorted order
> vars :: CNF -> [Var]
> vars = undefinedHere are two test cases, using the example formula above. Make sure to add a few of your own unit tests, too!
> testCountVars :: Test
> testCountVars = "countVars" ~:
> countVars exampleFormula ~?= Map.fromList [(vA, 2), (vB, 2), (vC, 2)]Of course, most of the testing we will do in this homework will use QuickCheck.
To do that, we need to be able to generate arbitrary formulae. The following generators are parameterized by the number of distinct variables to use. When you are testing solvers below, you'll find that changing this number affects the efficiency of certain solvers and also the distribution of satisfiable random formulae.
> -- | Generate a random CNF with `n` distinct variables.
> genCNF :: Int -> Gen CNF
> genCNF n = Conj <$> listOf (genClause n)We use these generators in our Arbitrary instances.
> instance Arbitrary Var where
> arbitrary = genVar defaultNumVariables
> shrink v | v == vA = []
> | otherwise = [ vA .. pred v ]> instance Arbitrary Lit where
> arbitrary = genLit defaultNumVariables
> shrink (Lit b v) = map (flip Lit v) (shrink b) ++
> map (Lit b) (shrink v)> instance Arbitrary Clause where
> arbitrary = genClause defaultNumVariables
> shrink (Disj l) = [Disj l' | l' <- shrink l]> instance Arbitrary CNF where
> arbitrary = fmap Conj arbitrary
> shrink (Conj x) = [Conj x' | x' <- shrink x]> ---------------------------------------------------------------------
> -- Satisfiable and unsatisfiable formulaeOur example formula is said to be satisfiable because it is possible to find an assignment of truth values to variables -- namely
A |-> False
B |-> True
C |-> True-- that makes the example formula true. On the other hand, this formula
> -- A /\ (not A)
> unSatFormula :: CNF
> unSatFormula = Conj [Disj [Lit True vA], Disj [Lit False vA]]is unsatisfiable because there is no such assignment.
An assignment of truth values to variables is called a valuation. (In logic, valuations usually assign a truth value to all variables of a formula. Here we will do things a little bit differently and define a valuation to be a map from some variables to truth values.)
For instance, the valuation above is represented thus:
> exampleValuation :: Valuation
> exampleValuation = Map.fromList [(vA, False), (vB, True), (vC, True)]We say that a CNF formula is satisfied by a valuation if the valuation makes the formula true.
> litSatisfied :: Valuation -> Lit -> Bool
> litSatisfied a (Lit b v) = Map.member v a && (b == a Map.! v)> satisfiedBy :: CNF -> Valuation -> Bool
> satisfiedBy p a = all (any (litSatisfied a) . lits) (clauses p)Take a moment to look at the definition of satisfiedBy and consider the following two formulae:
This first formula is a conjunction of zero clauses, all of which must be satisfied for the formula to be true. So this formula will be satisfied by any valuation, including the empty one.
On the other hand, anotherUnsatFormula below is the conjunction of a single clause. That clause must be satisfied in order for the whole formula to be true. However, that clause is a disjunction; there must be some true literal in the clause for it to be satisfied, and there isn't. So this formula cannot be satisfied by any valuation.
Let's create a few tests for satisfiedBy. Our example formula is satisfied by the example valuation. (Add a few more tests of formulae and their satisfying valuations to the list below.)
> testSatisfiedBy :: Test
> testSatisfiedBy = "satisfiedBy" ~: TestList
> [ "exampleFormula" ~:
> assertBool "" (exampleFormula `satisfiedBy` exampleValuation)
> , "another example" ~: assertBool "" (error "ADD your own test case here") ]Note that our unsatisfiable formula is not satisfied by ANY valuation. This is a property that we can check with QuickCheck, because we can generate arbitrary valuations.
Valuations support two main operations: extending them with a new binding and checking what is the value of a variable. Please define them using functions from the Data.Map module. (These definitions are short. If the valuation already has a binding for a variable, extend should replace that binding with the new value).
> ---------------------------------------------------------------------------
> -- Simple SAT SolverA solver is a function that finds a satisfying valuations for a given formula (assuming one exists).
We start with a simple combinatorial solver that basically tries all possible valuations and stops whenever it finds a satisfying valuation.
The first step is to implement the makeValuations function that calculates all the valuations for the given variables.
To test your implementation, QuickCheck the following property stating that makeValuations is correct, in the sense that it has the right length (2^n, where n is the number of variables in the set) and all its elements are distinct.
> prop_makeValuations :: CNF -> Bool
> prop_makeValuations p = length valuations == 2 ^ length ss
> && allElementsDistinct valuations
> where
> valuations = makeValuations ss
> ss = vars p> allElementsDistinct :: Eq a => [a] -> Bool
> allElementsDistinct [] = True
> allElementsDistinct (x:xs) = x `notElem` xs
> && allElementsDistinct xsYour first sat solver should now simply search the list of all valuations for one that satisfies the given formula:
To check that it works, QuickCheck the property prop_satResultSound sat0 5, stating that a successful result returned by a sat0 on formulae containing five variables is always a satisfying valuation.
> prop_satResultSound :: Solver -> Int -> Property
> prop_satResultSound solver i =
> forAll (genCNF i) $ \p -> case solver p of
> Just a -> p `satisfiedBy` a
> Nothing -> TrueWARNING: don't QuickCheck this property on sat0 without specifying the number of variables (and that number should be small!)
A solver is also complete if whenever it fails to find a satisfying assignment, then that formula is unsatisfiable. We say that a solver is correct if it is both sound and complete.
> unsatisfiable :: CNF -> Bool
> unsatisfiable p = all (\a -> not (p `satisfiedBy` a))
> (makeValuations (vars p))> prop_satResult :: Solver -> CNF -> Bool
> prop_satResult solver p = case solver p of
> Just a -> p `satisfiedBy` a
> Nothing -> unsatisfiable pThis property will always be expensive to test, so we separate full correctness from soundness.
In the remainder of this section, we will gradually build up to an implementation of DPLL.
The simple solver we have just developed is very inefficient. One reason for this (not the main one, but solving it will set us up for more interesting optimizations later) is that it evaluates the whole formula every time it tries a different valuation. Indeed, we can do much better: once we choose a truth value for a propositional variable, we can simplify the formula to take this choice into account.
For instance, imagine we have the CNF formula
(A \/ not B) /\ (not A \/ B \/ C).If we instantiate A to True, then the formula becomes (True \/ not B) /\ (False \/ B \/ C), which can be simplified to (B \/ C).
Please implement the instantiate function:
Informally, the correctness property for instantiate is that, if s is a formula and v a variable, s should be satisfiable iff either instantiate s v True or instantiate s v False is satisfiable. Use your simple satisfiability checker sat0 to state this formally as a QuickCheck property. Use QuickCheck (in GHCi) to test whether your implementation of instantiate has this property.
Now use instantiate to write a very simple sat solver that, at each step, chooses a variable and recursively tries instantiating it with both True and False. The algorithm should proceed like this:
First, check if the formula is either
satisfied(returning an empty valuation if so) orfalsified(returningNothing). A formula has been satisfied when it is satisfied by the empty valuation (i.e. we have already instantiated enough variables in the formula that the others don't matter.) Alternatively, a formula isfalsifiedwhen, likeanotherUnsatFormula, it contains a clause with an empty disjunction.Otherwise, choose one of the variables in the formula, instantiate it with both
TrueandFalse, and see if either of the resulting formulae are satisfiable. If so, add an appropriate binding for the variable we instantiated to the resultingValuationand return it.
IMPLEMENTATION NOTES:
- Make sure that your definition of
falsifieddoesn't rely on the formula being completely instantiated. It is possible to cut off large parts of the search space by identifying unsatifiable formula as soon as possible. - If your implementation determines that instantiating a variable with, say
Trueproduces a satisfying valuation, make sure that it does not also test whethe instantiating that variable withFalsealso works. You only need to find one valuation and can cut off the search at that point.
To check that it works, QuickCheck the property prop_satResultSound sat1, prop_satResult sat1, plus this one (and any others that you can think of).
The first significant optimization performed by DPLL is simplifying unit clauses. Please see the Wikipedia page on DPLL (linked above) for a general sense of how it should work.
The signature of the unit clause simplifier is this:
It should take a formula, choose a unit clause (or return Nothing if there aren't any), and simplify it, returning the simplified formula together with the variable that was instantiated away in the process and the value that it was given.
This time, let's start by writing down the correctness property for simplifyUnitClause:
> -- 1) If (simplifyUnitClause s) returns Nothing, then there
> -- are no remaining unit clauses in s.
> -- 2) If it returns (Just s'), then s' is satisfiable iff s is.
> prop_simplifyUnitClause :: CNF -> Bool
> prop_simplifyUnitClause = undefinedNow let's implement the simplifier. First, let's just find all the unit clauses in a formula. For example, the unit clauses of
(A \/ not B) /\ (not A) /\ (B) /\ (B \/ C \/ D)are not A and B, while
(A \/ not B) /\ (not A \/ B \/ C)has no unit clauses.
Use QuickCheck to make sure your implementation satisfies the property you wrote.
Next, we can improve the sat1 solver by inserting a new step:
If the formula is either
satisfiedorfalsified, return an appropriate answer as before.(New step) If there are any unit clauses, choose one, simplify it, and call the solver recursively on the simplified formula. If the recursive call returns a satisfying valuation, add a binding for the variable that was eliminated when we simplified the unit clause and return it.
Otherwise, instantiate one of the variables in the formula and recurse, as before.
Please do so:
To check that it works, QuickCheck the property prop_satResultSound sat2, prop_satResult sat2 plus this one:
> ---------------------------------------------------------------------------
> -- Pure literal eliminationThe next (and last) significant optimization is simplifying pure literals. Again, please see the Wikipedia page (linked above) for how this works.
Again, let's write the correctness property first:
> -- 1) If (simplifyPureLiteral s) returns Nothing, then there
> -- are no remaining pure literals in s
> -- 2) If it returns (Just s'), then s' is satisfiable iff s is
> prop_simplifyPureLiteral :: CNF -> Bool
> prop_simplifyPureLiteral = undefinedNow let's write the pure literal simplifier (and QuickCheck it!). For example, the pure literals in the formula
(A \/ B) /\ (not A) /\ (B) /\ (B \/ C \/ not D)are B, C, and not D.
This brings us to the final DPLL algorithm, inserting a new step in sat2:
If the formula is either
satisfiedorfalsified, return an appropriate answer as before.If there are any unit clauses, choose one, simplify it, and call the solver recursively on the simplified formula.
(New step) If there are any pure literals, choose one, simplify it, and call the solver recursively on the simplified formula.
Otherwise, instantiate one of the variables in the formula and recurse, as before.
To check that it works, QuickCheck the property prop_satResultSound dpll, prop_satResultSound dpll, plus this one:
> ------------------------------------------------------------------------------
> -- All the tests in one convenient place:> quickCheckN :: Testable prop => Int -> prop -> IO ()
> quickCheckN n = quickCheckWith $ stdArgs { maxSuccess = n }> main :: IO ()
> main = do
> putStrLn "Unit tests:"
> runTestTT $ TestList [testCountVars, testVars, testSatisfiedBy]
> putStrLn "Quickcheck properties:"
> quickCheckN 500 prop_unSatBy
> quickCheckN 500 $ prop_satResultSound sat0 defaultNumVariables
> quickCheckN 500 $ prop_satResult sat0
> quickCheckN 500 prop_instantiate
> quickCheckN 500 prop_sat1
> quickCheckN 500 $ prop_satResultSound sat1
> quickCheckN 500 $ prop_satResult sat1
> quickCheckN 500 prop_simplifyUnitClause
> quickCheckN 500 prop_sat2
> quickCheckN 500 $ prop_satResultSound sat2
> quickCheckN 500 $ prop_satResult sat2
> quickCheckN 500 prop_simplifyPureLiteral
> quickCheckN 500 prop_dpll
> quickCheckN 500 $ prop_satResultSound dpll
> quickCheckN 500 $ prop_satResult dpll