# SAT Solving with the DPLL algorithm

```
-- Advanced Programming
-- by <YOUR NAME HERE> <pennid>
-- and <YOUR PARTNER's NAME> <PARTNER's pennid>
```

```
{-# OPTIONS -Wall -fwarn-tabs -fno-warn-type-defaults -fno-warn-orphans #-}
{-# LANGUAGE FlexibleInstances #-}
```

The Davis-Putnam-Logemann-Loveland algorithm is an algorithm for deciding the satisfiablility of propositional logic formulae. Although the SAT problem is NP-complete, it is stxill remarkably amenable to automation, and modern high-performance SAT-solvers are regularly used in software verification, constraint solving and optimization.

Your task is to implement the DPLL algorithm and verify its correctness using QuickCheck. To complete this problem, you should edit the file Sat.hs.

`module Sat where`

```
import Data.Map (Map) -- use finite map data structure from standard library
import qualified Data.Map as Map
import Test.QuickCheck
```

If you don't have the QuickCheck library installed on your machine, don't forget to

` cabal install quickcheck`

The DPLL algorithm works on formulae that are in Conjunctive Normal Form, i.e. formulae that are a conjunction of clauses, where each clause is a disjunction of literals, i.e. positive or negative propositional variables.

```
-- | An expression in CNF, the conjunction of clauses
newtype CNF = CNF [ Clause ] deriving (Eq, Ord, Show)
unCNF :: CNF -> [ Clause ]
unCNF (CNF cs) = cs
```

```
-- | A clause -- the disjunction of a number of literals
type Clause = [ Lit ]
```

```
-- | A literal, either a positive or negative variable
data Lit = Lit Bool Var deriving (Eq, Ord, Show)
```

```
-- | A variable
data Var = A | B | C | D | E | F | G | H | I | J
deriving (Read, Eq, Ord, Show, Enum, Bounded)
```

```
-- | invert the polarity of a literal
invert :: Lit -> Lit
invert (Lit b x) = Lit (not b) x
```

For example, we can represent the formula `A ^ (B v ~A)`

by:

```
exampleFormula :: CNF
exampleFormula = CNF [[Lit True A],[Lit True B,Lit False A]]
```

This formula is satisfiable as long as `A`

is assigned to `True`

.

```
exampleAssignment :: Map Var Bool
exampleAssignment = Map.fromList [(A, True), (B, True)]
```

Given an assignment for variables, we can determine the truth value of literals. Unassigned variables are assumed to be true.

```
interpLit :: Map Var Bool -> Lit -> Bool
interpLit m (Lit b k) = maybe b (if b then id else not) (Map.lookup k m)
```

We extend this to an interpretation of CNF formulae by ensuring that in all conjunctions, there is at least one literal that is true.

```
interp :: Map Var Bool -> CNF -> Bool
interp m (CNF formula) = all (any (interpLit m)) formula
```

```
prop_interpExample :: Bool
prop_interpExample = interp exampleAssignment exampleFormula
```

The DPLL algorithm takes a formula in conjunctive normal form and produces an assignment for the variables if the formula is satisfiable. Your job is to complete this implementation based on the description of the algorithm on the Wikipedia page. Note that the pseudocode given is fairly imperative. You should think about how to define a *functional* version of the algorithm, based on what we have learned in this course so far.

```
dpll :: CNF -> Maybe (Map Var Bool)
dpll (CNF cnf) = loop initial where
initial :: Solver
initial = undefined cnf
loop :: Solver -> Maybe (Map Var Bool)
loop s = undefined s
```

As a hint, you can think of the main part of the dpll function as executing a loop, where each recursive call of the loop takes as argument the current 'state' of the solver --- the clauses and the current variable assignment.

We can represent this solver state with the following datatype. The record labels give us convenient access to the two components.

```
data Solver = Solver { clauses :: [Clause] , assignment :: (Map Var Bool) }
deriving (Eq, Ord, Show)
```

Part of the action of the loop will be to update that solver state using algorithms for *Unit propagation* and *Pure literal elimination*.

```
-- | If a clause is a unit clause, i.e. it contains only a single
-- unassigned literal, this clause can only be satisfied by assigning
-- the necessary value to make this literal true. Unit propagation updates
-- the map with the assignment and simplifies the clauses to reflect this
-- reasoning.
unitPropagate :: Solver -> Solver
unitPropagate = undefined
```

```
-- | After unit propagation, solver state should contain no more unit
-- clauses.
prop_unitPropagate :: Solver -> Bool
prop_unitPropagate s =
let cs = clauses (unitPropagate s) in
all (\c -> length c /= 1) cs
```

```
-- | If a propositional variable occurs with only one polarity in the
-- formula, it is called pure. Pure literals can always be assigned in
-- a way that makes all clauses containing them true. Thus, these
-- clauses do not constrain the search anymore and can be deleted.
pureLitAssign :: Solver -> Solver
pureLitAssign = undefined
```

```
-- | After pure literal assignment, the solver state should not contain
-- any pure literals
prop_pureLitAssign :: Solver -> Bool
prop_pureLitAssign s =
let cs = clauses (pureLitAssign s) in
all (all (\l -> invert l `elem` concat cs)) cs
```

You will know that you have a correct version when the following property is satisfied by quick check. Note: You should instrument this property (using collect/classify) to make sure that you are testing your solution with meaningful tests.

Remember, though, that even if your assignment passes all of the test cases you should go back and think about code style. Can you improve the assignment? Can you make the code clearer in some way?

```
prop_dpll :: CNF -> Property
prop_dpll c =
case dpll c of
Just m -> property (interp m c)
Nothing -> property True
```

` `

To run quickcheck you will need both the CNF and Solver types to be members of the Arbitrary type class. You may find it useful to add definitions for shrink as well.

```
instance Arbitrary CNF where
arbitrary = undefined
```

```
instance Arbitrary Solver where
arbitrary = undefined
```

Note that you will need more tests / property checks than prop_dpll above. In particular, the properties for unitPropagate and pureLitAssign do not completely characterize those steps----it is possible for buggy implementations to satisfy those properties. You'll need to come up with some additional tests/properties to help you debug your program if it does not satisfy prop_dpll.

```
main :: IO ()
main = do
quickCheck prop_interpExample
quickCheck prop_unitPropagate
quickCheck prop_pureLitAssign
quickCheck prop_dpll
```

## News :

Welcome to CIS 552!

See the home page for basic
information about the course, the schedule for the lecture notes
and assignments, the resources for links to the required software
and online references, and the syllabus for detailed information about
the course policies.