Re: [Haskell-cafe] Unit propagation
How can I create he function propagateUnits by just using this 2 functions and recursion? remove :: (Eq a) -a -[a] -[a] -This function removes an item from a list. assignModel :: Model - Formula - Formula -This function applies the assign function for all the assignments of a given model. -- View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3387910.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unit propagation
That look compicatedI 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 typealso 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unit propagation
any other advice? -- View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3386915.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Unit propagation
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 -- View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3384635.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unit propagation
On Mon, Feb 14, 2011 at 7:43 AM, PatrickM patrickm7...@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) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
