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