Skip to content

Commit b3d8b89

Browse files
author
ctjoreilly
committed
- Added subsumption elimination capability.
 . Currently will remove subsumed clauses from factors, and the background clauses used by ModelElimination and Resolution based theorem provers. Will in the future extend Resolution based theorem prover to do backward and possibly forward subsumption elimination in order to improve its overall general performance. - Unifier, fixed a defect in how the cascade occurs check was working. - MixedRadixNumber, fixed a minor defect in constructor and added toString() method to help with debugging.
1 parent d21f4cc commit b3d8b89

12 files changed

Lines changed: 700 additions & 52 deletions

‎src/aima/learning/learners/CurrentBestLearner.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
import aima.learning.knowledge.FOLDataSetDomain;
1111
import aima.learning.knowledge.FOLExample;
1212
import aima.learning.knowledge.Hypothesis;
13-
import aima.logic.fol.inference.FOLModelElimination;
13+
import aima.logic.fol.inference.FOLOTTERLikeTheoremProver;
1414
import aima.logic.fol.inference.InferenceResult;
1515
import aima.logic.fol.kb.FOLKnowledgeBase;
1616

@@ -43,7 +43,7 @@ public void train(DataSet ds) {
4343
}
4444

4545
// Setup a KB to be used for learning
46-
kb = new FOLKnowledgeBase(folDSDomain, new FOLModelElimination(1000));
46+
kb = new FOLKnowledgeBase(folDSDomain, new FOLOTTERLikeTheoremProver(1000, false));
4747

4848
CurrentBestLearning cbl = new CurrentBestLearning(folDSDomain, kb);
4949

‎src/aima/logic/fol/SubsumptionElimination.java‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
package aima.logic.fol;
2+
3+
import java.util.ArrayList;
4+
import java.util.HashMap;
5+
import java.util.HashSet;
6+
import java.util.List;
7+
import java.util.Map;
8+
import java.util.Set;
9+
10+
import aima.logic.fol.kb.data.Clause;
11+
12+
/**
13+
* Note: From slide 17.
14+
* http://logic.stanford.edu/classes/cs157/2008/lectures/lecture12.pdf
15+
*
16+
* Relational Subsumption
17+
*
18+
* A relational clause Phi subsumes Psi is and only if there
19+
* is a substitution delta that, when applied to Phi, produces a
20+
* clause Phidelta that is a subset of Psi.
21+
*/
22+
23+
/**
24+
* @author Ciaran O'Reilly
25+
*
26+
*/
27+
public class SubsumptionElimination {
28+
public static Set<Clause> findSubsumedClauses(Set<Clause> clauses) {
29+
Set<Clause> subsumed = new HashSet<Clause>();
30+
31+
// Group the clauses by their # of literals.
32+
// Keep track of the min and max # of literals.
33+
int min = Integer.MAX_VALUE;
34+
int max = 0;
35+
Map<Integer, Set<Clause>> clausesGroupedBySize = new HashMap<Integer, Set<Clause>>();
36+
for (Clause c : clauses) {
37+
int size = c.getNumberLiterals();
38+
if (size < min) {
39+
min = size;
40+
}
41+
if (size > max) {
42+
max = size;
43+
}
44+
Set<Clause> cforsize = clausesGroupedBySize.get(size);
45+
if (null == cforsize) {
46+
cforsize = new HashSet<Clause>();
47+
clausesGroupedBySize.put(size, cforsize);
48+
}
49+
cforsize.add(c);
50+
}
51+
// Check if each smaller clause
52+
// subsumes any of the larger clauses.
53+
for (int i = min; i < max; i++) {
54+
Set<Clause> scs = clausesGroupedBySize.get(i);
55+
// Ensure there are clauses with this # of literals
56+
if (null != scs) {
57+
for (int j = i + 1; j <= max; j++) {
58+
Set<Clause> lcs = clausesGroupedBySize.get(j);
59+
// Ensure there are clauses with this # of literals
60+
if (null != lcs) {
61+
for (Clause sc : scs) {
62+
// Don't bother checking clauses
63+
// that are already subsumed.
64+
if (!subsumed.contains(sc)) {
65+
for (Clause lc : lcs) {
66+
if (!subsumed.contains(lc)) {
67+
if (sc.subsumes(lc)) {
68+
subsumed.add(lc);
69+
}
70+
}
71+
}
72+
}
73+
}
74+
}
75+
}
76+
}
77+
}
78+
79+
return subsumed;
80+
}
81+
}

‎src/aima/logic/fol/Unifier.java‎

Lines changed: 54 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package aima.logic.fol;
22

3+
import java.util.HashSet;
34
import java.util.LinkedHashMap;
45
import java.util.List;
56
import java.util.Map;
@@ -81,12 +82,11 @@ public Map<Variable, Term> unify(FOLNode x, FOLNode y) {
8182
*/
8283
public Map<Variable, Term> unify(FOLNode x, FOLNode y,
8384
Map<Variable, Term> theta) {
84-
8585
// if theta = failure then return failure
8686
if (theta == null) {
8787
return null;
8888
} else if (x.equals(y)) {
89-
// else if x = y the return theta
89+
// else if x = y then return theta
9090
return theta;
9191
} else if (x instanceof Variable) {
9292
// else if VARIABLE?(x) then return UNIVY-VAR(x, y, theta)
@@ -134,30 +134,23 @@ public Map<Variable, Term> unify(List<? extends FOLNode> x,
134134
protected boolean occurCheck(Map<Variable, Term> theta, Variable var,
135135
FOLNode x) {
136136
if (x instanceof Function) {
137-
Set<Variable> vars = _variableCollector
137+
Set<Variable> varsToCheck = _variableCollector
138138
.collectAllVariables((Function) x);
139-
if (vars.contains(var)) {
139+
if (varsToCheck.contains(var)) {
140140
return true;
141141
}
142142

143143
// Now need to check if cascading will cause occurs to happen
144-
// e.g. Loves(SF1(v2),v2) and Loves(v3,SF0(v3))
145-
for (Variable v : theta.keySet()) {
146-
Term t = theta.get(v);
147-
if (t instanceof Function) {
148-
// If a possible occurs problem
149-
// i.e. the term x contains this variable
150-
if (vars.contains(v)) {
151-
// then need to ensure the function this variable
152-
// is to be replaced by does not contain var.
153-
Set<Variable> indirectvars = _variableCollector
154-
.collectAllVariables((Function) t);
155-
if (indirectvars.contains(var)) {
156-
return true;
157-
}
158-
}
159-
}
160-
}
144+
// e.g.
145+
// Loves(SF1(v2),v2)
146+
// Loves(v3,SF0(v3))
147+
// or
148+
// P(v1,SF0(v1),SF0(v1))
149+
// P(v2,SF0(v2),v2 )
150+
// or
151+
// P(v1, F(v2),F(v2),F(v2),v1, F(F(v1)),F(F(F(v1))),v2)
152+
// P(F(v3),v4, v5, v6, F(F(v5)),v4, F(v3), F(F(v5)))
153+
return cascadeOccurCheck(theta, var, varsToCheck, new HashSet<Variable>(varsToCheck));
161154
}
162155
return false;
163156
}
@@ -217,6 +210,46 @@ private String op(FOLNode x) {
217210
private boolean isCompound(FOLNode x) {
218211
return x.isCompound();
219212
}
213+
214+
private boolean cascadeOccurCheck(Map<Variable, Term> theta, Variable var, Set<Variable> varsToCheck, Set<Variable> varsCheckedAlready) {
215+
// Want to check if any of the variable to check end up
216+
// looping back around on the new variable.
217+
Set<Variable> nextLevelToCheck = new HashSet<Variable>();
218+
for (Variable v : varsToCheck) {
219+
Term t = theta.get(v);
220+
if (null == t) {
221+
// Variable may not be a key so skip
222+
continue;
223+
}
224+
if (t.equals(var)) {
225+
// e.g.
226+
// v1=v2
227+
// v2=SFO(v1)
228+
return true;
229+
} else if (t instanceof Function) {
230+
// Need to ensure the function this variable
231+
// is to be replaced by does not contain var.
232+
Set<Variable> indirectvars = _variableCollector
233+
.collectAllVariables((Function) t);
234+
if (indirectvars.contains(var)) {
235+
return true;
236+
} else {
237+
// Determine the next cascade/level
238+
// of variables to check for looping
239+
for (Variable iv : indirectvars) {
240+
if (!varsCheckedAlready.contains(iv)) {
241+
nextLevelToCheck.add(iv);
242+
}
243+
}
244+
}
245+
}
246+
}
247+
if (nextLevelToCheck.size() > 0) {
248+
varsCheckedAlready.addAll(nextLevelToCheck);
249+
return cascadeOccurCheck(theta, var, nextLevelToCheck, varsCheckedAlready);
250+
}
251+
return false;
252+
}
220253

221254
// See:
222255
// http://logic.stanford.edu/classes/cs157/2008/miscellaneous/faq.html#jump165

‎src/aima/logic/fol/inference/FOLModelElimination.java‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import java.util.ArrayList;
44
import java.util.HashMap;
55
import java.util.LinkedHashMap;
6+
import java.util.LinkedHashSet;
67
import java.util.List;
78
import java.util.Map;
89
import java.util.Set;
@@ -13,6 +14,7 @@
1314
import aima.logic.fol.StandardizeApartIndexical;
1415
import aima.logic.fol.StandardizeApartIndexicalFactory;
1516
import aima.logic.fol.SubstVisitor;
17+
import aima.logic.fol.SubsumptionElimination;
1618
import aima.logic.fol.Unifier;
1719
import aima.logic.fol.inference.proof.Proof;
1820
import aima.logic.fol.inference.proof.ProofFinal;
@@ -87,7 +89,9 @@ public InferenceResult ask(FOLKnowledgeBase kb, Sentence aQuery) {
8789
//
8890
// Get the background knowledge - are assuming this is satisfiable
8991
// as using Set of Support strategy.
90-
List<Chain> background = createChainsFromClauses(kb.getAllClauses());
92+
Set<Clause> bgClauses = new LinkedHashSet<Clause>(kb.getAllClauses());
93+
bgClauses.removeAll(SubsumptionElimination.findSubsumedClauses(bgClauses));
94+
List<Chain> background = createChainsFromClauses(bgClauses);
9195

9296
// Collect the information necessary for constructing
9397
// an answer (supports use of answer literals).

‎src/aima/logic/fol/inference/FOLOTTERLikeTheoremProver.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
import java.util.Set;
99

1010
import aima.logic.fol.Connectors;
11+
import aima.logic.fol.SubsumptionElimination;
1112
import aima.logic.fol.inference.otter.ClauseFilter;
1213
import aima.logic.fol.inference.otter.ClauseSimplifier;
1314
import aima.logic.fol.inference.otter.LightestClauseHeuristic;
@@ -163,6 +164,7 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
163164
c.setStandardizedApartCheckNotRequired();
164165
usable.addAll(c.getFactors());
165166
}
167+
usable.removeAll(SubsumptionElimination.findSubsumedClauses(usable));
166168

167169
// Ensure reflexivity axiom is added to usable if using paramodulation.
168170
if (isUseParamodulation()) {

0 commit comments

Comments
 (0)