[Haskell-cafe] Unit propagation

[PatrickM]

That look compicated....I have a couple of functions at my disposal
remove :: (Eq a) )a ->[a] ->[a] 
-This function removes an item from a list.

 neg :: Literal->Literal
-This function flips a literal (ie. from P to :P and from :P to P).
falseClause :: Model -> Clause -> Bool 
-This function takes a Model and a Clause and returns True
if the clause is unsatisfied by the model or False otherwise.
falseClauses :: Formula -> Model -> [Clause]
-This function takes a Formula and a Model and returns the list of clauses
of the  formula that are not satisfied.
 assignModel :: Model -> Formula -> Formula 
 -This function applies the assign function for all the assignments of a
given model.
 checkFormula :: Formula -> Maybe Bool This function checks whether a
formula can be  decided to be satisfiable or unsatisfiable based on the
effects of the assign function.
 satisfies :: Model -> Formula -. Bool This function checks whether a model
satisfies a formula. This is done with the combination of the assignModel
and checkFormula functions.


I was thinking something similair with this
resFormula ::  Formula  -> Literal  -> Formula 
resFormula f literal = let f' = filter (literal `notElem`) f in -- Get rid
of satisfied clauses
    map (filter (/= (neg literal))) f'    -- Remove negations from clauses
But I can't match the expected type....also I have to choose an atom..
-- 
View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3385699.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.