Re: [Haskell-cafe] Update2
1. Atom: The Atom is the datatype used to describe Atomic Sentences or propositions. These are basically represented as a string. 2. Literal: Literals correspond to either atoms or negations of atoms. In this implementation each literal is represented as a pair consisting of a boolean value, indicating the polarity of the Atom, and the actual Atom. Thus, the literal ‘P’ is represented as (True,P) whereas its negation ‘-P’ as (False,P). 2 3. Clause: A Clause is a disjunction of literals, for example PvQvRv-S. In this implementation this is represented as a list of Literals. So the last clause would be [(True,P), (True,Q), (True,R),(False,S)]. 4. Formula: A Formula is a conjunction of clauses, for example (P vQ)^(RvP v-Q)^(-P v-R). This is the CNF form of a propositional formula. In this implementation this is represented as a list of Clauses, so it is a list of lists of Literals. Our above example formula would be [[(True,P), (True,Q)], [(True,R), (True,P), (False,Q)], [(False, P), (False,P)]]. 5. Model: A (partial) Model is a (partial) assignment of truth values to the Atoms in a Formula. In this implementation this is a list of (Atom, Bool) pairs, ie. the Atoms with their assignments. So in the above example of type Formula if we assigned true to P and false to Q then our model would be [(P, True),(Q, False)] -- View this message in context: http://haskell.1045720.n5.nabble.com/Update2-tp3392490p3392589.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
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
[Haskell-cafe] Haskell Help
I'm writting a function that will remove tautologies from a fomula.The basic idea is that if in a clause, a literal and its negation are found, it means that the clause will be true, regardless of the value finally assigned to that propositional variable.My appoach is to create a function that will remove this but for a clause and map it to the fomula.Of course I have to remove duplicates at the beginning. module Algorithm where import System.Random import Data.Maybe import Data.List type Atom = String type Literal = (Bool,Atom) type Clause = [Literal] type Formula = [Clause] type Model = [(Atom, Bool)] type Node = (Formula, ([Atom], Model)) removeTautologies :: Formula - Formula removeTautologies = map tC.map head.group.sort where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest | otherwise = (vx, x) : rt ((vy, y) : clauses) Now I have problems when I try to give it a formula (for example (A v B v -A) ^ (B v C v A)).Considering that example the first clause contains the literals A and -A. This means that the clause will always be true, in which case it can be simplify the whole set to simply (B v C v A) . But I get the following Loading package old-locale-1.0.0.2 ... linking ... done. Loading package time-1.1.4 ... linking ... done. Loading package random-1.0.0.2 ... linking ... done. [[(True,A),(True,B)*** Exception: Assignment.hs:(165,11)-(166,83): Non-exhaustive patterns in function rt What should I do? -- View this message in context: http://haskell.1045720.n5.nabble.com/Haskell-Help-tp3381647p3381647.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
