[Haskell-cafe] Haskell function help

[Daniel Fischer]

Let me see if I understand that correctly.

On Tuesday 01 February 2011 12:18:06, Houdini wrote:
>  module Algorithm where
>
> import System.Random import Data.Maybe import Data.List
>
> type Atom = String
> type Literal = (Bool,Atom)

(True "P") correspnds to "P", (False, "P") to "not P"?

> type Clause = [Literal]

A Clause is the disjunction of the literals appearing in it?
So [(True,"P"),(False,"Q")] translates to (p || not q) ?

> type Formula = [Clause]

A Formula is the conjunction of its Clauses?
[[(True,"P"),(False,"Q")],[(True,"R")]] translates to
(p || not q) && r ?

> type Model = [(Atom, Bool)]

> type Node = (Formula, ([Atom], Model))

No idea what that would mean

>
> atomsClause :: Clause -> [Atom]
> --This function takess a Clause and return the set of Atoms of that 
Clause.
> atomsClause = nub . map snd
>
> atoms :: Formula -> [Atom]
> atoms = nub . map snd

Doesn't type check, should be

atoms = nub . map snd . concat

> --This function takes a Formula returns the set of Atoms of a Formula
>
> isLiteral :: Literal -> Clause -> Bool
> isLiteral = isLiteral = any . (==)
> --This function returns True if the given Literal can be found within the 
Clause.
>
> flipSymbol :: Model -> Atom -> Model
> flipSymbol m a = map f m
>   where
>     f (atom, value) =
>         if a == atom
>              then (atom, not value) else (atom, value)
> -- this function takes a Model and an Atom and flip the truthvalue of the 
atom in the model
>
> assign :: (Atom,Bool)->Formula->Formula
> assign = undefined--------any advice here? Thank you

You have to find what should happen on
- Literals
- Clauses
- Formulae
(not necessarily in that order)

If the Formula is empty, I suppose nothing should be done,

assign _ [] = []

if there are Clauses,

assign (atom,value) (clause:rest)

should do the assignment in the Clause and depending on the outcome, remove 
the (modified) Clause and assign in the rest, or prepend the modified 
Clause to the result of assigning in the rest,

assign (atom,value) (clause:rest) =
  case assignClause (atom,value) clause of
    Nothing -> assign (atom,value) rest
    Just cl -> cl : assign (atom,value) rest

Now for assigning in a Clause. You get a trivially satisfied Clause, which 
we'll indicate by a Nothing return value, or a reduced Clause (which may be 
empty and hence unsatisfiable).

assignClause :: (Atom,Bool) -> Clause -> Maybe Clause
assignClause (atom,value) clause =
  case partition ((== atom) . snd) clause of
       -- the atom doesn't appear in the clause, nothing to do
    ([],_) -> Just clause
       -- the atom appears in the clause, we have see whether
       -- assigning produces a True or only False
    (ms,cs)
       -- a True, clause is satisfied
       | any (satisfied value) (map fst ms) -> Nothing
       -- all occurrences lead to a False, we have to keep the other 
Literals
       | otherwise -> Just cs

Now, what happens for Literals? We only call this for matching Atoms, so we 
need only care for the Bools. If the Literal has the form (True,p), we get 
value, otherwise we get (not value):

satisfied :: Bool -> Bool -> Bool
satisfied value True = value -- Literal in positive form
staisfied value False = not value -- the Literal was negated

Now we can write satisfied shorter: satisfied = (==)
Or better, now we know what it is supposed to do, remove it altogether and 
make the guard condition in assignClause

     (ms,cs)
       | any (== value) (map fst ms) -> Nothing
       | otherwise -> Just cs