Lab01

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 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
todo :: a
todo = undefined
0.5s

Syntax

We define an inductive type for formulas of first-order logic.

For propositional logic we will only use atomic formulas of the form "Rel RelName []", i.e., zero-ary relations, and no quantifiers. It's convenient to have here a more general definition since later we will use it for first-order logic.

-- propositional variable names are just strings
type PropName = String
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)
0.4s

We introduce a binary operator syntax:

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

Example formulas:

p, q, r, s, t :: Formula
p = Prop "p"
q = Prop "q"
r = Prop "r"
s = Prop "s"
t = Prop "t"
satisfiable_formulas = [
    p ∧ q ∧ s ∧ p,
    T,
    p,
    Not p,
    (p ∨ q ∧ r) ∧ (Not p ∨ Not r),
    (p ∨ q) ∧ (Not p ∨ Not q)
  ]
unsatisfiable_formulas = [
    p ∧ q ∧ s ∧ Not p,
    T ∧ F,
    F,
    (p ∨ q ∧ r) ∧ Not p ∧ Not r,
    (p ⇔ q) ∧ (q ⇔ r) ∧ (r ⇔ s) ∧ (s ⇔ Not p)
  ]
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)
        ]
0.3s

Semantics (EXERCISE)

Define the semantic function for propositional logic. Hint: proceed by structural induction on formulas (ignoring the cases corresponding to quantifiers and relations of >0 arity).

-- truth valuations
type Valuation = PropName -> Bool
-- the evaluation function
eval :: Formula -> Valuation -> Bool
eval T _ = True
eval F _ = todo
eval (Prop p) ρ = todo
eval (Not φ) ρ = not (eval φ ρ)
eval (And φ ψ) ρ = todo
eval (Or φ ψ) ρ = todo
eval (Implies φ ψ) ρ = todo
eval (Iff φ ψ) ρ = todo
eval _  _ = error "not a propositional formula"
0.3s

Tests for the evaluation function:

ρ0 = const True
ρ1 = const False
ρ2 = update ρ0 "p" False
test_eval =
  eval (p ∧ Not p) ρ0 == False &&
  eval (p ∧ Not p) ρ1 == False &&
  eval (p ∨ q) ρ2 == True
quickCheck test_eval
-- check that the eval function is efficient
-- ifformula 3 == Iff (Iff (Iff T T) T) T
ifformula :: Int -> Formula
ifformula 0 = T
ifformula n = Iff (ifformula (n-1)) T
-- this should evaluate within a fraction of second
test_eval2 = eval (ifformula 23) (const True) == True
quickCheck test_eval2
0.7s

Satisfiable formulas

List of variables appearing in a 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 ψ
  go _ = error "not a propositional formula"
0.7s

A trivial SAT solver based on truth tables:

type SATSolver = Formula -> Bool
-- the list of all valuations on a given list of variables
valuations :: [PropName] -> [Valuation]
valuations [] = [undefined]
valuations (x : xs) = concat [[update ρ x True, update ρ x False] | ρ <- valuations xs]
satisfiable :: SATSolver
satisfiable φ = or [eval φ ρ | ρ <- valuations (variables φ)]
0.3s

Tautologies (EXERCISE)

Write a program that checks whether a given input formula is a tautology. Hint: Reduce to satisfiability.

tautology :: Formula -> Bool
tautology φ = todo
0.2s

Normal forms

Negation normal form (EXERCISE)

A formula of propositional logic is in negation normal form (NNF) if the only connectives are true (T), false (F), conjunction (And), disjunction (Or), and negation (Not), and moreover negation is only applied to atomic formulas:

is_nnf :: Formula -> Bool
is_nnf T = True
is_nnf F = True
is_nnf (Prop _) = True
is_nnf (Not (Prop _)) = True
is_nnf (And phi psi) = is_nnf phi && is_nnf psi
is_nnf (Or phi psi) = is_nnf phi && is_nnf psi
is_nnf (Implies phi psi) = False
is_nnf (Iff phi psi) = False
is_nnf (Not _) = False
is_nnf _ = error "not a propositional formula"
quickCheck $
  is_nnf (Not p ∧ (q ∨ (r ∧ s)))  -- NNF example
  && (not $ is_nnf $ Not (p ∨ q)) -- NNF non-example
0.5s

Write a function that turns an arbitrary formula to a logically equivalent one in NNF. What is the complexity of the NNF translation? Hint: Proceed by structural induction on formulas:

  1. express Implies in terms of Not and Or,

  2. express Iff in terms of And, Or, and Not, and

  3. push negation inside the formula with De Morgan's laws.

nnf :: Formula -> Formula
nnf = todo
0.3s

Tests:

prop_nnf :: Formula -> Bool
prop_nnf φ = let ψ = nnf φ in is_nnf ψ && (tautology $ φ ⇔ ψ)
quickCheck prop_nnf
0.4s

Disjunctive normal form (EXERCISE)

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
0.3s

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

type DNFClause = [Literal]
type DNF = [DNFClause]
dnf2formula :: [[Literal]] -> Formula
dnf2formula [] = F
dnf2formula lss = foldr1 Or (map go lss) where
  go [] = T
  go ls = foldr1 And (map go2 ls)
  go2 (Pos p) = Prop p
  go2 (Neg p) = Not (Prop p)
0.2s

Write a function that turns an arbitrary formula to a logically equivalent one in DNF. What is the complexity of the DNF translation? Hint: Convert the formula to NNF first, then proceed by structural induction on NNF formulas (analogy with polynomial multiplication).

dnf :: Formula -> DNF
dnf = todo
0.2s

Tests:

test_dnf :: Formula -> Bool
test_dnf φ = tautology $ φ ⇔ (dnf2formula (dnf φ))
quickCheckWith (stdArgs {maxSize = 18}) test_dnf
0.5s

Conjunctive normal form

The conjunctive normal form (CNF) is entirely dual to the DNF. In the next lab we will see how to convert a propositional formula to an equisatisfiable one in CNF, which is sufficient for SAT solving.

DNF-based SAT solver (EXERCISE)

Write a SAT solver based on the following recipe:

  1. Convert the input formula to DNF.

  2. Find whether there exists a satisfiable clause.

Hint: A clause is satisfiable iff it does not contain the same literal both positively and negatively.

What is the complexity of this SAT solver compared to the one based on truth tables? Is it potentially more efficient on satisfiable or on unsatisfiable instances?

sat_dnf :: SATSolver
sat_dnf = todo
0.2s

Tests:

prop_sat_dnf :: Formula -> Bool
prop_sat_dnf phi = sat_dnf phi == satisfiable phi
quickCheckWith (stdArgs {maxSize = 20}) prop_sat_dnf
test_solver :: SATSolver -> Bool
test_solver solver = and $ map solver satisfiable_formulas ++ map (not . solver) unsatisfiable_formulas
quickCheck (test_solver sat_dnf)
0.6s
stack install QuickCheck
4.9s
Runtimes (2)
Runtime Languages (1)