On Mon, Feb 14, 2011 at 7:43 AM, 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
Your specification is a bit too much a single pass of filter. You need to collect the atomic clauses, and filter those out of the non-atomic clauses using the semantics you specified: To filter out the atomic clauses, you can use:
not_atomic = filter (\not_atomic -> (length not_atomic /= 1)
But you want to collect the atomics and remove their negations (and other things based on the atomics) from not_atomic, so you need at least two filters:
atomic :: [Clause] -> [Clause] filter = (\atomic -> length atomic == 1)
atomic_satisfaction atoms = empty $ intersect (filter (\literal -> (True,
The partition function partition :: (a -> Bool) -> [a] -> ([a], [a]) will construct your list of atomic and non-atomic values for you. At this stage we have removed the unit/atomic clauses. We can now test for unsatisfiability, at least in terms of the atomic clauses:: literal)) atoms) (filter (\literal -> (False, literal)) atoms) You will then want to take the list of atomic values, and apply something like:
filter (\(_, atom) -> atom `elem` (fmap snd atomic))
to each element of each Clause. (where atomic is either the value I defined above, or the the correct value from an application of partition). The function is defined in terms of my understanding of "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)." Putting all of this stuff together will be challenging, and very slow. ;0)