[Haskell-cafe] Haskell WalkSat algorithm implementation

Mihai Maruseac mihai.maruseac at gmail.com
Mon Jan 31 20:18:43 CET 2011


On Mon, Jan 31, 2011 at 9:11 PM, Manolache Andrei-Ionut <
andressocrates90 at yahoo.com> wrote:

> I need some help if possible with the following problem.....The WalkSat
> algorithm takes a formula, a probability 0 =< p =< 1, and a boundary of
> maximum flips maxflips
> and returns a model that satisfies the formula or failure. The algorithm
> begins by assigning truth values to
> the atoms randomly, ie. generating a random model. Then it proceeds to flip
> the value of an atom from one
> of the unsatisfied clauses until it is able to find a model that satisfies
> the formula or reaches the maximum
> number of flips.
> In order to select which atom from the currently selected clause to flip,
> it follows two strategies:
> 1. Either flip any atom randomly.
> 2. Or flip the atom that maximizes the number of satisfied clauses in the
> formula.
> The choice to flip randomly is followed with probability p.
> 1.atomsClause :: Clause ! [Atom] This function must take a Clause and
> return the set of Atoms of
> that Clause. Note that the set should not contain any duplicates.
> 2. atoms :: Formula![Atom] This function must take a Formula return the set
> of Atoms of a Formula.
> Note that the set should not contain any duplicates.
> 3. isLiteral :: Literal ! Clause ! Bool This function returns True if the
> given Literal can be found
> within the Clause.
> 4. 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've done the first 3 I need some help with the last one, Here is the
> code:
> 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))
>
> atomsClause :: Clause -> [Atom]
> atomsClause = nub . map snd
>
> atoms :: Formula -> [Atom]
> atoms =atomsClause . concat
>
> isLiteral :: Literal -> Clause -> Bool
> isLiteral (b,a) cs = or[x==b && y==a|(x,y)<-cs]
>
> flipSymbol :: Model -> Atom -> Model
> flipSymbol = undefined ---the last one
> Thank you.
>
>
Hi,

I guess that

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

should do the trick.

-- 
Mihai
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110131/b97baa86/attachment-0001.htm>


More information about the Haskell-Cafe mailing list