[Haskell-cafe] Unit propagation

[Alexander Solla]

On Mon, Feb 14, 2011 at 7:43 AM, PatrickM <patrickm7860 at yahoo.co.uk> wrote:

>
> 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)

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::

> atomic_satisfaction atoms  = empty $ intersect (filter (\literal -> (True,
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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110214/edb54679/attachment.htm>