Skip to content

Commit 3115ba2

Browse files
author
ctjoreilly
committed
- added forward and backward sumbsumption elimination logic to FOLOtterLikeTheorem prover.
- removed subsumption elimination from Clause.getFactors() as best to perform this logic outside. - As FOLOtterLikeTheorem prover will now exhaust its search space more readily, due to using subsumption elimination, the CurrentBestLearner has been updated to take advantage of this. - Cleanep up output of InterenceResultPrinter.
1 parent 4f30b10 commit 3115ba2

File tree

5 files changed

+205
-50
lines changed

5 files changed

+205
-50
lines changed

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,8 @@ public void train(DataSet ds) {
4343
}
4444

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

4849
CurrentBestLearning cbl = new CurrentBestLearning(folDSDomain, kb);
4950

@@ -57,16 +58,15 @@ public String predict(Example e) {
5758
kb.clear();
5859
kb.tell(etp.getDescription());
5960
kb.tell(currentBestHypothesis.getHypothesis());
60-
6161
InferenceResult ir = kb.ask(etp.getClassification());
6262
if (ir.isTrue()) {
63-
prediction = e.targetValue();
64-
} else if (ir.isUnknownDueToTimeout()) {
65-
// If unknown due to timeout then assume
66-
// is true by default, as can't prove
67-
// either way based on known hypothesis,
68-
// facts and available time.
69-
prediction = e.targetValue();
63+
if (trueGoalValue.equals(e.targetValue())) {
64+
prediction = e.targetValue();
65+
}
66+
} else if (ir.isPossiblyFalse() || ir.isUnknownDueToTimeout()) {
67+
if (!trueGoalValue.equals(e.targetValue())) {
68+
prediction = e.targetValue();
69+
}
7070
}
7171
}
7272

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

Lines changed: 117 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
import java.util.ArrayList;
44
import java.util.HashMap;
5+
import java.util.HashSet;
56
import java.util.LinkedHashSet;
67
import java.util.List;
78
import java.util.Map;
@@ -153,8 +154,8 @@ public void setClauseSimplifier(ClauseSimplifier clauseSimplifier) {
153154
//
154155
// START-InferenceProcedure
155156
public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
156-
Set<Clause> sos = new LinkedHashSet<Clause>();
157-
Set<Clause> usable = new LinkedHashSet<Clause>();
157+
Set<Clause> sos = new HashSet<Clause>();
158+
Set<Clause> usable = new HashSet<Clause>();
158159

159160
// Usable set will be the set of clauses in the KB,
160161
// are assuming this is satisfiable as using the
@@ -164,7 +165,6 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
164165
c.setStandardizedApartCheckNotRequired();
165166
usable.addAll(c.getFactors());
166167
}
167-
usable.removeAll(SubsumptionElimination.findSubsumedClauses(usable));
168168

169169
// Ensure reflexivity axiom is added to usable if using paramodulation.
170170
if (isUseParamodulation()) {
@@ -206,14 +206,21 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
206206
}
207207
}
208208

209+
// Ensure all subsumed clauses are removed
210+
usable.removeAll(SubsumptionElimination.findSubsumedClauses(usable));
211+
sos.removeAll(SubsumptionElimination.findSubsumedClauses(sos));
212+
209213
OTTERAnswerHandler ansHandler = new OTTERAnswerHandler(answerLiteral,
210214
answerLiteralVariables, answerClause, maxQueryTime);
211215

212-
return otter(ansHandler, sos, usable);
216+
IndexedClauses idxdClauses = new IndexedClauses(
217+
getLightestClauseHeuristic(), sos, usable);
218+
219+
return otter(ansHandler, idxdClauses, sos, usable);
213220
}
214221

215222
// END-InferenceProcedure
216-
//
223+
//
217224

218225
/**
219226
* <pre>
@@ -223,7 +230,7 @@ public InferenceResult ask(FOLKnowledgeBase KB, Sentence alpha) {
223230
* </pre>
224231
*/
225232
private InferenceResult otter(OTTERAnswerHandler ansHandler,
226-
Set<Clause> sos, Set<Clause> usable) {
233+
IndexedClauses idxdClauses, Set<Clause> sos, Set<Clause> usable) {
227234

228235
getLightestClauseHeuristic().initialSOS(sos);
229236

@@ -234,11 +241,13 @@ private InferenceResult otter(OTTERAnswerHandler ansHandler,
234241
if (null != clause) {
235242
// * move clause from sos to usable
236243
sos.remove(clause);
237-
usable.add(clause);
238244
getLightestClauseHeuristic().removedClauseFromSOS(clause);
245+
usable.add(clause);
239246
// * PROCESS(INFER(clause, usable), sos)
240-
process(ansHandler, infer(clause, usable), sos, usable);
247+
process(ansHandler, idxdClauses, infer(clause, usable), sos,
248+
usable);
241249
}
250+
242251
// * until sos = [] or a refutation has been found
243252
} while (sos.size() != 0 && !ansHandler.isComplete());
244253

@@ -251,7 +260,7 @@ private InferenceResult otter(OTTERAnswerHandler ansHandler,
251260
*/
252261
private Set<Clause> infer(Clause clause, Set<Clause> usable) {
253262
Set<Clause> resultingClauses = new LinkedHashSet<Clause>();
254-
263+
255264
// Remember to resolve with self
256265
Set<Clause> resolvents = clause.binaryResolvents(clause);
257266
for (Clause rc : resolvents) {
@@ -279,8 +288,9 @@ private Set<Clause> infer(Clause clause, Set<Clause> usable) {
279288
}
280289

281290
// procedure PROCESS(clauses, sos)
282-
private void process(OTTERAnswerHandler ansHandler, Set<Clause> clauses,
283-
Set<Clause> sos, Set<Clause> usable) {
291+
private void process(OTTERAnswerHandler ansHandler,
292+
IndexedClauses idxdClauses, Set<Clause> clauses, Set<Clause> sos,
293+
Set<Clause> usable) {
284294

285295
// * for each clause in clauses do
286296
for (Clause clause : clauses) {
@@ -308,14 +318,15 @@ private void process(OTTERAnswerHandler ansHandler, Set<Clause> clauses,
308318
if (!sos.contains(clause) && !usable.contains(clause)) {
309319
for (Clause ac : clause.getFactors()) {
310320
if (!sos.contains(ac) && !usable.contains(ac)) {
311-
sos.add(ac);
312-
getLightestClauseHeuristic().addedClauseToSOS(ac);
321+
idxdClauses.addClause(ac, sos, usable);
322+
323+
// * if clause has one literal then look for unit
324+
// refutation
325+
lookForUnitRefutation(ansHandler, idxdClauses, ac,
326+
sos, usable);
313327
}
314328
}
315329
}
316-
317-
// * if clause has one literal then look for unit refutation
318-
lookForUnitRefutation(ansHandler, clause, sos, usable);
319330
}
320331

321332
if (ansHandler.isComplete()) {
@@ -325,7 +336,8 @@ private void process(OTTERAnswerHandler ansHandler, Set<Clause> clauses,
325336
}
326337

327338
private void lookForUnitRefutation(OTTERAnswerHandler ansHandler,
328-
Clause clause, Set<Clause> sos, Set<Clause> usable) {
339+
IndexedClauses idxdClauses, Clause clause, Set<Clause> sos,
340+
Set<Clause> usable) {
329341

330342
Set<Clause> toCheck = new LinkedHashSet<Clause>();
331343

@@ -362,8 +374,7 @@ private void lookForUnitRefutation(OTTERAnswerHandler ansHandler,
362374
// LightestClauseHeuristic to loop continuously
363375
// on the same pair of objects.
364376
if (!sos.contains(t) && !usable.contains(t)) {
365-
sos.add(t);
366-
getLightestClauseHeuristic().addedClauseToSOS(t);
377+
idxdClauses.addClause(t, sos, usable);
367378
}
368379
}
369380

@@ -374,6 +385,90 @@ private void lookForUnitRefutation(OTTERAnswerHandler ansHandler,
374385
}
375386
}
376387

388+
class IndexedClauses {
389+
private LightestClauseHeuristic lightestClauseHeuristic = null;
390+
// Group the clauses by their # of literals.
391+
private Map<Integer, Set<Clause>> clausesGroupedBySize = new HashMap<Integer, Set<Clause>>();
392+
// Keep track of the min and max # of literals.
393+
private int minNoLiterals = Integer.MAX_VALUE;
394+
private int maxNoLiterals = 0;
395+
396+
public IndexedClauses(LightestClauseHeuristic lightestClauseHeuristic,
397+
Set<Clause> sos, Set<Clause> usable) {
398+
this.lightestClauseHeuristic = lightestClauseHeuristic;
399+
Set<Clause> allClauses = new HashSet<Clause>();
400+
allClauses.addAll(sos);
401+
allClauses.addAll(usable);
402+
for (Clause c : allClauses) {
403+
indexClause(c);
404+
}
405+
}
406+
407+
public void addClause(Clause c, Set<Clause> sos, Set<Clause> usable) {
408+
// Perform forward subsumption elimination
409+
boolean addToSOS = true;
410+
for (int i = minNoLiterals; i < c.getNumberLiterals(); i++) {
411+
Set<Clause> fs = clausesGroupedBySize.get(i);
412+
if (null != fs) {
413+
for (Clause s : fs) {
414+
if (s.subsumes(c)) {
415+
addToSOS = false;
416+
break;
417+
}
418+
}
419+
}
420+
if (!addToSOS) {
421+
break;
422+
}
423+
}
424+
425+
if (addToSOS) {
426+
sos.add(c);
427+
lightestClauseHeuristic.addedClauseToSOS(c);
428+
indexClause(c);
429+
// Perform backward subsumption elimination
430+
Set<Clause> subsumed = new HashSet<Clause>();
431+
for (int i = c.getNumberLiterals() + 1; i <= maxNoLiterals; i++) {
432+
subsumed.clear();
433+
Set<Clause> bs = clausesGroupedBySize.get(i);
434+
if (null != bs) {
435+
for (Clause s : bs) {
436+
if (c.subsumes(s)) {
437+
subsumed.add(s);
438+
if (sos.contains(s)) {
439+
sos.remove(s);
440+
lightestClauseHeuristic
441+
.removedClauseFromSOS(s);
442+
}
443+
usable.remove(s);
444+
}
445+
}
446+
bs.removeAll(subsumed);
447+
}
448+
}
449+
}
450+
}
451+
452+
//
453+
// PRIVATE METHODS
454+
//
455+
private void indexClause(Clause c) {
456+
int size = c.getNumberLiterals();
457+
if (size < minNoLiterals) {
458+
minNoLiterals = size;
459+
}
460+
if (size > maxNoLiterals) {
461+
maxNoLiterals = size;
462+
}
463+
Set<Clause> cforsize = clausesGroupedBySize.get(size);
464+
if (null == cforsize) {
465+
cforsize = new HashSet<Clause>();
466+
clausesGroupedBySize.put(size, cforsize);
467+
}
468+
cforsize.add(c);
469+
}
470+
}
471+
377472
class OTTERAnswerHandler implements InferenceResult {
378473
private Literal answerLiteral = null;
379474
private Set<Variable> answerLiteralVariables = null;
@@ -392,13 +487,13 @@ public OTTERAnswerHandler(Literal answerLiteral,
392487
//
393488
this.finishTime = System.currentTimeMillis() + maxQueryTime;
394489
}
395-
490+
396491
//
397492
// START-InferenceResult
398493
public boolean isPossiblyFalse() {
399494
return !timedOut && proofs.size() == 0;
400495
}
401-
496+
402497
public boolean isTrue() {
403498
return proofs.size() > 0;
404499
}
@@ -488,7 +583,7 @@ public boolean isAnswer(Clause aClause) {
488583
}
489584
if (addNewAnswer) {
490585
proofs.add(new ProofFinal(aClause.getProofStep(),
491-
answerBindings));
586+
answerBindings));
492587
}
493588
isAns = true;
494589
}

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,17 @@ public static String printInferenceResult(InferenceResult ir) {
2020
StringBuilder sb = new StringBuilder();
2121

2222
sb.append("InferenceResult.isTrue=" + ir.isTrue());
23+
sb.append("\n");
2324
sb.append("InferenceResult.isPossiblyFalse=" + ir.isPossiblyFalse());
25+
sb.append("\n");
2426
sb.append("InferenceResult.isUnknownDueToTimeout="
2527
+ ir.isUnknownDueToTimeout());
28+
sb.append("\n");
2629
sb.append("InferenceResult.isPartialResultDueToTimeout="
2730
+ ir.isPartialResultDueToTimeout());
31+
sb.append("\n");
2832
sb.append("InferenceResult.#Proofs=" + ir.getProofs().size());
33+
sb.append("\n");
2934
int proofNo = 0;
3035
for (Proof p : ir.getProofs()) {
3136
proofNo++;

0 commit comments

Comments
 (0)