aima.core.logic.propositional.inference

Class WalkSAT

java.lang.Object

aima.core.logic.propositional.inference.WalkSAT

public class WalkSAT
extends java.lang.Object

Artificial Intelligence A Modern Approach (3rd Edition): page 263.

 
 function WALKSAT(clauses, p, max_flips) returns a satisfying model or failure
   inputs: clauses, a set of clauses in propositional logic
           p, the probability of choosing to do a "random walk" move, typically around 0.5
           max_flips, number of flips allowed before giving up
           
   model <- a random assignment of true/false to the symbols in clauses
   for i = 1 to max_flips do
       if model satisfies clauses then return model
       clause <- a randomly selected clause from clauses that is false in model
       with probability p flip the value in model of a randomly selected symbol from clause
       else flip whichever symbol in clause maximizes the number of satisfied clauses
   return failure
 
 

Figure 7.18 The WALKSAT algorithm for checking satisfiability by randomly flipping the values of variables. Many versions of the algorithm exist.

Author:

Ciaran O'Reilly, Ravi Mohan, Mike Stampone

Constructor Summary

Constructors

Constructor and Description
WalkSAT() Default Constructor.
WalkSAT(java.util.Random random) Constructor.

Method Summary

Modifier and Type	Method and Description
protected void	assertLegalProbability(double p)
protected Model	flipSymbolInClauseMaximizesNumberSatisfiedClauses(Clause clause, java.util.Set<Clause> clauses, Model model)
protected Model	randomAssignmentToSymbolsInClauses(java.util.Set<Clause> clauses)
protected Clause	randomlySelectFalseClause(java.util.Set<Clause> clauses, Model model)
protected PropositionSymbol	randomlySelectSymbolFromClause(Clause clause)
Model	walkSAT(java.util.Set<Clause> clauses, double p, int maxFlips) WALKSAT(clauses, p, max_flips)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

WalkSAT

public WalkSAT()

Default Constructor.

WalkSAT

public WalkSAT(java.util.Random random)

Constructor.

Parameters:

random - the random generator to be used by the algorithm.

Method Detail

walkSAT

public Model walkSAT(java.util.Set<Clause> clauses,
                     double p,
                     int maxFlips)

WALKSAT(clauses, p, max_flips)

Parameters:

clauses - a set of clauses in propositional logic

p - the probability of choosing to do a "random walk" move, typically around 0.5

maxFlips - number of flips allowed before giving up. Note: a value < 0 is interpreted as infinity.

Returns:

a satisfying model or failure (null).

assertLegalProbability

protected void assertLegalProbability(double p)

randomAssignmentToSymbolsInClauses

protected Model randomAssignmentToSymbolsInClauses(java.util.Set<Clause> clauses)

randomlySelectFalseClause

protected Clause randomlySelectFalseClause(java.util.Set<Clause> clauses,
                                           Model model)

randomlySelectSymbolFromClause

protected PropositionSymbol randomlySelectSymbolFromClause(Clause clause)

flipSymbolInClauseMaximizesNumberSatisfiedClauses

protected Model flipSymbolInClauseMaximizesNumberSatisfiedClauses(Clause clause,
                                                                  java.util.Set<Clause> clauses,
                                                                  Model model)