Refactor DefaultSolver

src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java

@@ -158,8 +158,6 @@ default boolean violates(NoGood noGood) {
  */
  int getMBTCount();
 
- void backtrack();
-
  /**
  * Grows all internal data structures to accommodate for all atoms known.
  */
@@ -175,10 +173,4 @@ default boolean violates(NoGood noGood) {
  * @return some BasicAtom that is assigned MBT.
  */
  int getBasicAtomAssignedMBT();
-
- /**
- * Assigns all unassigned atoms to FALSE.
- * @return true if any atom was assigned.
- */
- boolean closeUnassignedAtoms();
 }

src/main/java/at/ac/tuwien/kr/alpha/solver/Choice.java

@@ -32,25 +32,37 @@
 
 class Choice {
  private final int atom;
- private final boolean value;
+ private final boolean truthValue;
  private final boolean backtracked;
 
- Choice(int atom, boolean value, boolean backtracked) {
+ Choice(int atom, boolean truthValue, boolean backtracked) {
  this.atom = atom;
- this.value = value;
+ this.truthValue = truthValue;
  this.backtracked = backtracked;
  }
 
  Choice(int literal, boolean backtracked) {
  this(atomOf(literal), isPositive(literal), backtracked);
  }
 
+ /**
+ * Returns the inverse choice to the given one.
+ * @param choice the choice to invert.
+ * @return a new Choice representing the inverse of the given one, or null if the given choice was already backtracked.
+ */
+ public static Choice getInverted(Choice choice) {
+ if (choice.isBacktracked()) {
+ return null;
+ }
+ return new Choice(choice.getAtom(), !choice.getTruthValue(), true);
+ }
+
  public int getAtom() {
  return atom;
  }
 
- public boolean getValue() {
- return value;
+ public boolean getTruthValue() {
+ return truthValue;
  }
 
  public boolean isBacktracked() {
@@ -59,6 +71,6 @@ public boolean isBacktracked() {
 
  @Override
  public String toString() {
- return atom + "=" + (value ? "TRUE" : "FALSE");
+ return atom + "=" + (truthValue ? "TRUE" : "FALSE");
  }
 }

src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceManager.java

@@ -27,14 +27,19 @@
  */
 package at.ac.tuwien.kr.alpha.solver;
 
-import at.ac.tuwien.kr.alpha.common.Assignment;
 import at.ac.tuwien.kr.alpha.common.NoGood;
 import org.apache.commons.lang3.tuple.Pair;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
 import java.util.Map.Entry;
+import java.util.Set;
+import java.util.Stack;
 import java.util.stream.Collectors;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
@@ -87,7 +92,7 @@ NoGood computeEnumeration() {
  int[] enumerationLiterals = new int[choiceStack.size()];
  int enumerationPos = 0;
  for (Choice e : choiceStack) {
- enumerationLiterals[enumerationPos++] = atomToLiteral(e.getAtom(), e.getValue());
+ enumerationLiterals[enumerationPos++] = atomToLiteral(e.getAtom(), e.getTruthValue());
  }
  return new NoGood(enumerationLiterals);
  }
@@ -152,7 +157,7 @@ public void choose(Choice choice) {
  choices++;
  }
 
- if (assignment.choose(choice.getAtom(), choice.getValue()) != null) {
+ if (assignment.choose(choice.getAtom(), choice.getTruthValue()) != null) {
  throw oops("Picked choice is incompatible with current assignment");
  }
  LOGGER.debug("Choice {} is {}@{}", choices, choice, assignment.getDecisionLevel());
@@ -184,49 +189,19 @@ public void backjump(int target) {
  }
 
  /**
- * Fast backtracking will backtrack but not give any information about which choice was backtracked. This is
- * handy in cases where higher level backtracking mechanisms already know what caused the backtracking and what
- * to do next.
- *
- * In order to analyze the choice that was backtracked, use the more expensive {@link #backtrackSlow()}.
+ * Backtracks the last decision level. Backtracks its choice stack as well as the employed {@link NoGoodStore}
+ * followed by a propagation in order to restore consequences from out-of-order literals.
+ * @return the {@link Choice} that was backtracked.
  */
- public void backtrackFast() {
- backtrack();
-
- final Choice choice = choiceStack.pop();
-
- LOGGER.debug("Backtracked (fast) to level {} from choice {}", assignment.getDecisionLevel(), choice);
- }
-
- /**
- * Slow backtracking will take more time, but allow to analyze the {@link Assignment.Entry} corresponding to the
- * choice that is being backtracked. Higher level backtracking mechanisms can use this information to change
- * their plans.
- *
- * @return the assignment entry of the choice being backtracked, or {@code null} if the choice cannot be
- * backtracked any futher (it already is a backtracking choice)
- */
- public Assignment.Entry backtrackSlow() {
- final Choice choice = choiceStack.pop();
- final Assignment.Entry lastChoiceEntry = assignment.get(choice.getAtom());
-
- backtrack();
- LOGGER.debug("Backtracked (slow) to level {} from choice {}", assignment.getDecisionLevel(), choice);
-
- if (choice.isBacktracked()) {
- return null;
- }
-
- return lastChoiceEntry;
- }
-
- /**
- * This method implements the backtracking "core" that will be executed for both slow and fast backtracking.
- * It backtracks the NoGoodStore and recomputes choice points.
- */
- private void backtrack() {
+ public Choice backtrack() {
  store.backtrack();
  backtracks++;
+ Choice choice = choiceStack.pop();
+ if (store.propagate() != null) {
+ throw oops("Violated NoGood after backtracking.");
+ }
+ LOGGER.debug("Backtracked to level {} from choice {}", assignment.getDecisionLevel(), choice);
+ return choice;
  }
 
  void addChoiceInformation(Pair<Map<Integer, Integer>, Map<Integer, Integer>> choiceAtoms, Map<Integer, Set<Integer>> headsToBodies) {