2 Haskell Questions

Question

I have 2 Question about 2 haskell functions

1. flipSymbol :: Model -> Atom -> Model This function must take a Model and an Atom and flip the truth value of the atom in the model. Now I was thinking of writing this function like this:...

   flipSymbol m a = map f m
     where
     f (atom, value) = if a == atom then (atom, not value) else (atom, value)

   Is there a better way?

2. The second one is a something more complicated and I need some help with it if possible.. In order to check the satisfiability of a formula in a given model we propagate the effects of assigning a truth value to an atom in a formula. Assume an atom to which we assign the value True. The following effects can be applied to the formula:

   • The positive literals have the same True value and, therefore, any clauses that contain them are removed from the formula. This is to indicate that these clauses could be satisfied and hence no longer affect the satisfiability of the formula.
   • The negated literals have a value of False and are, therefore, removed from any clause they are in. This is to indicate that these clauses are still not satisfied and can only be made true by one of the other literals obtaining a value of True. In the case where False is assigned to the atom, the positive literals will now be false and should be removed from their clauses while the negative literals will become true and have their clauses removed from the formula.
     For example, in the formula (P _ Q _ R) ^ (:P _ Q _ :R) ^ (P _ :Q), assume we assign True to P. Then the clauses containing P, ie. (P _ Q _ R) and (P _ :Q) are removed from the formula, whereas :P is removed from any clause it is in, ie. (:P _ Q _ :R). This results in the formula (Q _ :R). On the other hand, if we assign False to P, we then remove (:P _ Q _ :R) from the formula and P from its clauses, thus obtaining (Q _ R) ^ (:Q).
     The overall formula is satisfiable if it can be reduced to the empty list since in this case all the clauses were satisfied. If there is an empty list within the overall formula then that means that a clause was not satisfied and hence the formula can not be satisfied with the assignment that led to this state.
   • assign :: (Atom,Bool) -> Formula -> Formula The assign function should take an (Atom,Bool) pair and a formula and propagate the effects of assigning the given truth value to the atom in the formula as described above.

The code(on which I received help from here also):

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]
atomsClause = undefined 

-- This function  takes a Formula returns the set of Atoms of a Formula
atoms :: Formula -> [Atom]
atoms = nub . map snd 

-- This function returns True if the given Literal can be found within
-- the Clause.
isLiteral :: Literal -> Clause -> Bool
isLiteral = isLiteral = any . (==)

-- 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?
flipSymbol m a = map f m  where
    f (atom, value) = if a == atom
        then (atom, not value)
        else (atom, value) 

assign :: (Atom,Bool) -> Formula -> Formula
assign = undefined --any advice here?

Answer 1

At a glance, I can't see any way to improve your first formula, maybe you may use logical functions instead of a if-then-else, it's faster:

flipSymbol m a = map f m where
    f (atom, value) = (atom, value /= (a == atom))

Notice: /= for Bool is basically xor.

To your last question: The basic idea is to compare the Atoms, incorporate the Bool-values and fiddeling around with logical ops to get your result. Basically, it looks like this:

assign :: (Atom,Bool) -> Formula -> Formula
assign (a,b) = map . (map f) where
  f (x,b) = (x,(x==a)&&b)