/
PLResolution.java
220 lines (200 loc) · 7.41 KB
/
PLResolution.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
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
package aima.core.logic.propositional.inference;
import java.util.ArrayList;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;
import aima.core.logic.propositional.kb.KnowledgeBase;
import aima.core.logic.propositional.kb.data.Clause;
import aima.core.logic.propositional.kb.data.Literal;
import aima.core.logic.propositional.parsing.ast.ComplexSentence;
import aima.core.logic.propositional.parsing.ast.Connective;
import aima.core.logic.propositional.parsing.ast.PropositionSymbol;
import aima.core.logic.propositional.parsing.ast.Sentence;
import aima.core.logic.propositional.transformations.ConvertToConjunctionOfClauses;
import aima.core.util.SetOps;
/**
* Artificial Intelligence A Modern Approach (3rd Edition): page 255.<br>
* <br>
*
* <pre>
* <code>
* function PL-RESOLUTION(KB, α) returns true or false
* inputs: KB, the knowledge base, a sentence in propositional logic
* α, the query, a sentence in propositional logic
*
* clauses ← the set of clauses in the CNF representation of KB ∧ ¬α
* new ← {}
* loop do
* for each pair of clauses C<sub>i</sub>, C<sub>j</sub> in clauses do
* resolvents ← PL-RESOLVE(C<sub>i</sub>, C<sub>j</sub>)
* if resolvents contains the empty clause then return true
* new ← new ∪ resolvents
* if new ⊆ clauses then return false
* clauses ← clauses ∪ new
* </code>
* </pre>
*
* Figure 7.12 A simple resolution algorithm for propositional logic. The
* function PL-RESOLVE returns the set of all possible clauses obtained by
* resolving its two inputs.<br>
* <br>
* Note: Optional optimization added to implementation whereby tautological
* clauses can be removed during processing of the algorithm - see pg. 254 of
* AIMA3e:<br>
* <blockquote> Inspection of Figure 7.13 reveals that many resolution steps are
* pointless. For example, the clause B<sub>1,1</sub> ∨ ¬B<sub>1,1</sub>
* ∨ P<sub>1,2</sub> is equivalent to <i>True</i> ∨ P<sub>1,2</sub> which
* is equivalent to <i>True</i>. Deducing that <i>True</i> is true is not very
* helpful. Therefore, any clauses in which two complementary literals appear
* can be discarded. </blockquote>
*
* @see Clause#isTautology()
*
* @author Ciaran O'Reilly
* @author Ravi Mohan
* @author Mike Stampone
* @author Ruediger Lunde
*/
public class PLResolution implements EntailmentChecker {
/**
* PL-RESOLUTION(KB, α)<br>
* A simple resolution algorithm for propositional logic.
*
* @param kb
* the knowledge base, a sentence in propositional logic.
* @param alpha
* the query, a sentence in propositional logic.
* @return true if KB |= α, false otherwise.
*/
public boolean isEntailed(KnowledgeBase kb, Sentence alpha) {
// clauses <- the set of clauses in the CNF representation
// of KB & ~alpha
Set<Clause> clauses = convertKBAndNotAlphaIntoCNF(kb, alpha);
// new <- {}
Set<Clause> newClauses = new LinkedHashSet<>();
// loop do
while (true) {
// for each pair of clauses C_i, C_j in clauses do
List<Clause> clausesList = new ArrayList<>(clauses);
for (int i = 0; i < clausesList.size() - 1; i++) {
Clause ci = clausesList.get(i);
for (int j = i + 1; j < clausesList.size(); j++) {
Clause cj = clausesList.get(j);
// resolvents <- PL-RESOLVE(C_i, C_j)
Set<Clause> resolvents = plResolve(ci, cj);
// if resolvents contains the empty clause then return true
if (resolvents.contains(Clause.EMPTY)) {
return true;
}
// new <- new U resolvents
newClauses.addAll(resolvents);
}
}
// if new is subset of clauses then return false
if (clauses.containsAll(newClauses)) {
return false;
}
// clauses <- clauses U new
clauses.addAll(newClauses);
}
}
/**
* PL-RESOLVE(C<sub>i</sub>, C<sub>j</sub>)<br>
* Calculate the set of all possible clauses by resolving its two inputs.
*
* @param ci
* clause 1
* @param cj
* clause 2
* @return the set of all possible clauses obtained by resolving its two
* inputs.
*/
public Set<Clause> plResolve(Clause ci, Clause cj) {
Set<Clause> resolvents = new LinkedHashSet<>();
// The complementary positive literals from C_i
resolvePositiveWithNegative(ci, cj, resolvents);
// The complementary negative literals from C_i
resolvePositiveWithNegative(cj, ci, resolvents);
return resolvents;
}
//
// SUPPORTING CODE
//
private boolean discardTautologies = true;
/**
* Default constructor, which will set the algorithm to discard tautologies
* by default.
*/
public PLResolution() {
this(true);
}
/**
* Constructor.
*
* @param discardTautologies
* true if the algorithm is to discard tautological clauses
* during processing, false otherwise.
*/
public PLResolution(boolean discardTautologies) {
setDiscardTautologies(discardTautologies);
}
/**
* @return true if the algorithm will discard tautological clauses during
* processing.
*/
public boolean isDiscardTautologies() {
return discardTautologies;
}
/**
* Determine whether or not the algorithm should discard tautological
* clauses during processing.
*/
public void setDiscardTautologies(boolean discardTautologies) {
this.discardTautologies = discardTautologies;
}
protected Set<Clause> convertKBAndNotAlphaIntoCNF(KnowledgeBase kb, Sentence alpha) {
// KB & ~alpha;
Sentence isContradiction = new ComplexSentence(Connective.AND,
kb.asSentence(), new ComplexSentence(Connective.NOT, alpha));
// the set of clauses in the CNF representation
Set<Clause> clauses = new LinkedHashSet<>(
ConvertToConjunctionOfClauses.apply(isContradiction)
.getClauses());
discardTautologies(clauses);
return clauses;
}
protected void resolvePositiveWithNegative(Clause c1, Clause c2,
Set<Clause> resolvents) {
// Calculate the complementary positive literals from c1 with
// the negative literals from c2
Set<PropositionSymbol> complementary = SetOps.intersection(
c1.getPositiveSymbols(), c2.getNegativeSymbols());
// Construct a resolvent clause for each complement found
for (PropositionSymbol complement : complementary) {
List<Literal> resolventLiterals = new ArrayList<>();
// Retrieve the literals from c1 that are not the complement
for (Literal c1l : c1.getLiterals()) {
if (c1l.isNegativeLiteral() || !c1l.getAtomicSentence().equals(complement)) {
resolventLiterals.add(c1l);
}
}
// Retrieve the literals from c2 that are not the complement
for (Literal c2l : c2.getLiterals()) {
if (c2l.isPositiveLiteral() || !c2l.getAtomicSentence().equals(complement)) {
resolventLiterals.add(c2l);
}
}
// Construct the resolvent clause
Clause resolvent = new Clause(resolventLiterals);
// Discard tautological clauses if this optimization is turned on.
if (!(isDiscardTautologies() && resolvent.isTautology())) {
resolvents.add(resolvent);
}
}
}
// Utility routine for removing the tautological clauses from a set (in place).
protected void discardTautologies(Set<Clause> clauses) {
if (isDiscardTautologies())
clauses.removeIf(Clause::isTautology);
}
}