[Haskell-cafe] Unit propagation

[PatrickM]

This is my last part from a  project and I need some help with the following
function:
"If a clause in a propositional formula contains only one literal, then that
literal must be true (so that the
particular clause can be satisfied). When this happens, we remove the unit
clauses (the ones that contain
only one literal), all the clauses where the literal appears and also, from
the remaining clauses, we delete the
negation of the literal (because if P is true, -P will be false).
For example, in the formula (P v Q v R) ^ (-P v Q v-R) ^ (P) we have one
unit clause (the third clause
(P) ). Because this one has to be true for the whole formula to be true we
assign True to P and try to find
a satisfying assignment for the remaining formula. Finally because -P cannot
be true (given the assigned
value of P) then the second clause is reduced by eliminating the symbol -P .
This simplification results in
the revised formula (Q v -R).
The resulting simplification can create other unit clauses. For example in
the formula (-P v Q) ^ (P) is
simplified to (Q) when the unit clause (P) is propagated. This makes (Q) a
unit clause which can now also
be simplified to give a satisfying assignment to the formula. Your function
should apply unit propagation
until it can no longer make any further simplifications.
Note that if both P and -P are unit clauses then the formula is
unsatisfiable. In this case the function"

type Atom = String
type Literal = (Bool,Atom)
type Clause = [Literal]
type Formula = [Clause]
type Model = [(Atom, Bool)]
type Node = (Formula, ([Atom], Model))

ropagateUnits :: Formula -> Formula
propagateUnits   = filter.something---here I need help
             Thanks in advance

-- 
View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3384635.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.