<br><br><div class="gmail_quote">On Mon, Feb 14, 2011 at 7:43 AM, PatrickM <span dir="ltr"><<a href="mailto:patrickm7860@yahoo.co.uk">patrickm7860@yahoo.co.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
This is my last part from a project and I need some help with the following<br>
function:<br>
"If a clause in a propositional formula contains only one literal, then that<br>
literal must be true (so that the<br>
particular clause can be satisfied). When this happens, we remove the unit<br>
clauses (the ones that contain<br>
only one literal), all the clauses where the literal appears and also, from<br>
the remaining clauses, we delete the<br>
negation of the literal (because if P is true, -P will be false).<br>
For example, in the formula (P v Q v R) ^ (-P v Q v-R) ^ (P) we have one<br>
unit clause (the third clause<br>
(P) ). Because this one has to be true for the whole formula to be true we<br>
assign True to P and try to find<br>
a satisfying assignment for the remaining formula. Finally because -P cannot<br>
be true (given the assigned<br>
value of P) then the second clause is reduced by eliminating the symbol -P .<br>
This simplification results in<br>
the revised formula (Q v -R).<br>
The resulting simplification can create other unit clauses. For example in<br>
the formula (-P v Q) ^ (P) is<br>
simplified to (Q) when the unit clause (P) is propagated. This makes (Q) a<br>
unit clause which can now also<br>
be simplified to give a satisfying assignment to the formula. Your function<br>
should apply unit propagation<br>
until it can no longer make any further simplifications.<br>
Note that if both P and -P are unit clauses then the formula is<br>
unsatisfiable. In this case the function"<br>
<br>
type Atom = String<br>
type Literal = (Bool,Atom)<br>
type Clause = [Literal]<br>
type Formula = [Clause]<br>
type Model = [(Atom, Bool)]<br>
type Node = (Formula, ([Atom], Model))<br>
<br>
ropagateUnits :: Formula -> Formula<br>
propagateUnits = filter.something---here I need help<br>
Thanks in advance<br>
<font color="#888888"><br></font></blockquote><div><br></div><div>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:</div>
<div><br></div><div>To filter out the atomic clauses, you can use:</div><div>> not_atomic = filter (\not_atomic -> (length not_atomic /= 1) </div><div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>
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:</div></div><div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>
> atomic :: [Clause] -> [Clause]</div><div>> filter = (\atomic -> length atomic == 1)</div></div><div><br></div><div>The partition function</div><div>partition :: (a -> Bool) -> [a] -> ([a], [a])</div>
<div>will construct your list of atomic and non-atomic values for you.</div><div><br></div><div>At this stage we have removed the unit/atomic clauses. We can now test for unsatisfiability, at least in terms of the atomic clauses::</div>
<div><br></div><div>> atomic_satisfaction atoms = empty $ intersect (filter (\literal -> (True, literal)) atoms) (filter (\literal -> (False, literal)) atoms)</div><div><br></div><div>You will then want to take the list of atomic values, and apply something like:</div>
<div><br></div><div>> filter (\(_, atom) -> atom `elem` (fmap snd atomic))</div><div><br></div><div>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</div>
<div><div><br></div><div>"all the clauses where the literal appears and also, from</div><div>the remaining clauses, we delete the</div><div>negation of the literal (because if P is true, -P will be false)."</div>
</div><div><br></div><div>Putting all of this stuff together will be challenging, and very slow. ;0)</div></div>