[Haskell-cafe] Unit propagation
patrickm7860 at yahoo.co.uk
Tue Feb 15 10:08:51 CET 2011
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
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.
More information about the Haskell-Cafe