Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improve code quality of DefaultSolver a bit. #254

Merged
merged 1 commit into from
Jul 9, 2020
Merged

Improve code quality of DefaultSolver a bit. #254

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 14 additions & 12 deletions src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,6 @@
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.util.AbstractMap;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.LinkedHashMap;
Expand Down Expand Up @@ -241,7 +240,7 @@ private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd)
}
choiceManager.backjump(backjumpLevel);
if (store.propagate() != null) {
throw oops("Violated NoGood after backtracking.");
throw oops("Violated NoGood after backtracking.");
}
}
return true;
Expand Down Expand Up @@ -300,7 +299,7 @@ private boolean justifyMbtAndBacktrack() {
}
ProgramAnalyzingGrounder analyzingGrounder = (ProgramAnalyzingGrounder) grounder;
// Justify one MBT assigned atom.
Integer atomToJustify = assignment.getBasicAtomAssignedMBT();
int atomToJustify = assignment.getBasicAtomAssignedMBT();
if (LOGGER.isDebugEnabled()) {
LOGGER.debug("Searching for justification of {} / {}", atomToJustify, atomStore.atomToString(atomToJustify));
LOGGER.debug("Assignment is (TRUE part only): {}", translate(assignment.getTrueAssignments()));
Expand Down Expand Up @@ -485,20 +484,26 @@ private boolean ingest(Map<Integer, NoGood> obtained) {
continue;
}

final NoGood learnedNoGood = fixContradiction(entry, conflictCause);
if (learnedNoGood != null) {
noGoodsToAdd.addFirst(new AbstractMap.SimpleEntry<>(grounder.register(learnedNoGood), learnedNoGood));
if (!fixContradiction(entry, conflictCause)) {
return false;
}
}
return true;
}

private NoGood fixContradiction(Map.Entry<Integer, NoGood> noGoodEntry, ConflictCause conflictCause) {
/**
* Attempts to fix a given conflict that arose from adding a nogood.
* @param noGoodEntry the description of the NoGood that caused the conflict.
* @param conflictCause a description of the cause of the conflict.
* @return true if the contradiction could be resolved (by backjumping) and the NoGood was added.
* False otherwise, i.e., iff the program is UNSAT.
*/
private boolean fixContradiction(Map.Entry<Integer, NoGood> noGoodEntry, ConflictCause conflictCause) {
LOGGER.debug("Attempting to fix violation of {} caused by {}", noGoodEntry.getValue(), conflictCause);

GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictFromAddingNoGood(conflictCause.getAntecedent());
if (conflictAnalysisResult == UNSAT) {
return NoGood.UNSAT;
return false;
}
branchingHeuristic.analyzedConflict(conflictAnalysisResult);
if (conflictAnalysisResult.learnedNoGood != null) {
Expand All @@ -510,11 +515,8 @@ private NoGood fixContradiction(Map.Entry<Integer, NoGood> noGoodEntry, Conflict
// If NoGood was learned, add it to the store.
// Note that the learned NoGood may cause further conflicts, since propagation on lower decision levels is lazy,
// hence backtracking once might not be enough to remove the real conflict cause.
if (!addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue(), LBD_NO_VALUE)) {
return NoGood.UNSAT;
}
return addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue(), LBD_NO_VALUE);

return conflictAnalysisResult.learnedNoGood;
}

private boolean choose() {
Expand Down