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.