/
WalkSAT.java
192 lines (169 loc) · 5.88 KB
/
WalkSAT.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
package aima.core.logic.propositional.inference;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Random;
import java.util.Set;
import aima.core.logic.propositional.kb.data.Clause;
import aima.core.logic.propositional.kb.data.Model;
import aima.core.logic.propositional.parsing.ast.PropositionSymbol;
/**
* Artificial Intelligence A Modern Approach (3rd Edition): page 263.<br>
* <br>
*
* <pre>
* <code>
* 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
* </code>
* </pre>
*
* 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
* @author Ravi Mohan
* @author Mike Stampone
*/
public class WalkSAT {
/**
* WALKSAT(clauses, p, max_flips)<br>
*
* @param clauses
* a set of clauses in propositional logic
* @param p
* the probability of choosing to do a "random walk" move,
* typically around 0.5
* @param maxFlips
* number of flips allowed before giving up. Note: a value < 0 is
* interpreted as infinity.
*
* @return a satisfying model or failure (null).
*/
public Model walkSAT(Set<Clause> clauses, double p, int maxFlips) {
assertLegalProbability(p);
// model <- a random assignment of true/false to the symbols in clauses
Model model = randomAssignmentToSymbolsInClauses(clauses);
// for i = 1 to max_flips do (Note: maxFlips < 0 means infinity)
for (int i = 0; i < maxFlips || maxFlips < 0; i++) {
// if model satisfies clauses then return model
if (model.satisfies(clauses)) {
return model;
}
// clause <- a randomly selected clause from clauses that is false
// in model
Clause clause = randomlySelectFalseClause(clauses, model);
// with probability p flip the value in model of a randomly selected
// symbol from clause
if (random.nextDouble() < p) {
model = model.flip(randomlySelectSymbolFromClause(clause));
} else {
// else flip whichever symbol in clause maximizes the number of
// satisfied clauses
model = flipSymbolInClauseMaximizesNumberSatisfiedClauses(
clause, clauses, model);
}
}
// return failure
return null;
}
//
// SUPPORTING CODE
//
private Random random = new Random();
/**
* Default Constructor.
*/
public WalkSAT() {
}
/**
* Constructor.
*
* @param random
* the random generator to be used by the algorithm.
*/
public WalkSAT(Random random) {
this.random = random;
}
//
// PROTECTED
//
protected void assertLegalProbability(double p) {
if (p < 0 || p > 1) {
throw new IllegalArgumentException("p is not a legal propbability value [0-1]: "+p);
}
}
protected Model randomAssignmentToSymbolsInClauses(Set<Clause> clauses) {
// Collect the symbols in clauses
Set<PropositionSymbol> symbols = new LinkedHashSet<PropositionSymbol>();
for (Clause c : clauses) {
symbols.addAll(c.getSymbols());
}
// Make initial set of assignments
Map<PropositionSymbol, Boolean> values = new HashMap<PropositionSymbol, Boolean>();
for (PropositionSymbol symbol : symbols) {
// a random assignment of true/false to the symbols in clauses
values.put(symbol, random.nextBoolean());
}
Model result = new Model(values);
return result;
}
protected Clause randomlySelectFalseClause(Set<Clause> clauses, Model model) {
// Collect the clauses that are false in the model
List<Clause> falseClauses = new ArrayList<Clause>();
for (Clause c : clauses) {
if (Boolean.FALSE.equals(model.determineValue(c))) {
falseClauses.add(c);
}
}
// a randomly selected clause from clauses that is false
Clause result = falseClauses.get(random.nextInt(falseClauses.size()));
return result;
}
protected PropositionSymbol randomlySelectSymbolFromClause(Clause clause) {
// all the symbols in clause
Set<PropositionSymbol> symbols = clause.getSymbols();
// a randomly selected symbol from clause
PropositionSymbol result = (new ArrayList<PropositionSymbol>(symbols))
.get(random.nextInt(symbols.size()));
return result;
}
protected Model flipSymbolInClauseMaximizesNumberSatisfiedClauses(
Clause clause, Set<Clause> clauses, Model model) {
Model result = model;
// all the symbols in clause
Set<PropositionSymbol> symbols = clause.getSymbols();
int maxClausesSatisfied = -1;
for (PropositionSymbol symbol : symbols) {
Model flippedModel = result.flip(symbol);
int numberClausesSatisfied = 0;
for (Clause c : clauses) {
if (Boolean.TRUE.equals(flippedModel.determineValue(c))) {
numberClausesSatisfied++;
}
}
// test if this symbol flip is the new maximum
if (numberClausesSatisfied > maxClausesSatisfied) {
result = flippedModel;
maxClausesSatisfied = numberClausesSatisfied;
if (numberClausesSatisfied == clauses.size()) {
// i.e. satisfies all clauses
break; // this is our goal.
}
}
}
return result;
}
}