(*
02157 - Functional Programming
Mandatory assignment 3: Solver for Propositional Logic

Solved by:
Alexander Rosenberg Johansen
s145706


*)

(*
1. You should define a type Prop for propositions so that the following are values of type
Prop:
• A "p" represents the atom p,
• Dis(A "p", A "q") represents the proposition p ∨ q.
• Con(A "p", A "q") represents the proposition p ∧ q.
• Neg(A "p") represents the proposition ¬p.
*)
exception Error of string

type Prop = | A of string
            | Dis of Prop * Prop
            | Con of Prop * Prop
            | Neg of Prop

(*
2. A proposition is in negation normal form if the negation operator just appears as applied
directly to atoms. Write an F# function transforming a proposition into an equivalent
proposition in negation normal form, using the de Morgan laws:

    ¬(a ∧ b) is equivalent to (¬a) ∨ (¬b)
    ¬(a ∨ b) is equivalent to (¬a) ∧ (¬b)

and the law: ¬(¬a) is equivalent to a.
*)
//dml is short for de Morgan laws
let rec dml :Prop -> Prop = function
    | Neg(Con(p1,p2))    -> Dis(dml (Neg(p1)), dml (Neg(p2)))   //dml case: "¬(a ∧ b) is equivalent to (¬a) ∨ (¬b)"
    | Neg(Dis(p1,p2))    -> Con(dml (Neg(p1)), dml (Neg(p2)))   //dml case: "¬(a ∨ b) is equivalent to (¬a) ∧ (¬b)"
    | Neg(Neg(p))        -> dml p                               //dml case: "¬(¬a) is equivalent to a"
    | A(p)               -> A(p)                //Base case
    | Dis(p1,p2)         -> Dis(dml p1, dml p2) //Not a "dml", branching
    | Con(p1,p2)         -> Con(dml p1, dml p2) //Not a "dml", branching
    | Neg(p)             -> Neg(dml p)          //Not a "dml", branching

(*
3. A literal is an atom or the negation of an atom and a basic conjunct is a conjunction
of literals. A proposition is in disjunctive normal form if it is a disjunction of basic
conjuncts. Write an F# function which transforms a proposition in negation normal form
into an equivalent proposition in disjunctive normal form using the distributive laws:

    a ∧ (b ∨ c) is equivalent to (a ∧ b) ∨ (a ∧ c)
    (a ∨ b) ∧ c is equivalent to (a ∧ c) ∨ (b ∧ c)
*)

//dl is short for distributed law
let rec dl :Prop -> Prop = function
  //  |Con(a,Dis(b,c)) -> Dis(Con(dl a,dl b),Con(dl a,dl c))   //dl case: "a ∧ (b ∨ c) is equivalent to (a ∧ b) ∨ (a ∧ c)"
  |Con(a,Dis(b,c)) -> Dis(dl (Con(a,b)), dl (Con(a,c)))
  //  |Con(Dis(a,b),c) -> Dis(Con(dl a,dl c),Con(dl b,dl c))   //dl case: "(a ∨ b) ∧ c is equivalent to (a ∧ c) ∨ (b ∧ c)"
  |Con(Dis(a,b),c) -> Dis(dl (Con(a,c)), dl (Con(b,c)))
    |A(p)               -> A(p)             //Base case
    |Dis(p1,p2)         -> Dis(dl p1,dl p2) //Not a "dl", branching
    |Con(p1,p2)         -> Con(dl p1,dl p2) //Not a "dl", branching
    |Neg(p)             -> Neg(dl p)        //Not a "dl", branching




(*
4. We shall use a set-based representation of formulas in disjunctive normal form. Since
conjunction is commutative, associative and (a ∧ a) is equivalent to a it is convenient to
represent a basic conjunct bc by its set of literals litOf(bc).
Similarly, we represent a disjunctive normal form formula a:

    bc1 ∨ . . . ∨ bcn

by the set

    dnfToSet(a) = {litOf(bc1), . . . , litOf(bcn)}

that we will call the dns set of a.
Write F# declarations for the functions litOf and dnfToSet.
*)

let rec litOf :Prop -> Set<Prop> = function
    |A(p)       -> Set.ofList([A(p)])
    |Neg(A(p))  -> Set.ofList([Neg(A(p))])
    |Con(p1,p2) -> let setP1 = litOf p1
                   let setP2 = litOf p2
                   Set.union setP1 setP2
    |Neg(p)     -> raise (Error("litOf cannot resolve"))  //incomplete Pattern matches
    |Dis(p1,p2) -> raise (Error("litOf cannot resolve")) //incomplete Pattern matches


let rec dnfToSet :Prop -> Set<Set<Prop>> = function
    |Dis(p1,p2)  -> Set.union (dnfToSet(p1))  (dnfToSet(p2))
    |Con(p1,p2)  -> Set.add (litOf (Con(p1,p2))) Set.empty
    |p           -> Set.add (litOf (p)) Set.empty

(*
5. A set of literals ls (and the corresponding basic conjunct) is said to be consistent if it does
not contain both literals p and ¬p for any atom p. Otherwise, ls (and the corresponding
basic conjunct) is said to be inconsistent. An inconsistent basic conjunct yields false
regardless of the truth values assigned to atoms. Removing it from a disjunctive normal
form formula will therefore not change the meaning of that formula.

Declare an F# function isConsistent that checks the consistency of a set of literals.
Declare an F# function removeInconsistent that removes inconsistent literal sets from
a dns set.
*)

let auxIsConsistent :Prop -> Prop = function
    |A(p)       -> Neg(A(p))
    |Neg(p)     -> p
    |p          -> raise (Error("litOf cannot resolve"))

let rec isConsistent :Set<Prop> -> bool = function
    |latSet ->  let comparisonSet = Set.foldBack(fun x set -> if Set.contains (auxIsConsistent x) (Set.remove x latSet) then Set.add x Set.empty else set) latSet Set.empty
                if Set.intersect latSet comparisonSet <> Set.empty then false else true


let removeInconsistent :Set<Set<Prop>> -> Set<Set<Prop>> = function
    |allThemLats -> Set.filter(fun x -> (isConsistent x)) allThemLats



(*
6. A proposition is satisfiable if it is true for some assignment of truth values to the atoms.
A formula in disjunctive normal is satisfiable when one (or more) of its basic conjunctions
are. Therefore, the set of satisfying assignments of a proposition can be derived from the
consistent literal sets of its disjunctive normal form.

Declare an F# function toDNFsets that transforms an arbitrary proposition into a dns set
with just consistent literal sets.

Declare a function impl a b for computing the implication a ⇒ b and a function iff a b
for computing the bi-implication a ⇔ b.
Use toDNFsets to determine the satisfying assignments for the following two formulas:

• ((¬p) ⇒ (¬q)) ⇒ (p ⇒ q)
• ((¬p) ⇒ (¬q)) ⇒ (q ⇒ p)

where p and q are atoms
*)

let toDNFsets :Prop -> Set<Set<Prop>> = function
    |p   -> removeInconsistent (dnfToSet (dl (dml p)))

let impl :Prop*Prop -> Prop = function
    |a,b -> Dis(Neg(a),b)

let iff :Prop*Prop -> Prop = function
    |a,b -> Con(impl(a,b), impl(b,a))

let p = A("p")
let q = A("q")
let negP = Neg(p)
let negQ = Neg(q)

let first1 = impl(negP,negQ)
let first2 = impl(p,q)
let propFirst = impl(first1,first2)
let resFirst = toDNFsets propFirst

let second1 = first1
let second2 = impl(q,p)
let propSecond = impl(second1,second2)
let resSecond = toDNFsets propSecond

(*
8: The satisability problem for propositional logic is an NP-complete problem, and the above
transformation to disjunctive normal form proposition or to a dns set has in the worst case
an exponential running time.
The disjunctive normal form of the following proposition:

(p1 _ q1) ^ (p2 _ q2) ^ 
 
 
 ^ (pn _ qn) (1)

will, for example, have 2n basic conjuncts.
Declare an F# function badProp n that computes the F# representation of (1).
Compute toDNFsets(badProp n) for a small number of cases and check that the resulting
sets indeed have 2**n elements.
*)
let rec badProp :int -> Prop = function
    |1 -> Dis(A("p"+ string 1),A("q" + string 1))
    |n -> Con(Dis(A("p" + string n),A("q" + string n)),badProp(n-1))

let testBadProp = badProp 3
let testDML = dml testBadProp
let testDL = dl testDML
//let testDnfToSets = dnfToSet testDL
//let testRemoveInconsistent = removeInconsistent testDnfToSets
//let testToDNFsets = toDNFsets testBadProp