Lab02

Unicode input: type "\varphi" to obtain φ, "\rho" for ρ, and similarly for other mathematical characters.

Imports and utility functions

{-# LANGUAGE UnicodeSyntax, TypeSynonymInstances, FlexibleInstances #-}
import Data.List
import Control.Monad
import Control.Monad.State
import Test.QuickCheck
import System.IO.Unsafe
-- updating a function
update :: Eq a => (a -> b) -> a -> b -> a -> b
update ρ x v = \y -> if x == y then v else ρ y
-- useful for debugging
debug :: Show a => String -> a -> a
debug str x = seq (unsafePerformIO $ do putStr "<"; putStr str; putStr ": "; print x; putStr ">") x
copy = undefined
todo = undefined
1.8s

Syntax

We define an inductive type for formulas of propositional logic.

-- Variable names are just strings
type PropName = String
-- generation of fresh variable names
fresh :: [PropName] -> PropName
fresh vars = head $ filter (not . (`elem` vars)) $ map (("p"++) . show) [0..]
data Formula =
      T
    | F
    | Prop PropName -- atomic formulas
    | Not Formula
    | And Formula Formula
    | Or Formula Formula
    | Implies Formula Formula
    | Iff Formula Formula
    deriving (Eq, Show)
    
p, q, r, s, t :: Formula
p = Prop "p"
q = Prop "q"
r = Prop "r"
s = Prop "s"
t = Prop "t"
0.6s

We define infix versions of some formula constructors:

infixr 8 /\, ∧
(/\) = And
(∧) = And
infixr 5 \/, ∨, ==>
(\/) = Or
(∨) = Or -- input with "\or"
(==>) = Implies
infixr 4 <==>, ⇔
(<==>) = Iff
(⇔) = Iff -- input with "\lr"
0.3s

Random generation of propositional formulas (for testing):

instance Arbitrary Formula where
    arbitrary = sized f where
      
      f 0 = oneof $ map return $ [p, q, r, s, t] ++ [T, F]
      f size = frequency [
        (1, liftM Not (f (size - 1))),
        (4, do
              size' <- choose (0, size - 1)
              conn <- oneof $ map return [And, Or, Implies, Iff]
              left <- f size'
              right <- f $ size - size' - 1
              return $ conn left right)
        ]
        
    shrink (Not φ) = [φ]
    shrink (Or φ ψ) = [φ, ψ]
    shrink (And φ ψ) = [φ, ψ]
    shrink (Implies φ ψ) = [φ, ψ]
    shrink (Iff φ ψ) = [φ, ψ]
    shrink _ = []
0.5s

In the previous episode

Semantics of propositional logic:

type Valuation = PropName -> Bool
eval :: Formula -> Valuation -> Bool
eval T _ = True
eval F _ = False
eval (Prop p) ρ = ρ p
eval (Not φ) ρ = not (eval φ ρ)
eval (And φ ψ) ρ = (eval φ ρ) && (eval ψ ρ)
eval (Or φ ψ) ρ = (eval φ ρ) || (eval ψ ρ)
eval (Implies φ ψ) ρ = not (eval φ ρ) || (eval ψ ρ)
eval (Iff φ ψ) ρ = (phiv && psiv) || (not phiv && not psiv) where
  phiv = eval φ ρ
  psiv = eval ψ ρ
eval _  _ = error "not a propositional formula"
0.3s

Variables appearing in the formula:

variables :: Formula -> [PropName]
variables = nub . go where
  go T = []
  go F = []
  go (Prop p) = [p]
  go (Not φ) = go φ
  go (And φ ψ) = go φ ++ go ψ
  go (Or φ ψ) = go φ ++ go ψ
  go (Implies φ ψ) = go φ ++ go ψ
  go (Iff φ ψ) = go φ ++ go ψ
0.4s

All truth assignments on a given list of variables:

valuations :: [PropName] -> [Valuation]
valuations [] = [undefined]
valuations (x : xs) = concat [[update ϱ x True, update ϱ x False] | ϱ <- valuations xs]
0.4s

A SAT solver based on truth-tables:

type SATSolver = Formula -> Bool
satisfiable :: SATSolver
satisfiable φ = or [eval φ ϱ | ϱ <- valuations (variables φ)]
0.4s

A tautology checker:

tautology :: Formula -> Bool
tautology φ = and [eval φ ρ | ρ <- valuations (variables φ)]
0.3s

Negation normal form:

nnf :: Formula -> Formula
nnf T = T
nnf F = F
nnf r@(Prop p) = r
nnf (Not phi) = case nnf phi of
  T -> F
  F -> T
  Not phi' -> phi'
  Or phi' psi' -> And (nnf (Not phi')) (nnf (Not psi'))
  And phi' psi' -> Or (nnf (Not phi')) (nnf (Not psi'))
  phi' -> Not phi'
nnf (And phi psi) = And (nnf phi) (nnf psi)
nnf (Or phi psi) = Or (nnf phi) (nnf psi)
nnf (Implies phi psi) = Or (nnf (Not phi)) (nnf psi)
nnf (Iff phi psi) = nnf ((φ ==> ψ) ∧ (ψ ==> φ))
nnf _ = error "not a propositional formula"
0.3s

More normal forms

Conjunctive normal form (CNF)

A literal is either a propositional variable, or the negation of a propositional variable:

data Literal = Pos PropName | Neg PropName deriving (Eq, Show, Ord)
literal2var :: Literal -> PropName
literal2var (Pos p) = p
literal2var (Neg p) = p
opposite :: Literal -> Literal
opposite (Pos p) = Neg p
opposite (Neg p) = Pos p
0.4s

A clause is a disjunction of literals. A formula of propositional logic is in conjunctive normal form (CNF) if it is a conjunction of clauses. It is customary to represent CNF formulas as lists of lists of literals:

type CNFClause = [Literal]
type CNF = [CNFClause]
cnf2formula :: CNF -> Formula
cnf2formula [] = T
cnf2formula lss = foldr1 And (map go lss) where
  go [] = F
  go ls = foldr1 Or (map go2 ls)
  go2 (Pos p) = Prop p
  go2 (Neg p) = Not (Prop p)
  
positive_literals :: CNFClause -> [PropName]
positive_literals ls = nub [p | Pos p <- ls]
negative_literals :: CNFClause -> [PropName]
negative_literals ls = nub [p | Neg p <- ls]
literals :: [Literal] -> [PropName]
literals ls = nub $ positive_literals ls ++ negative_literals ls
0.3s

Converting an arbitrary formula to a logically equivalent one in CNF is entirely dual to the DNF translation from the previous lab:

cnf :: Formula -> CNF
cnf = go . nnf where
  go T = []
  go F = [[]]
  go (Prop p) = [[Pos p]]
  go (Not (Prop p)) = [[Neg p]]
  go (φ `And` ψ) = go φ ++ go ψ
  go (φ `Or` ψ) = [as ++ bs | as <- go φ, bs <- go ψ]
0.3s

Tests:

test_cnf :: Formula -> Bool
test_cnf φ = tautology $ φ ⇔ (cnf2formula (cnf φ))
quickCheckWith (stdArgs {maxSize = 18}) test_cnf
1083.0s

Equisatisfiable conjunctive normal form (ECNF) (EXERCISE)

Two propositional formulas are equisatisfiable if they are either both satisfiable, or both unsatisfiable:

equi_satisfiable :: Formula -> Formula -> Bool
equi_satisfiable φ ψ = satisfiable φ == satisfiable ψ
0.3s

Note that 1) if two formulas are logically equivalent, then they are also equisatisfiable, and 2) the other way around is false: For example, inline_formula not implemented and inline_formula not implemented are both satisfiable, and thus they are equisatisfiable, however they clearly are not logically equivalent.

Write a function transforming a propositional formula into an equisatisfiable CNF formula of polynomial size. Fresh variable names can be generated according to the helper function "fresh" defined at the beginning.

ecnf :: Formula -> CNF
ecnf f = todo
ecnf (T ∧ F ∨ T)
0.3s

Tests:

prop_ecnf :: Formula -> Bool
prop_ecnf phi = equi_satisfiable phi (cnf2formula $ ecnf phi)
quickCheckWith (stdArgs {maxSize = 10}) prop_ecnf
0.5s

Davis-Putnam SAT solver

Tautological clauses (EXERCISE)

A SAT clause is tautological if it contains some literal both positively and negatively. Write a function that removes tautological clauses:

remove_tautologies :: CNF -> CNF
remove_tautologies = todo
0.2s

One literal rule (EXERCISE)

A one-literal clause is a clause containing only one literal inline_formula not implemented. If a CNF contains a one-literal clause inline_formula not implemented, say a positive literal inline_formula not implemented, then inline_formula not implemented must necessarily be true in any satisfying assignment (if any exists). Consequently, we can remove all clauses containing inline_formula not implemented positively, and we can remove all occurrences of the opposite literal inline_formula not implemented from all the other clauses. The same idea can be (dually) applied if inline_formula not implemented is a one-literal clause.

Write a function that transforms a given CNF into an equisatisfiable one without one-literal clauses:

one_literal :: CNF -> CNF
one_literal cnf = todo
one_literal
    [[Pos "p"], [Pos "p", Pos "q", Pos "p", Pos "r"], [Neg "q", Pos "r", Neg "p", Neg "r", Neg "p"], [Neg "q", Neg "p"], [Pos "q", Pos "r", Pos "s"], [Neg "p", Pos "p"]]
0.6s

Note: Removing a proposition inline_formula not implemented in this way can generate new one-literal clauses.

Tests:

prop_one_literal :: Bool
prop_one_literal =
  one_literal
    [[Pos "p"], [Pos "p", Pos "q", Pos "p", Pos "r"], [Neg "q", Pos "r", Neg "p", Neg "r", Neg "p"], [Neg "q", Neg "p"], [Pos "q", Pos "r", Pos "s"], [Neg "p", Pos "p"]] ==
    [[Neg "q",Pos "r",Neg "r"],[Neg "q"],[Pos "q",Pos "r",Pos "s"]] &&
  one_literal
    [[Pos "p2"],[Neg "p2",Pos "p"],[Neg "p2",Pos "p1"],[Neg "p",Neg "p1",Pos "p2"],[Neg "p1",Pos "q"],[Neg "p1",Pos "p0"],[Neg "q",Neg "p0",Pos "p1"],[Neg "p0",Pos "s"],[Neg "p0",Neg "p"],[Neg "s",Pos "p",Pos "p0"]] ==
    [[Pos "p"],[Pos "p1"],[Neg "p1",Pos "q"],[Neg "p1",Pos "p0"],[Neg "q",Neg "p0",Pos "p1"],[Neg "p0",Pos "s"],[Neg "p0",Neg "p"],[Neg "s",Pos "p",Pos "p0"]] &&
  one_literal
    [[Pos "q"],[Pos "p0"],[Neg "p0",Pos "s"],[Neg "p0"]] ==
    [[]]
    
quickCheck prop_one_literal
0.4s

Affirmative-negative rule (EXERCISE)

If a literal appears either only positively, or only negatively, then all clauses where it occurs can be removed, preserving satisfiability. Write a function that removes all literals which appear only positively, or only negatively:

affirmative_negative :: CNF -> CNF
affirmative_negative cnf = todo
0.4s

Tests:

prop_affirmative_negative :: Bool
prop_affirmative_negative =
  affirmative_negative [[Pos "p"],[Pos "p1"],[Neg "p1",Pos "q"],[Neg "p1",Pos "p0"],[Neg "q",Neg "p0",Pos "p1"],[Neg "p0",Pos "s"],[Neg "p0",Neg "p"],[Neg "s",Pos "p",Pos "p0"]] ==
    [[Pos "p"],[Pos "p1"],[Neg "p1",Pos "q"],[Neg "p1",Pos "p0"],[Neg "q",Neg "p0",Pos "p1"],[Neg "p0",Pos "s"],[Neg "p0",Neg "p"],[Neg "s",Pos "p",Pos "p0"]] &&
  affirmative_negative [[Pos "p", Pos "q"], [Pos "p", Neg "q"]] ==
  []
    
quickCheck prop_affirmative_negative
0.4s

Resolution (EXERCISE)

After applying all the previous rules, we know that 1) every variable appears positively and negatively, 2) no variable appears both positively and negatively in the same clause, 3) there is at least one clause, and 4) all clauses are nonempty.

We can thus select a variable that appears both positively and negatively (necessarily from different clauses) and perform resolution in all possible ways and remove this variable altogether. Write a function that removes such a variable:

resolution :: CNF -> CNF
resolution cnf = todo
resolution [[Pos "p", Pos "q"],[Neg "p", Neg "q"]]
0.4s

Tests:

prop_resolution :: Bool
prop_resolution = resolution [[Pos "p", Pos "q"],[Neg "p", Neg "q"]] == [[Pos "q", Neg "q"]]
quickCheck prop_resolution
0.3s

Davis-Putnam algorithm (EXERCISE)

By combining the previous steps we obtain the Davis-Putnam satisfiability algorithm: Convert the input formula to ECNF, and then:

  1. If the CNF is empty, then it is satisfiable.

  2. If the CNF contains an empty clause, then it is not satisfiable.

  3. Remove all tautological clauses.

  4. Apply the one-literal rule until it can no longer be applied.

  5. Apply the affirmative-negative rue until it can no longer be applied.

  6. Only when 3., 4., and 5. above can no longer be applied, apply resolution, and start again from the beginning.

dp :: CNF -> Bool
dp cnf = todo
sat_DP :: SATSolver
sat_DP form = dp cnf where
  cnf = ecnf form
0.2s

Tests:

prop_DP :: Formula -> Bool
prop_DP φ = sat_DP φ == satisfiable φ
quickCheckWith (stdArgs {maxSize = 10}) prop_DP
0.3s
stack install QuickCheck
4.9s
Runtimes (2)
Runtime Languages (1)