Haskell procedure

Question

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)) -- This function takess a Clause and return the set of Atoms of that Clause. atomsClause :: Clause -> [Atom] -- This function takes a Formula returns the set of Atoms of a Formula atoms :: Formula -> [Atom] -- This function returns True if the given Literal can be found within -- the Clause. isLiteral :: Literal -> Clause -> Bool -- this function takes a Model and an Atom and flip the truthvalue of -- the atom in the model flipSymbol :: Model -> Atom -> Model -- is this ok? Additional functions : 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. 

Answer 1

One place to get you started: take a look

  removeTautologies :: Formula -> Formula 

Now suppose we can write a function

  isTautology :: Clause -> Bool 

Then we may have the opportunity to use this function to filter general formulas. Therefore, I am trying to ignore everything except the isTautology function. Essentially the question here is: what is a tautology and how do we discover it? Some of the ideas posted by Edward Z. Young should definitely help you understand what's going on. In this case, we could look at the sentence [(True,"A"), (True,"B"), (False,"A")] and try to pass it to isTautology for testing it. Similar to another sentence published by Edward, [(True,"B"), (True,"C"), (True,"A")] .

The trick as a whole is to figure out how to break the functions into smaller components that are easy to write, and then glue these separate parts together with the code to solve the final problem. We decompose removeTautologies , which works with general formulas, into the isTautology helper, which can work on sentences in a formula, and then we try to define removeTautologies through it through some filtering code.

Hope this helps you get started with your problem. This may seem completely inappropriate, but note that the model verification algorithms use more advanced options that confirm the correctness of your processor, that the protocols behave, and are also recently used in automatic refactoring, see http: //coccinelle.lip6 .fr / for use. Thus, this problem is a good way to study serious applicability in the real world!

---

I will edit it here to help you, and not respond in the comments section. You wrote:

 rt ((x, x') : (y, y') : rest) | x' == y' = rt rest | otherwise = (x, x') : rt ((y, y') : rest) 

There are a couple of problems with this approach, as you mentioned. First of all, the game is that your rt function is working on sentences. If this sentence is a tautology, it should be deleted, so it would be better to call it isTautology type mentioned above, or simply simply:

 isRemovableClause :: Clause -> Bool 

The path you take requires you to sort the list in a lexicographic document, and then consider what to do if you have [P, P, not P, Q] for example. Another approach is to set up a search. Let's pretend that

 isRemovableClause ((tv, name) : rest) = ... 

Note that if the value (not tv, name) present in rest , this sentence should be a tautology. Otherwise, we can throw away (tv, name) and look for a tautology in rest .

Moving the focus to removeTautologies , it’s clear that the function can be written using isRemovableClause : The formula is a list of sentences, so we can just go through the list of sentences and delete all those for which isRemovableClause returns true. To do this, a bold solver will use List.filter , a higher order function.

Answer 2

This question is too broad: it might be slightly OK if you focused on one particular function that you need help with, but in fact, in order for us to be effective, you need to give us more than just indicating that the code should: just with that, it's just the “My homework for me” problem.

As I said, I recommend taking the examples that you posted in your descriptions and converting them into your presentation (I assume you are using CNF?). Then you will have something in the lines

 (A v B v -A) ^ (B v C v A) 

becomes

 [[(True,"A"), (True,"B"), (False,"A")], [(True,"B"), (True,"C"), (True,"A")]] 

and then think about what the resulting data type looks like and how you can access it from a strictly computational point of view. Do not worry about performance.