PROBLEM 4 (Challenge): Your final task is to determine, given an arbitrary formula *in DNF*, whether that formula is satisfiable. That is to say, you are trying to determine whether there is an assignment of truth values to the propositional variables that makes the formula true. To represent the result of your function, we introduce a new datatype `Sat`. A `Sat` value can either be `Sat g`, for some list of pairs `g`, if the formula is satisfiable, or `Unsat` if the formula is unsatisfiable. For example, given the formula (A /\ ~B) \/ (B /\ ~B), your function should return `Sat [("A", True), ("B", False)]`. Or, given the formula (A /\ ~A) \/ (B /\ ~B), your function should return `Unsat`. -------------------------------------------------------------------------------} data Sat = Sat [(String, Bool)] | Unsat deriving (Show) sat :: Formula -> Sat sat = error "sat not implemented" satTests = TestList [ satisfiable (dnf (And (Var "A") (Or (Not (Var "A")) (And (Not (Var "B")) (Var "C"))))) , unsatisfiable (dnf (And (Var "A") (Or (Not (Var "A")) (And (Not (Var "A")) (Var "B"))))) ] where satisfiable phi = showFormula phi ~: case sat phi of Unsat -> assertFailure "should be satisfiable" Sat g -> eval g phi @? "unsatisfying assignment" unsatisfiable phi = showFormula phi ~: case sat phi of Unsat -> return () Sat _ -> assertFailure "show be unsatisfiable" allTests = TestList [evalTests, nnfTests, dnfTests] check = runTestTT allTests