diff --git a/.travis.yml b/.travis.yml
index f9d534d9d..f319d099c 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -45,7 +45,7 @@ install:
   - true
 
 script:
-  - ./gradlew build --scan --stacktrace
+  - travis_wait ./gradlew build --scan --stacktrace
 
 after_success:
   - ./gradlew jacocoTestReport coveralls
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java
index 4dcb2e2a1..a355ca45a 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java
@@ -33,6 +33,7 @@
 import at.ac.tuwien.kr.alpha.config.SystemConfig;
 import at.ac.tuwien.kr.alpha.grounder.Grounder;
 import at.ac.tuwien.kr.alpha.grounder.GrounderFactory;
+import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser;
 import at.ac.tuwien.kr.alpha.solver.Solver;
 import at.ac.tuwien.kr.alpha.solver.SolverFactory;
@@ -103,8 +104,12 @@ public Solver prepareSolverFor(Program program, java.util.function.Predicate<Pre
 		String grounderName = this.config.getGrounderName();
 		boolean doDebugChecks = this.config.isDebugInternalChecks();
 
+		GrounderHeuristicsConfiguration grounderHeuristicConfiguration = GrounderHeuristicsConfiguration
+				.getInstance(this.config.getGrounderToleranceConstraints(), this.config.getGrounderToleranceRules());
+		grounderHeuristicConfiguration.setDisableInstanceRemoval(this.config.isDisableInstanceRemoval());
+
 		AtomStore atomStore = new AtomStoreImpl();
-		Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, doDebugChecks);
+		Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, grounderHeuristicConfiguration, doDebugChecks);
 
 		return SolverFactory.getInstance(this.config, atomStore, grounder);
 	}
@@ -117,7 +122,7 @@ public Stream<AnswerSet> solve(Program program, java.util.function.Predicate<Pre
 		Stream<AnswerSet> retVal = this.prepareSolverFor(program, filter).stream();
 		return this.config.isSortAnswerSets() ? retVal.sorted() : retVal;
 	}
-	
+
 	public Stream<AnswerSet> solve(Program program) {
 		return this.solve(program, InputConfig.DEFAULT_FILTER);
 	}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java
index 638696fce..9e3b6ca00 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java
@@ -33,7 +33,8 @@
 import java.util.Iterator;
 import java.util.Set;
 
-import static at.ac.tuwien.kr.alpha.common.Literals.*;
+import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
+import static at.ac.tuwien.kr.alpha.common.Literals.isNegated;
 
 public interface Assignment {
 	Entry get(int atom);
@@ -71,6 +72,13 @@ default ThriceTruth getTruth(int atom) {
 	 */
 	Antecedent getImpliedBy(int atom);
 
+	/**
+	 * Returns the last truth value (i.e., phase) assigned to the atom.
+	 * @param atom the atom
+	 * @return the last truth value.
+	 */
+	boolean getLastValue(int atom);
+
 	/**
 	 * Determines if the given {@code noGood} is undefined in the current assignment.
 	 *
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java
index 6a57c4061..91ac679d3 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2017-2018, the Alpha Team.
+ * Copyright (c) 2017-2019, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -171,6 +171,12 @@ public List<Substitution> getSubstitutions(Substitution partialSubstitution) {
 		extendedSubstitution.put(variable, resultTerm);
 		return Collections.singletonList(extendedSubstitution);
 	}
+	
+	public boolean isLeftOrRightAssigning() {
+		final Term left = getTerms().get(0);
+		final Term right = getTerms().get(1);
+		return isNormalizedEquality && (assignable(left) && right.isGround() || assignable(right) && left.isGround());
+	}
 
 	private Term evaluateTerm(Term term) {
 		// Evaluate arithmetics.
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java
index 6efa8e4b4..063f7c1c6 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java
@@ -107,6 +107,24 @@ public class CommandLineParser {
 			.desc("disable the deletion of (learned, little active) nogoods (default: "
 					+ SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION + ")")
 			.build();
+	private static final Option OPT_GROUNDER_TOLERANCE_CONSTRAINTS = Option.builder("gtc").longOpt("grounderToleranceConstraints")
+			.desc("grounder tolerance for constraints (default: " + SystemConfig.DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS + ")")
+			.hasArg().argName("tolerance")
+			.build();
+	private static final Option OPT_GROUNDER_TOLERANCE_RULES = Option.builder("gtr").longOpt("grounderToleranceRules")
+			.desc("grounder tolerance for rules (default: " + SystemConfig.DEFAULT_GROUNDER_TOLERANCE_RULES + ")")
+			.hasArg().argName("tolerance")
+			.build();
+	private static final Option OPT_NO_INSTANCE_REMOVAL = Option.builder("dir").longOpt("disableInstanceRemoval")
+			.desc("activates the accumulator grounding strategy by disabling removal of instances from grounder memory in certain cases (default: " + SystemConfig.DEFAULT_DISABLE_INSTANCE_REMOVAL + ")")
+			.build();
+	private static final Option OPT_ENABLE_RESTARTS = Option.builder("rs").longOpt("enableRestarts")
+		.desc("enable the usage of (dynamic and static) restarts (default: "
+			+ SystemConfig.DEFAULT_ENABLE_RESTARTS + ")")
+		.build();
+	private static final Option OPT_INITIAL_PHASE = Option.builder("ph").longOpt("initialPhase").hasArg(true).argName("initializer")
+		.desc("set the initial phase [ alltrue | allfalse | random ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + ")")
+		.build();
 
 	private static final Options CLI_OPTS = new Options();
 
@@ -137,6 +155,11 @@ public class CommandLineParser {
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_JUSTIFICATION);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NORMALIZATION_GRID);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_NOGOOD_DELETION);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_INSTANCE_REMOVAL);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_ENABLE_RESTARTS);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_INITIAL_PHASE);
 	}
 
 	/*
@@ -180,6 +203,11 @@ public CommandLineParser(String cmdLineSyntax, Consumer<String> abortAction) {
 		this.globalOptionHandlers.put(CommandLineParser.OPT_NO_JUSTIFICATION.getOpt(), this::handleNoJustification);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_NORMALIZATION_GRID.getOpt(), this::handleNormalizationGrid);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_NO_NOGOOD_DELETION.getOpt(), this::handleNoNoGoodDeletion);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS.getOpt(), this::handleGrounderToleranceConstraints);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES.getOpt(), this::handleGrounderToleranceRules);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_NO_INSTANCE_REMOVAL.getOpt(), this::handleNoInstanceRemoval);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_ENABLE_RESTARTS.getOpt(), this::handleEnableRestarts);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_INITIAL_PHASE.getOpt(), this::handleInitialPhase);
 
 		this.inputOptionHandlers.put(CommandLineParser.OPT_NUM_ANSWER_SETS.getOpt(), this::handleNumAnswerSets);
 		this.inputOptionHandlers.put(CommandLineParser.OPT_INPUT.getOpt(), this::handleInput);
@@ -325,7 +353,7 @@ private void handleMomsStrategy(Option opt, SystemConfig cfg) throws ParseExcept
 			throw new ParseException("Unknown mom's strategy: " + momsStrategyName + ". Please try one of the following: " + BinaryNoGoodPropagationEstimation.Strategy.listAllowedValues());
 		}
 	}
-	
+
 	private void handleReplayChoices(Option opt, SystemConfig cfg) throws ParseException {
 		String replayChoices = opt.getValue(SystemConfig.DEFAULT_REPLAY_CHOICES.toString());
 		try {
@@ -359,4 +387,25 @@ private void handleNoNoGoodDeletion(Option opt, SystemConfig cfg) {
 		cfg.setDisableNoGoodDeletion(true);
 	}
 
+	private void handleGrounderToleranceConstraints(Option opt, SystemConfig cfg) {
+		String grounderToleranceConstraints = opt.getValue(SystemConfig.DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS);
+		cfg.setGrounderToleranceConstraints(grounderToleranceConstraints);
+	}
+
+	private void handleGrounderToleranceRules(Option opt, SystemConfig cfg) {
+		String grounderToleranceRules = opt.getValue(SystemConfig.DEFAULT_GROUNDER_TOLERANCE_RULES);
+		cfg.setGrounderToleranceRules(grounderToleranceRules);
+	}
+
+	private void handleNoInstanceRemoval(Option opt, SystemConfig cfg) {
+		cfg.setDisableInstanceRemoval(true);
+	}
+
+	private void handleEnableRestarts(Option opt, SystemConfig cfg) {
+		cfg.setRestartsEnabled(true);
+	}
+
+	private void handleInitialPhase(Option opt, SystemConfig cfg) {
+		cfg.setPhaseInitializer(opt.getValue(SystemConfig.DEFAULT_PHASE_INITIALIZER));
+	}
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java
index 6ffeeb8cf..8c6e74306 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java
@@ -27,6 +27,7 @@
  */
 package at.ac.tuwien.kr.alpha.config;
 
+import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation;
 import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic;
 
@@ -56,6 +57,11 @@ public class SystemConfig {
 	public static final boolean DEFAULT_SORT_ANSWER_SETS = false;
 	public static final List<Integer> DEFAULT_REPLAY_CHOICES = Collections.emptyList();
 	public static final boolean DEFAULT_DISABLE_NOGOOD_DELETION = false;
+	public static final String DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS = GrounderHeuristicsConfiguration.STRICT_STRING;
+	public static final String DEFAULT_GROUNDER_TOLERANCE_RULES = GrounderHeuristicsConfiguration.STRICT_STRING;
+	public static final boolean DEFAULT_DISABLE_INSTANCE_REMOVAL = false;
+	public static final boolean DEFAULT_ENABLE_RESTARTS = false;
+	public static final String DEFAULT_PHASE_INITIALIZER = "random";
 
 	private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME;
 	private String solverName = SystemConfig.DEFAULT_SOLVER_NAME;
@@ -72,6 +78,11 @@ public class SystemConfig {
 	private boolean sortAnswerSets = SystemConfig.DEFAULT_SORT_ANSWER_SETS;
 	private List<Integer> replayChoices = SystemConfig.DEFAULT_REPLAY_CHOICES;
 	private boolean disableNoGoodDeletion = SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION;
+	private String grounderToleranceConstraints = DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS;
+	private String grounderToleranceRules = DEFAULT_GROUNDER_TOLERANCE_RULES;
+	private boolean disableInstanceRemoval = DEFAULT_DISABLE_INSTANCE_REMOVAL;
+	private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS;
+	private String phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER;
 
 	public String getGrounderName() {
 		return this.grounderName;
@@ -205,4 +216,43 @@ public void setDisableNoGoodDeletion(boolean disableNoGoodDeletion) {
 		this.disableNoGoodDeletion = disableNoGoodDeletion;
 	}
 
+	public String getGrounderToleranceConstraints() {
+		return grounderToleranceConstraints;
+	}
+
+	public void setGrounderToleranceConstraints(String grounderToleranceConstraints) {
+		this.grounderToleranceConstraints = grounderToleranceConstraints;
+	}
+
+	public String getGrounderToleranceRules() {
+		return grounderToleranceRules;
+	}
+
+	public void setGrounderToleranceRules(String grounderToleranceRules) {
+		this.grounderToleranceRules = grounderToleranceRules;
+	}
+
+	public boolean isDisableInstanceRemoval() {
+		return disableInstanceRemoval;
+	}
+
+	public void setDisableInstanceRemoval(boolean disableInstanceRemoval) {
+		this.disableInstanceRemoval = disableInstanceRemoval;
+	}
+	public boolean areRestartsEnabled() {
+		return areRestartsEnabled;
+	}
+
+	public void setRestartsEnabled(boolean areRestartsEnabled) {
+		this.areRestartsEnabled = areRestartsEnabled;
+	}
+
+	public String getPhaseInitializerName() {
+		return phaseInitializer;
+	}
+
+	public void  setPhaseInitializer(String phaseInitializer) {
+		this.phaseInitializer = phaseInitializer;
+	}
+
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java
index c807e0bae..d4b223a60 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java
@@ -121,7 +121,7 @@ public String toString() {
 		}
 		sb.append(" disablers: ");
 		for (Map.Entry<Integer, Integer> disablers : newChoiceAtoms.getRight().entrySet()) {
-			sb.append(disablers.getKey()).append("/").append(disablers.getValue());
+			sb.append(disablers.getKey()).append("/").append(disablers.getValue()).append(", ");
 		}
 		return sb.append("]").toString();
 	}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java
index cee82381e..89503f40f 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java
@@ -31,6 +31,7 @@
 import at.ac.tuwien.kr.alpha.common.Assignment;
 import at.ac.tuwien.kr.alpha.common.NoGood;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import org.apache.commons.lang3.tuple.Pair;
 
 import java.util.Iterator;
@@ -79,4 +80,11 @@ public interface Grounder {
 	 * @return
 	 */
 	int register(NoGood noGood);
+
+
+	/**
+	 * Returns the relation between atoms and choices in form of an {@link AtomChoiceRelation} object.
+	 * @return the {@link AtomChoiceRelation} of the grounded program parts.
+	 */
+	AtomChoiceRelation getAtomChoiceRelation();
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/GrounderFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/GrounderFactory.java
index 55742d30d..555a18986 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/GrounderFactory.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/GrounderFactory.java
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2016-2018, the Alpha Team.
+ * Copyright (c) 2016-2019, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -32,21 +32,22 @@
 import at.ac.tuwien.kr.alpha.common.Program;
 import at.ac.tuwien.kr.alpha.config.InputConfig;
 import at.ac.tuwien.kr.alpha.grounder.bridges.Bridge;
+import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 
 public final class GrounderFactory {
-	public static Grounder getInstance(String name, Program program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter, boolean useCountingGridNormalization, boolean debugInternalChecks, Bridge... bridges) {
+	public static Grounder getInstance(String name, Program program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter, GrounderHeuristicsConfiguration heuristicsConfiguration, boolean useCountingGridNormalization, boolean debugInternalChecks, Bridge... bridges) {
 		switch (name.toLowerCase()) {
 			case "naive":
-				return new NaiveGrounder(program, atomStore, filter, useCountingGridNormalization, debugInternalChecks, bridges);
+				return new NaiveGrounder(program, atomStore, filter, heuristicsConfiguration, useCountingGridNormalization, debugInternalChecks, bridges);
 		}
 		throw new IllegalArgumentException("Unknown grounder requested.");
 	}
 
-	public static Grounder getInstance(String name, Program program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter, boolean debugInternalChecks) {
-		return getInstance(name, program, atomStore, filter, false, debugInternalChecks);
-	}	
-	
+	public static Grounder getInstance(String name, Program program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter, GrounderHeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks) {
+		return getInstance(name, program, atomStore, filter, heuristicsConfiguration, false, debugInternalChecks);
+	}
+
 	public static Grounder getInstance(String name, Program program, AtomStore atomStore, boolean debugInternalChecks) {
-		return getInstance(name, program, atomStore, InputConfig.DEFAULT_FILTER, false, debugInternalChecks);
+		return getInstance(name, program, atomStore, InputConfig.DEFAULT_FILTER, new GrounderHeuristicsConfiguration(), false, debugInternalChecks);
 	}
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java
index 387f86a4e..dbdb6866b 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java
@@ -29,16 +29,16 @@
 
 import at.ac.tuwien.kr.alpha.common.*;
 import at.ac.tuwien.kr.alpha.common.NoGood.Type;
-import at.ac.tuwien.kr.alpha.common.atoms.Atom;
-import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
-import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral;
-import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.common.atoms.*;
 import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
 import at.ac.tuwien.kr.alpha.grounder.atoms.ChoiceAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom;
+import at.ac.tuwien.kr.alpha.grounder.atoms.IntervalLiteral;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
 import at.ac.tuwien.kr.alpha.grounder.bridges.Bridge;
+import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.grounder.structure.AnalyzeUnjustified;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis;
 import at.ac.tuwien.kr.alpha.grounder.transformation.*;
 import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
@@ -50,12 +50,11 @@
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
 import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
-import static java.util.Collections.emptyList;
 import static java.util.Collections.singletonList;
 
 /**
  * A semi-naive grounder.
- * Copyright (c) 2016-2018, the Alpha Team.
+ * Copyright (c) 2016-2019, the Alpha Team.
  */
 public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGrounder {
 	private static final Logger LOGGER = LoggerFactory.getLogger(NaiveGrounder.class);
@@ -72,29 +71,28 @@ public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGr
 	private final Map<IndexedInstanceStorage, ArrayList<FirstBindingAtom>> rulesUsingPredicateWorkingMemory = new HashMap<>();
 	private final Map<NonGroundRule, HashSet<Substitution>> knownGroundingSubstitutions = new HashMap<>();
 	private final Map<Integer, NonGroundRule> knownNonGroundRules = new HashMap<>();
+	private final AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation();
 
 	private ArrayList<NonGroundRule> fixedRules = new ArrayList<>();
 	private LinkedHashSet<Atom> removeAfterObtainingNewNoGoods = new LinkedHashSet<>();
-	private int maxAtomIdBeforeGroundingNewNoGoods = -1;
-	private boolean disableInstanceRemoval;
-	private boolean useCountingGridNormalization;
-	private boolean debugInternalChecks;
-	
-	/**
-	 * If this configuration parameter is {@code true} (which it is by default),
-	 * the grounder stops grounding a rule if it contains a positive body atom which is not
-	 * yet true, except if the whole rule is already ground. Is currently used only internally,
-	 * but might be used for grounder heuristics and also set from the outside in the future.
-	 */
-	private boolean stopBindingAtNonTruePositiveBody = true;
+	private final boolean useCountingGridNormalization;
+	private final boolean debugInternalChecks;
+
+	private final GrounderHeuristicsConfiguration heuristicsConfiguration;
 
 	public NaiveGrounder(Program program, AtomStore atomStore, boolean debugInternalChecks, Bridge... bridges) {
-		this(program, atomStore, p -> true, false, debugInternalChecks, bridges);
+		this(program, atomStore, new GrounderHeuristicsConfiguration(), debugInternalChecks, bridges);
+	}
+
+	private NaiveGrounder(Program program, AtomStore atomStore, GrounderHeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks, Bridge... bridges) {
+		this(program, atomStore, p -> true, heuristicsConfiguration, false, debugInternalChecks, bridges);
 	}
 
-	NaiveGrounder(Program program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter, boolean useCountingGrid, boolean debugInternalChecks, Bridge... bridges) {
+	NaiveGrounder(Program program, AtomStore atomStore, java.util.function.Predicate<Predicate> filter, GrounderHeuristicsConfiguration heuristicsConfiguration, boolean useCountingGrid, boolean debugInternalChecks, Bridge... bridges) {
 		super(filter, bridges);
 		this.atomStore = atomStore;
+		this.heuristicsConfiguration = heuristicsConfiguration;
+		LOGGER.debug("Grounder configuration: " + heuristicsConfiguration);
 
 		programAnalysis = new ProgramAnalysis(program);
 		analyzeUnjustified = new AnalyzeUnjustified(programAnalysis, atomStore, factsFromProgram);
@@ -108,11 +106,15 @@ public NaiveGrounder(Program program, AtomStore atomStore, boolean debugInternal
 
 		final Set<NonGroundRule> uniqueGroundRulePerGroundHead = getRulesWithUniqueHead();
 		choiceRecorder = new ChoiceRecorder(atomStore);
-		noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, programAnalysis, uniqueGroundRulePerGroundHead);
-		
+		noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, programAnalysis, uniqueGroundRulePerGroundHead, atomChoiceRelation);
 		this.debugInternalChecks = debugInternalChecks;
 	}
 
+	@Override
+	public AtomChoiceRelation getAtomChoiceRelation() {
+		return atomChoiceRelation;
+	}
+
 	private void initializeFactsAndRules(Program program) {
 		// initialize all facts
 		for (Atom fact : program.getFacts()) {
@@ -140,6 +142,7 @@ private void initializeFactsAndRules(Program program) {
 			// Record the rule for later use
 			NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule);
 			knownNonGroundRules.put(nonGroundRule.getRuleId(), nonGroundRule);
+			LOGGER.debug("NonGroundRule #" + nonGroundRule.getRuleId() + ": " + nonGroundRule);
 
 			// Record defining rules for each predicate.
 			Atom headAtom = nonGroundRule.getHeadAtom();
@@ -292,7 +295,7 @@ public AnswerSet assignmentToAnswerSet(Iterable<Integer> trueAtoms) {
 	 * Prepares facts of the input program for joining and derives all NoGoods representing ground rules. May only be called once.
 	 * @return
 	 */
-	private HashMap<Integer, NoGood> bootstrap() {
+	HashMap<Integer, NoGood> bootstrap() {
 		final HashMap<Integer, NoGood> groundNogoods = new LinkedHashMap<>();
 
 		for (Predicate predicate : factsFromProgram.keySet()) {
@@ -302,9 +305,9 @@ private HashMap<Integer, NoGood> bootstrap() {
 
 		for (NonGroundRule nonGroundRule : fixedRules) {
 			// Generate NoGoods for all rules that have a fixed grounding.
-			Literal[] groundingOrder = nonGroundRule.groundingOrder.getFixedGroundingOrder();
-			List<Substitution> substitutions = bindNextAtomInRule(nonGroundRule, groundingOrder, 0, new Substitution(), null);
-			groundAndRegister(nonGroundRule, substitutions, groundNogoods);
+			RuleGroundingOrder groundingOrder = nonGroundRule.groundingOrder.getFixedGroundingOrder();
+			BindingResult bindingResult = bindNextAtomInRule(nonGroundRule, groundingOrder, new Substitution(), null);
+			groundAndRegister(nonGroundRule, bindingResult.generatedSubstitutions, groundNogoods);
 		}
 
 		fixedRules = null;
@@ -317,7 +320,6 @@ public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
 		// In first call, prepare facts and ground rules.
 		final Map<Integer, NoGood> newNoGoods = fixedRules != null ? bootstrap() : new LinkedHashMap<>();
 
-		maxAtomIdBeforeGroundingNewNoGoods = atomStore.getMaxAtomId();
 		// Compute new ground rule (evaluate joins with newly changed atoms)
 		for (IndexedInstanceStorage modifiedWorkingMemory : workingMemory.modified()) {
 			// Skip predicates solely used in the solver which do not occur in rules.
@@ -348,15 +350,14 @@ public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
 						continue;
 					}
 
-					final List<Substitution> substitutions = bindNextAtomInRule(
+					final BindingResult bindingResult = bindNextAtomInRule(
 						nonGroundRule,
 						nonGroundRule.groundingOrder.orderStartingFrom(firstBindingAtom.startingLiteral),
-						0,
 						unifier,
 						currentAssignment
 					);
 
-					groundAndRegister(nonGroundRule, substitutions, newNoGoods);
+					groundAndRegister(nonGroundRule, bindingResult.generatedSubstitutions, newNoGoods);
 				}
 			}
 
@@ -367,7 +368,11 @@ public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
 		workingMemory.reset();
 		for (Atom removeAtom : removeAfterObtainingNewNoGoods) {
 			final IndexedInstanceStorage storage = this.workingMemory.get(removeAtom, true);
-			storage.removeInstance(new Instance(removeAtom.getTerms()));
+			Instance instance = new Instance(removeAtom.getTerms());
+			if (storage.containsInstance(instance)) {
+				// lax grounder heuristics may attempt to remove instances that are not yet in the working memory
+				storage.removeInstance(instance);
+			}
 		}
 
 		removeAfterObtainingNewNoGoods = new LinkedHashSet<>();
@@ -378,17 +383,17 @@ public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
 			}
 			LOGGER.debug("{}", choiceRecorder);
 		}
-		
+
 		if (debugInternalChecks) {
 			checkTypesOfNoGoods(newNoGoods.values());
 		}
-		
+
 		return newNoGoods;
 	}
 
 	/**
 	 * Grounds the given {@code nonGroundRule} by applying the given {@code substitutions} and registers the nogoods generated during that process.
-	 * 
+	 *
 	 * @param nonGroundRule
 	 *          the rule to be grounded
 	 * @param substitutions
@@ -408,92 +413,135 @@ public int register(NoGood noGood) {
 		return registry.register(noGood);
 	}
 
-	private List<Substitution> bindNextAtomInRule(NonGroundRule rule, Literal[] groundingOrder, int orderPosition, Substitution partialSubstitution, Assignment currentAssignment) {
-		if (orderPosition == groundingOrder.length) {
-			return singletonList(partialSubstitution);
+	BindingResult bindNextAtomInRule(NonGroundRule rule, RuleGroundingOrder groundingOrder, Substitution partialSubstitution, Assignment currentAssignment) {
+		int tolerance = heuristicsConfiguration.getTolerance(rule.isConstraint());
+		if (tolerance < 0) {
+			tolerance = Integer.MAX_VALUE;
+		}
+		BindingResult bindingResult = bindNextAtomInRule(groundingOrder, 0, tolerance, tolerance, partialSubstitution, currentAssignment);
+		if (LOGGER.isDebugEnabled()) {
+			for (int i = 0; i < bindingResult.size(); i++) {
+				Integer numberOfUnassignedPositiveBodyAtoms = bindingResult.numbersOfUnassignedPositiveBodyAtoms.get(i);
+				if (numberOfUnassignedPositiveBodyAtoms > 0) {
+					LOGGER.debug("Grounded rule in which " + numberOfUnassignedPositiveBodyAtoms + " positive atoms are still unassigned: " + rule + " (substitution: " + bindingResult.generatedSubstitutions.get(i) + ")");
+				}
+			}
+		}
+		return bindingResult;
+	}
+
+	private BindingResult advanceAndBindNextAtomInRule(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance, Substitution partialSubstitution, Assignment currentAssignment) {
+		groundingOrder.considerUntilCurrentEnd();
+		return bindNextAtomInRule(groundingOrder, orderPosition + 1, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
+	}
+
+	private BindingResult pushBackAndBindNextAtomInRule(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance, Substitution partialSubstitution, Assignment currentAssignment) {
+		RuleGroundingOrder modifiedGroundingOrder = groundingOrder.pushBack(orderPosition);
+		if (modifiedGroundingOrder == null) {
+			return BindingResult.empty();
+		}
+		return bindNextAtomInRule(modifiedGroundingOrder, orderPosition + 1, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
+	}
+
+	private BindingResult bindNextAtomInRule(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance, Substitution partialSubstitution, Assignment currentAssignment) {
+		boolean laxGrounderHeuristic = originalTolerance > 0;
+
+		Literal currentLiteral = groundingOrder.getLiteralAtOrderPosition(orderPosition);
+		if (currentLiteral == null) {
+			return BindingResult.singleton(partialSubstitution, originalTolerance - remainingTolerance);
 		}
 
-		Literal currentLiteral = groundingOrder[orderPosition];
 		Atom currentAtom = currentLiteral.getAtom();
 		if (currentLiteral instanceof FixedInterpretationLiteral) {
 			// Generate all substitutions for the builtin/external/interval atom.
-			final List<Substitution> substitutions = ((FixedInterpretationLiteral)currentLiteral.substitute(partialSubstitution)).getSubstitutions(partialSubstitution);
+			FixedInterpretationLiteral substitutedLiteral = (FixedInterpretationLiteral)currentLiteral.substitute(partialSubstitution);
+			if (shallPushBackFixedInterpretationLiteral(substitutedLiteral)) {
+				return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
+			}
+			final List<Substitution> substitutions = substitutedLiteral.getSubstitutions(partialSubstitution);
 
 			if (substitutions.isEmpty()) {
-				return emptyList();
+				// if FixedInterpretationLiteral cannot be satisfied now, it will never be
+				return BindingResult.empty();
 			}
 
-			final List<Substitution> generatedSubstitutions = new ArrayList<>();
+			final BindingResult bindingResult = new BindingResult();
 			for (Substitution substitution : substitutions) {
 				// Continue grounding with each of the generated values.
-				generatedSubstitutions.addAll(bindNextAtomInRule(rule, groundingOrder, orderPosition + 1, substitution, currentAssignment));
+				bindingResult.add(advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, substitution, currentAssignment));
 			}
-			return generatedSubstitutions;
+			return bindingResult;
 		}
 		if (currentAtom instanceof EnumerationAtom) {
 			// Get the enumeration value and add it to the current partialSubstitution.
 			((EnumerationAtom) currentAtom).addEnumerationToSubstitution(partialSubstitution);
-			return bindNextAtomInRule(rule, groundingOrder, orderPosition + 1, partialSubstitution, currentAssignment);
+			return advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
 		}
 
+		Collection<Instance> instances = null;
+
 		// check if partialVariableSubstitution already yields a ground atom
 		final Atom substitute = currentAtom.substitute(partialSubstitution);
-
 		if (substitute.isGround()) {
 			// Substituted atom is ground, in case it is positive, only ground if it also holds true
 			if (currentLiteral.isNegated()) {
 				// Atom occurs negated in the rule: continue grounding
-				return bindNextAtomInRule(rule, groundingOrder, orderPosition + 1, partialSubstitution, currentAssignment);
-			}
-			
-			if (stopBindingAtNonTruePositiveBody && !rule.getRule().isGround() && !workingMemory.get(currentAtom.getPredicate(), true).containsInstance(new Instance(substitute.getTerms()))) {
-				// Generate no variable substitution.
-				return emptyList();
+				return advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
 			}
 
-			// Check if atom is also assigned true.
-			final LinkedHashSet<Instance> instances = factsFromProgram.get(substitute.getPredicate());
-			if (!(instances == null || !instances.contains(new Instance(substitute.getTerms())))) {
-				// Ground literal holds, continue finding a variable substitution.
-				return bindNextAtomInRule(rule, groundingOrder, orderPosition + 1, partialSubstitution, currentAssignment);
+			if (!groundingOrder.isGround() && remainingTolerance <= 0
+					&& !workingMemory.get(currentAtom.getPredicate(), true).containsInstance(new Instance(substitute.getTerms()))) {
+				// Generate no variable substitution.
+				return BindingResult.empty();
 			}
 
-			// Atom is not a fact already.
-			final int atomId = atomStore.putIfAbsent(substitute);
-
-			if (currentAssignment != null) {
-				final ThriceTruth truth = currentAssignment.getTruth(atomId);
-
-				if (atomId > maxAtomIdBeforeGroundingNewNoGoods || truth == null || !truth.toBoolean()) {
-					// Atom currently does not hold, skip further grounding.
-					// TODO: investigate grounding heuristics for use here, i.e., ground anyways to avoid re-grounding in the future.
-					if (!disableInstanceRemoval) {
-						removeAfterObtainingNewNoGoods.add(substitute);
-						return emptyList();
-					}
-				}
-			}
+			instances = singletonList(new Instance(substitute.getTerms()));
 		}
 
 		// substituted atom contains variables
 		if (currentLiteral.isNegated()) {
-			throw oops("Current atom should be positive at this point but is not");
+			if (laxGrounderHeuristic) {
+				return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
+			} else {
+				throw oops("Current atom should be positive at this point but is not");
+			}
+		}
+
+		if (instances == null) {
+			instances = getInstancesForSubstitute(substitute, partialSubstitution);
+		}
+
+		if (laxGrounderHeuristic && instances.isEmpty()) {
+			// we have reached a point where we have to terminate binding,
+			// but it might be possible that a different grounding order would allow us to continue binding
+			// under the presence of a lax grounder heuristic
+			return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment);
 		}
 
-		IndexedInstanceStorage storage = workingMemory.get(currentAtom.getPredicate(), true);
+		return createBindings(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution, currentAssignment, instances, substitute);
+	}
+
+	private boolean shallPushBackFixedInterpretationLiteral(FixedInterpretationLiteral substitutedLiteral) {
+		return !(substitutedLiteral.isGround() ||
+				(substitutedLiteral instanceof ComparisonLiteral && ((ComparisonLiteral)substitutedLiteral).isLeftOrRightAssigning()) ||
+				(substitutedLiteral instanceof IntervalLiteral && substitutedLiteral.getTerms().get(0).isGround()) ||
+				(substitutedLiteral instanceof ExternalLiteral));
+	}
+
+	private Collection<Instance> getInstancesForSubstitute(Atom substitute, Substitution partialSubstitution) {
 		Collection<Instance> instances;
+		IndexedInstanceStorage storage = workingMemory.get(substitute.getPredicate(), true);
 		if (partialSubstitution.isEmpty()) {
-			if (currentLiteral.isGround()) {
-				instances = singletonList(new Instance(currentLiteral.getTerms()));
-			} else {
-				// No variables are bound, but first atom in the body became recently true, consider all instances now.
-				instances = storage.getAllInstances();
-			}
+			// No variables are bound, but first atom in the body became recently true, consider all instances now.
+			instances = storage.getAllInstances();
 		} else {
 			instances = storage.getInstancesFromPartiallyGroundAtom(substitute);
 		}
+		return instances;
+	}
 
-		ArrayList<Substitution> generatedSubstitutions = new ArrayList<>();
+	private BindingResult createBindings(RuleGroundingOrder groundingOrder, int orderPosition, int originalTolerance, int remainingTolerance, Substitution partialSubstitution, Assignment currentAssignment, Collection<Instance> instances, Atom substitute) {
+		BindingResult bindingResult = new BindingResult();
 		for (Instance instance : instances) {
 			// Check each instance if it matches with the atom.
 			Substitution unified = Substitution.unify(substitute, instance, new Substitution(partialSubstitution));
@@ -509,32 +557,70 @@ private List<Substitution> bindNextAtomInRule(NonGroundRule rule, Literal[] grou
 			}
 
 			if (factsFromProgram.get(substitutedAtom.getPredicate()) == null || !factsFromProgram.get(substitutedAtom.getPredicate()).contains(new Instance(substitutedAtom.getTerms()))) {
-				int atomId = atomStore.putIfAbsent(substitutedAtom);
-
-				if (currentAssignment != null) {
-					ThriceTruth truth = currentAssignment.getTruth(atomId);
-					if (atomId > maxAtomIdBeforeGroundingNewNoGoods || truth == null || !truth.toBoolean()) {
-						// Atom currently does not hold, skip further grounding.
-						// TODO: investigate grounding heuristics for use here, i.e., ground anyways to avoid re-grounding in the future.
-						if (!disableInstanceRemoval) {
-							removeAfterObtainingNewNoGoods.add(substitutedAtom);
-							continue;
-						}
-					}
+				final TerminateOrTolerate terminateOrTolerate = storeAtomAndTerminateIfAtomDoesNotHold(substitutedAtom, currentAssignment, remainingTolerance);
+				if (terminateOrTolerate.decrementTolerance) {
+					remainingTolerance--;
+				}
+				if (terminateOrTolerate.terminate) {
+					continue;
+				}
+			}
+			bindingResult.add(advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, unified, currentAssignment));
+		}
+
+		return bindingResult;
+	}
+
+	private TerminateOrTolerate storeAtomAndTerminateIfAtomDoesNotHold(final Atom substitute, final Assignment currentAssignment, final int remainingTolerance) {
+		int decrementedTolerance = remainingTolerance;
+		if (currentAssignment != null) { // if we are not in bootstrapping
+			final int atomId = atomStore.putIfAbsent(substitute);
+			ThriceTruth truth = currentAssignment.isAssigned(atomId) ? currentAssignment.getTruth(atomId) : null;
+
+			if (heuristicsConfiguration.isDisableInstanceRemoval()) {
+				final Instance instance = new Instance(substitute.getTerms());
+				boolean isInWorkingMemory = workingMemory.get(substitute, true).containsInstance(instance);
+				if (isInWorkingMemory) {
+					return new TerminateOrTolerate(false, false);
+				}
+				if (truth != null && !truth.toBoolean()) {
+					return new TerminateOrTolerate(true, false);
+				}
+				if (--decrementedTolerance < 0) {
+					// terminate if more positive atoms are unsatisfied as tolerated by the heuristic
+					return new TerminateOrTolerate(true, true);
+				}
+			} else {
+				if (truth == null || !truth.toBoolean()) {
+					// Atom currently does not hold
+					removeAfterObtainingNewNoGoods.add(substitute);
+				}
+				if (truth == null && --decrementedTolerance < 0) {
+					// terminate if more positive atoms are unsatisfied as tolerated by the heuristic
+					return new TerminateOrTolerate(true, true);
 				}
+				// terminate if positive body atom is assigned false
+				return new TerminateOrTolerate(truth != null && !truth.toBoolean(), decrementedTolerance < remainingTolerance);
 			}
-			List<Substitution> boundSubstitutions = bindNextAtomInRule(rule, groundingOrder, orderPosition + 1, unified, currentAssignment);
-			generatedSubstitutions.addAll(boundSubstitutions);
 		}
+		return new TerminateOrTolerate(false, decrementedTolerance < remainingTolerance);
+	}
+
+	private static class TerminateOrTolerate {
+		boolean terminate;
+		boolean decrementTolerance;
 
-		return generatedSubstitutions;
+		TerminateOrTolerate(boolean terminate, boolean decrementTolerance) {
+			this.terminate = terminate;
+			this.decrementTolerance = decrementTolerance;
+		}
 	}
 
 	@Override
 	public Pair<Map<Integer, Integer>, Map<Integer, Integer>> getChoiceAtoms() {
 		return choiceRecorder.getAndResetChoices();
 	}
-	
+
 	@Override
 	public Map<Integer, Set<Integer>> getHeadsToBodies() {
 		return choiceRecorder.getAndResetHeadsToBodies();
@@ -552,17 +638,6 @@ public void forgetAssignment(int[] atomIds) {
 		throw new UnsupportedOperationException("Forgetting assignments is not implemented");
 	}
 
-	public void printCurrentlyKnownGroundRules() {
-		System.out.println("Printing known ground rules:");
-		for (Map.Entry<NonGroundRule, HashSet<Substitution>> ruleSubstitutionsEntry : knownGroundingSubstitutions.entrySet()) {
-			NonGroundRule nonGroundRule = ruleSubstitutionsEntry.getKey();
-			HashSet<Substitution> substitutions = ruleSubstitutionsEntry.getValue();
-			for (Substitution substitution : substitutions) {
-				System.out.println(groundAndPrintRule(nonGroundRule, substitution));
-			}
-		}
-	}
-
 	public static String groundAndPrintRule(NonGroundRule rule, Substitution substitution) {
 		StringBuilder ret = new StringBuilder();
 		if (!rule.isConstraint()) {
@@ -638,12 +713,42 @@ private void checkTypesOfNoGoods(Collection<NoGood> newNoGoods) {
 	}
 
 	private static class FirstBindingAtom {
-		NonGroundRule rule;
-		Literal startingLiteral;
+		final NonGroundRule rule;
+		final Literal startingLiteral;
 
 		FirstBindingAtom(NonGroundRule rule, Literal startingLiteral) {
 			this.rule = rule;
 			this.startingLiteral = startingLiteral;
 		}
 	}
+
+	static class BindingResult {
+		final List<Substitution> generatedSubstitutions = new ArrayList<>();
+		final List<Integer> numbersOfUnassignedPositiveBodyAtoms = new ArrayList<>();
+
+		void add(Substitution generatedSubstitution, int numberOfUnassignedPositiveBodyAtoms) {
+			this.generatedSubstitutions.add(generatedSubstitution);
+			this.numbersOfUnassignedPositiveBodyAtoms.add(numberOfUnassignedPositiveBodyAtoms);
+		}
+
+		void add(BindingResult otherBindingResult) {
+			this.generatedSubstitutions.addAll(otherBindingResult.generatedSubstitutions);
+			this.numbersOfUnassignedPositiveBodyAtoms.addAll(otherBindingResult.numbersOfUnassignedPositiveBodyAtoms);
+		}
+
+		int size() {
+			return generatedSubstitutions.size();
+		}
+
+		static BindingResult empty() {
+			return new BindingResult();
+		}
+
+		static BindingResult singleton(Substitution generatedSubstitution, int numberOfUnassignedPositiveBodyAtoms) {
+			BindingResult bindingResult = new BindingResult();
+			bindingResult.add(generatedSubstitution, numberOfUnassignedPositiveBodyAtoms);
+			return bindingResult;
+		}
+
+	}
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java
index 72500f499..7a1e015ff 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java
@@ -34,6 +34,7 @@
 import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral;
 import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis;
 
 import java.util.*;
@@ -52,13 +53,15 @@ public class NoGoodGenerator {
 	private final Map<Predicate, LinkedHashSet<Instance>> factsFromProgram;
 	private final ProgramAnalysis programAnalysis;
 	private final Set<NonGroundRule> uniqueGroundRulePerGroundHead;
+	private final AtomChoiceRelation atomChoiceRelation;
 
-	NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map<Predicate, LinkedHashSet<Instance>> factsFromProgram, ProgramAnalysis programAnalysis, Set<NonGroundRule> uniqueGroundRulePerGroundHead) {
+	NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map<Predicate, LinkedHashSet<Instance>> factsFromProgram, ProgramAnalysis programAnalysis, Set<NonGroundRule> uniqueGroundRulePerGroundHead, AtomChoiceRelation atomChoiceRelation) {
 		this.atomStore = atomStore;
 		this.choiceRecorder = recorder;
 		this.factsFromProgram = factsFromProgram;
 		this.programAnalysis = programAnalysis;
 		this.uniqueGroundRulePerGroundHead = uniqueGroundRulePerGroundHead;
+		this.atomChoiceRelation = atomChoiceRelation;
 	}
 
 	/**
@@ -126,6 +129,15 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround
 			result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals, negLiterals, bodyRepresentingLiteral));
 		}
 
+		// Record atom-choiceAtom relationships for rules that are choice points.
+		if (!negLiterals.isEmpty()) {
+			atomChoiceRelation.growForMaxAtomId(atomStore.getMaxAtomId());
+			atomChoiceRelation.addRelation(headId, atomOf(bodyRepresentingLiteral));
+			for (Integer negLiteral : negLiterals) {
+				atomChoiceRelation.addRelation(atomOf(negLiteral), atomOf(bodyRepresentingLiteral));
+			}
+		}
+
 		return result;
 	}
 
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java
index 557b5bb43..f9cdbdf05 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NonGroundRule.java
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2016-2018, the Alpha Team.
+ * Copyright (c) 2016-2019, the Alpha Team.
  * All rights reserved.
  * 
  * Additional changes made by Siemens.
@@ -45,7 +45,7 @@
  * Copyright (c) 2017-2018, the Alpha Team.
  */
 public class NonGroundRule {
-	private static final IntIdGenerator ID_GENERATOR = new IntIdGenerator();
+	static final IntIdGenerator ID_GENERATOR = new IntIdGenerator();
 
 	private final int ruleId;
 	private final Rule rule;
@@ -54,7 +54,7 @@ public class NonGroundRule {
 	private final List<Atom> bodyAtomsNegative;
 	private final Atom headAtom;
 
-	final RuleGroundingOrder groundingOrder;
+	final RuleGroundingOrders groundingOrder;
 
 	private NonGroundRule(Rule rule, int ruleId, List<Atom> bodyAtomsPositive, List<Atom> bodyAtomsNegative, Atom headAtom) {
 		this.ruleId = ruleId;
@@ -71,7 +71,7 @@ private NonGroundRule(Rule rule, int ruleId, List<Atom> bodyAtomsPositive, List<
 		this.headAtom = headAtom;
 
 		checkSafety();
-		this.groundingOrder = new RuleGroundingOrder(this);
+		this.groundingOrder = new RuleGroundingOrders(this);
 		groundingOrder.computeGroundingOrders();
 	}
 
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java
index 21295d1e7..57ba291e1 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java
@@ -3,6 +3,7 @@
 import at.ac.tuwien.kr.alpha.common.Assignment;
 import at.ac.tuwien.kr.alpha.common.atoms.Atom;
 import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 
 import java.util.Set;
 
@@ -32,4 +33,10 @@ public interface ProgramAnalyzingGrounder extends Grounder {
 	 * @return the corresponding NonGroundRule.
 	 */
 	NonGroundRule getNonGroundRule(Integer ruleId);
+
+	/**
+	 * Provides relationship information between atoms and choice points influencing their truth values.
+	 * @return the {@link AtomChoiceRelation}.
+	 */
+	AtomChoiceRelation getAtomChoiceRelation();
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrder.java
index 477888fd0..a7e780b2e 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrder.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrder.java
@@ -1,19 +1,17 @@
 /**
- * Copyright (c) 2016-2018, the Alpha Team.
+ * Copyright (c) 2019 Siemens AG
  * All rights reserved.
- *
- * Additional changes made by Siemens.
- *
+ * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
- *
+ * 
  * 1) Redistributions of source code must retain the above copyright notice, this
  *    list of conditions and the following disclaimer.
- *
+ * 
  * 2) Redistributions in binary form must reproduce the above copyright notice,
  *    this list of conditions and the following disclaimer in the documentation
  *    and/or other materials provided with the distribution.
- *
+ * 
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
@@ -27,188 +25,100 @@
  */
 package at.ac.tuwien.kr.alpha.grounder;
 
-import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
 import at.ac.tuwien.kr.alpha.common.atoms.Literal;
-import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.List;
 
 /**
- * Provides the grounder with information on the order to ground the literals in the body of a rule.
- * Grounding starts with some starting literal (i.e., one that does not require any variables to be bound already) and
- * then may join this with any other literal that requires no other variables to be bound other than those already bound
- * by the first literal. This class is prepared to take join-selectivities into account for finding a good grounding
- * order.
- *
- * Since the grounder must yield all ground instantiations of rules whose positive body is true in the current assignment,
- * a starting literals is a positive BasicAtom and the grounder can wait until after some instance in the working memory
- * of the corresponding predicate arrives and only then start grounding.
- *
- * There is also the case that a rule has no ordinary positive literals (i.e., no positive BasicAtom) but is still safe.
- * Such a rule has no starting literal but those rules have a fixed number of ground instantiations and they can be
- * computed similar to facts at the beginning of the computation.
- *
- * Note that rules with self-joins (rules with p(X,Y), p(A,B) in their body) make it necessary that every positive
- * literal (whose interpretation is not fixed) is a starting literal, at least for the current grounding procedure.
- * Copyright (c) 2017, the Alpha Team.
+ * A grounding order computed by {@link RuleGroundingOrders} for a specific {@link NonGroundRule} and a specific starting literal.
  */
 public class RuleGroundingOrder {
-	private final NonGroundRule nonGroundRule;
-	private HashMap<Literal, Literal[]> groundingOrder;
-	private HashMap<Literal, Float> literalSelectivity;
-	private List<Literal> startingLiterals;
 
-	private final boolean fixedGroundingInstantiation;
-	private Literal[] fixedGroundingOrder;
-
-	RuleGroundingOrder(NonGroundRule nonGroundRule) {
-		this.nonGroundRule = nonGroundRule;
-		this.literalSelectivity = new HashMap<>();
-		resetLiteralSelectivity();
-		this.groundingOrder = new HashMap<>();
-		this.fixedGroundingInstantiation = computeStartingLiterals();
+	private Literal startingLiteral;
+	private List<Literal> otherLiterals;
+	private int positionLastVarBound;
+	private int stopBindingAtOrderPosition;
+	private final boolean ground;
+	
+	RuleGroundingOrder(Literal startingLiteral, List<Literal> otherLiterals, int positionLastVarBound, boolean isGround) {
+		super();
+		this.startingLiteral = startingLiteral;
+		this.otherLiterals = otherLiterals;
+		this.positionLastVarBound = positionLastVarBound;
+		this.stopBindingAtOrderPosition = otherLiterals.size();
+		this.ground = isGround;
 	}
-
-	private void resetLiteralSelectivity() {
-		// Set selectivity of all literals to 1.0f.
-		for (Literal literal : nonGroundRule.getBodyLiterals()) {
-			literalSelectivity.put(literal, 1.0f);
-		}
+	
+	private RuleGroundingOrder(RuleGroundingOrder otherRuleGroundingOrder) {
+		this(otherRuleGroundingOrder.startingLiteral, new ArrayList<>(otherRuleGroundingOrder.otherLiterals), otherRuleGroundingOrder.positionLastVarBound, otherRuleGroundingOrder.ground);
+		this.stopBindingAtOrderPosition = otherRuleGroundingOrder.stopBindingAtOrderPosition;
 	}
-
+	
 	/**
-	 * Computes starting literals and indicates whether there is a fixed ground instantiation for this rule.
-	 * @return true iff the rule has a fixed ground instantiation.
+	 * Returns the literal at the given position in the grounding order,
+	 * except it is already known that this literal is not able to yield new bindings.
+	 * 
+	 * A literal cannot yield new bindings if it has been copied to the end of the grounding order
+	 * when no bindings could be found, and no bindings for other literals could be found in the meantime.
+	 * 
+	 * @param orderPosition zero-based index into list of literals except the starting literal
+	 * @return the literal at the given position, or {@code null} if it is already known that this literal is not able to yield new bindings
 	 */
-	private boolean computeStartingLiterals() {
-		LinkedHashSet<Literal> fixedStartingLiterals = new LinkedHashSet<>();
-		LinkedHashSet<Literal> ordinaryStartingLiterals = new LinkedHashSet<>();
-		
-		// If the rule is ground, every body literal is a starting literal and the ground instantiation is fixed.
-		if (nonGroundRule.getRule().isGround()) {
-			startingLiterals = new LinkedList<>(nonGroundRule.getBodyLiterals());
-			return true;
+	public Literal getLiteralAtOrderPosition(int orderPosition) {
+		if (orderPosition >= stopBindingAtOrderPosition) {
+			return null;
 		}
-		
-		// Check each literal in the rule body whether it is eligible.
-		for (Literal literal : nonGroundRule.getBodyLiterals()) {
-			// Only literals that need no variables already bound can start grounding.
-			if (literal.getNonBindingVariables().size() != 0) {
-				continue;
-			}
-
-			if (literal.getAtom() instanceof BasicAtom && !literal.isNegated()) {
-				// Positive BasicAtom is the main/ordinary case.
-				ordinaryStartingLiterals.add(literal);
-			} else {
-				// If literal is no positive BasicAtom but requires no bound variables,
-				// it can be the starting literal for some (fixed) instantiation.
-				fixedStartingLiterals.add(literal);
-			}
-		}
-		// If there are no positive BasicAtoms, the rule only contains fixed ground
-		// instantiation literals and those are starting for the one-time grounding.
-		if (!ordinaryStartingLiterals.isEmpty()) {
-			startingLiterals = new LinkedList<>(ordinaryStartingLiterals);
-			return false;
-		} else if (!fixedStartingLiterals.isEmpty()) {
-			startingLiterals = new LinkedList<>(fixedStartingLiterals);
-			return true;
-		} else {
-			throw new RuntimeException("Unsafe rule encountered: " + nonGroundRule.getRule());
-		}
-	}
-
-	Collection<Literal> getStartingLiterals() {
-		return Collections.unmodifiableList(startingLiterals);
-	}
-
-	public void updateLiteralSelectivity(Literal literal, int numGivenTuples, int numObtainedTuples) {
-		// TODO: add old selectivity (with a decay factor) and new selectivity.
-	}
-
-	Literal[] orderStartingFrom(Literal startingLiteral) {
-		return groundingOrder.get(startingLiteral);
-	}
-
-
-	Literal[] getFixedGroundingOrder() {
-		return fixedGroundingOrder;
+		return otherLiterals.get(orderPosition);
 	}
 
 	/**
-	 * States whether the rule is without positive ordinary atoms, as for example in: p(Y) :- X = 1..3, not q(X), Y = X + 2, &ext[X,Y]().
-	 * @return true if the rule has a (limited number of) fixed grounding instantiation(s).
+	 * @return the zero-based position from which on all variables are bound in list of literals except the starting literal
 	 */
-	boolean fixedInstantiation() {
-		return fixedGroundingInstantiation;
+	public int getPositionFromWhichAllVarsAreBound() {
+		return positionLastVarBound + 1;
 	}
 
-	void computeGroundingOrders() {
-		if (fixedGroundingInstantiation) {
-			// Fixed grounding is only evaluated once and not depending on a starting variable, just use the first.
-			computeGroundingOrder(startingLiterals.get(0));
-			return;
-		}
-		// Compute grounding orders for all positive BasicAtoms.
-		for (Literal literal : startingLiterals) {
-			computeGroundingOrder(literal);
-		}
+	public boolean isGround() {
+		return ground;
 	}
 
-	private void computeGroundingOrder(Literal startingLiteral) {
-		List<Literal> bodyLiterals = nonGroundRule.getBodyLiterals();
-		HashSet<VariableTerm> boundVariables = new HashSet<>();
-		boundVariables.addAll(startingLiteral.getBindingVariables());
-		LinkedHashSet<Literal> remainingLiterals = new LinkedHashSet<>(bodyLiterals);
-		remainingLiterals.remove(startingLiteral);
-		ArrayList<Literal> literalsOrder;
-		if (fixedGroundingInstantiation) {
-			literalsOrder = new ArrayList<>(bodyLiterals.size());
-			literalsOrder.add(startingLiteral);
-		} else {
-			literalsOrder = new ArrayList<>(bodyLiterals.size() - 1);
-		}
-		while (!remainingLiterals.isEmpty()) {
-			Literal nextGroundingLiteral = selectNextGroundingLiteral(remainingLiterals, boundVariables);
-			if (nextGroundingLiteral == null) {
-				throw new RuntimeException("Could not find a grounding order for rule " + nonGroundRule + " with starting literal: " + startingLiteral + ". Rule is not safe.");
+	/* (non-Javadoc)
+	 * @see java.lang.Object#toString()
+	 */
+	@Override
+	public String toString() {
+		StringBuilder sb = new StringBuilder();
+		sb.append(startingLiteral);
+		sb.append(" : ");
+		for (int i = 0; i < otherLiterals.size(); i++) {
+			if (i == positionLastVarBound + 1) {
+				sb.append("| ");
+			}
+			sb.append(otherLiterals.get(i));
+			if (i < otherLiterals.size() - 1) {
+				sb.append(", ");
 			}
-			remainingLiterals.remove(nextGroundingLiteral);
-			boundVariables.addAll(nextGroundingLiteral.getBindingVariables());
-			literalsOrder.add(nextGroundingLiteral);
-		}
-		if (fixedGroundingInstantiation) {
-			fixedGroundingOrder = literalsOrder.toArray(new Literal[0]);
 		}
-		groundingOrder.put(startingLiteral, literalsOrder.toArray(new Literal[0]));
+		
+		return sb.toString();
 	}
 
-	private Literal selectNextGroundingLiteral(LinkedHashSet<Literal> remainingLiterals, Set<VariableTerm> boundVariables) {
-		Float bestSelectivity = Float.MAX_VALUE;
-		Literal bestLiteral = null;
-		boolean bestLiteralSharesVariables = false;
-		// Find the best literal whose nonbinding variables are already bound and whose selectivity is highest.
-		// To avoid cross products, select those first that have some of their variables already bound.
-		for (Literal literal : remainingLiterals) {
-			if (!boundVariables.containsAll(literal.getNonBindingVariables())) {
-				// Only consider literals whose nonbinding variables are already bound.
-				continue;
-			}
-			Float selectivity = literalSelectivity.get(literal);
-			boolean sharesVariables = sharesVariables(boundVariables, literal.getBindingVariables(), literal.getNonBindingVariables());
-			if (bestLiteral == null
-				|| sharesVariables && selectivity < bestSelectivity
-				|| sharesVariables && !bestLiteralSharesVariables) {
-				bestLiteral = literal;
-				bestSelectivity = selectivity;
-				bestLiteralSharesVariables = sharesVariables;
-			}
+	/**
+	 * @param orderPosition
+	 * @return
+	 */
+	public RuleGroundingOrder pushBack(int orderPosition) {
+		if (orderPosition >= stopBindingAtOrderPosition - 1) {
+			return null;
 		}
-		return bestLiteral;
+		RuleGroundingOrder reorderedGroundingOrder = new RuleGroundingOrder(this);
+		reorderedGroundingOrder.otherLiterals.add(otherLiterals.get(orderPosition));
+		return reorderedGroundingOrder;
 	}
-
-	private boolean sharesVariables(Collection<VariableTerm> set1, Collection<VariableTerm> set2part1, Collection<VariableTerm> set2part2) {
-		return !Collections.disjoint(set1, set2part1) || !Collections.disjoint(set1, set2part2);
+	
+	public void considerUntilCurrentEnd() {
+		this.stopBindingAtOrderPosition = this.otherLiterals.size();
 	}
+
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrders.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrders.java
new file mode 100644
index 000000000..50fe9bada
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrders.java
@@ -0,0 +1,220 @@
+/**
+ * Copyright (c) 2016-2019, the Alpha Team.
+ * All rights reserved.
+ *
+ * Additional changes made by Siemens.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ *
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+package at.ac.tuwien.kr.alpha.grounder;
+
+import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
+import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
+
+import java.util.*;
+
+/**
+ * Provides the grounder with information on the order to ground the literals in the body of a rule.
+ * Grounding starts with some starting literal (i.e., one that does not require any variables to be bound already) and
+ * then may join this with any other literal that requires no other variables to be bound other than those already bound
+ * by the first literal. This class is prepared to take join-selectivities into account for finding a good grounding
+ * order.
+ *
+ * Since the grounder must yield all ground instantiations of rules whose positive body is true in the current assignment,
+ * a starting literals is a positive BasicAtom and the grounder can wait until after some instance in the working memory
+ * of the corresponding predicate arrives and only then start grounding.
+ *
+ * There is also the case that a rule has no ordinary positive literals (i.e., no positive BasicAtom) but is still safe.
+ * Such a rule has no starting literal but those rules have a fixed number of ground instantiations and they can be
+ * computed similar to facts at the beginning of the computation.
+ *
+ * Note that rules with self-joins (rules with p(X,Y), p(A,B) in their body) make it necessary that every positive
+ * literal (whose interpretation is not fixed) is a starting literal, at least for the current grounding procedure.
+ */
+public class RuleGroundingOrders {
+	private final NonGroundRule nonGroundRule;
+	HashMap<Literal, RuleGroundingOrder> groundingOrders;
+	private HashMap<Literal, Float> literalSelectivity;
+	private List<Literal> startingLiterals;
+
+	private final boolean fixedGroundingInstantiation;
+	private RuleGroundingOrder fixedGroundingOrder;
+
+	RuleGroundingOrders(NonGroundRule nonGroundRule) {
+		this.nonGroundRule = nonGroundRule;
+		this.literalSelectivity = new HashMap<>();
+		resetLiteralSelectivity();
+		this.groundingOrders = new HashMap<>();
+		this.fixedGroundingInstantiation = computeStartingLiterals();
+	}
+
+	private void resetLiteralSelectivity() {
+		// Set selectivity of all literals to 1.0f.
+		for (Literal literal : nonGroundRule.getBodyLiterals()) {
+			literalSelectivity.put(literal, 1.0f);
+		}
+	}
+
+	/**
+	 * Computes starting literals and indicates whether there is a fixed ground instantiation for this rule.
+	 * @return true iff the rule has a fixed ground instantiation.
+	 */
+	private boolean computeStartingLiterals() {
+		LinkedHashSet<Literal> fixedStartingLiterals = new LinkedHashSet<>();
+		LinkedHashSet<Literal> ordinaryStartingLiterals = new LinkedHashSet<>();
+		
+		// If the rule is ground, every body literal is a starting literal and the ground instantiation is fixed.
+		if (nonGroundRule.getRule().isGround()) {
+			startingLiterals = new LinkedList<>(nonGroundRule.getBodyLiterals());
+			return true;
+		}
+		
+		// Check each literal in the rule body whether it is eligible.
+		for (Literal literal : nonGroundRule.getBodyLiterals()) {
+			// Only literals that need no variables already bound can start grounding.
+			if (literal.getNonBindingVariables().size() != 0) {
+				continue;
+			}
+
+			if (literal.getAtom() instanceof BasicAtom && !literal.isNegated()) {
+				// Positive BasicAtom is the main/ordinary case.
+				ordinaryStartingLiterals.add(literal);
+			} else {
+				// If literal is no positive BasicAtom but requires no bound variables,
+				// it can be the starting literal for some (fixed) instantiation.
+				fixedStartingLiterals.add(literal);
+			}
+		}
+		// If there are no positive BasicAtoms, the rule only contains fixed ground
+		// instantiation literals and those are starting for the one-time grounding.
+		if (!ordinaryStartingLiterals.isEmpty()) {
+			startingLiterals = new LinkedList<>(ordinaryStartingLiterals);
+			return false;
+		} else if (!fixedStartingLiterals.isEmpty()) {
+			startingLiterals = new LinkedList<>(fixedStartingLiterals);
+			return true;
+		} else {
+			throw new RuntimeException("Unsafe rule encountered: " + nonGroundRule.getRule());
+		}
+	}
+
+	Collection<Literal> getStartingLiterals() {
+		return Collections.unmodifiableList(startingLiterals);
+	}
+
+	public void updateLiteralSelectivity(Literal literal, int numGivenTuples, int numObtainedTuples) {
+		// TODO: add old selectivity (with a decay factor) and new selectivity.
+	}
+
+	RuleGroundingOrder orderStartingFrom(Literal startingLiteral) {
+		return groundingOrders.get(startingLiteral);
+	}
+
+
+	RuleGroundingOrder getFixedGroundingOrder() {
+		return fixedGroundingOrder;
+	}
+
+	/**
+	 * States whether the rule is without positive ordinary atoms, as for example in: p(Y) :- X = 1..3, not q(X), Y = X + 2, &ext[X,Y]().
+	 * @return true if the rule has a (limited number of) fixed grounding instantiation(s).
+	 */
+	boolean fixedInstantiation() {
+		return fixedGroundingInstantiation;
+	}
+
+	void computeGroundingOrders() {
+		if (fixedGroundingInstantiation) {
+			// Fixed grounding is only evaluated once and not depending on a starting variable, just use the first.
+			computeGroundingOrder(startingLiterals.get(0));
+			return;
+		}
+		// Compute grounding orders for all positive BasicAtoms.
+		for (Literal literal : startingLiterals) {
+			computeGroundingOrder(literal);
+		}
+	}
+
+	private void computeGroundingOrder(Literal startingLiteral) {
+		List<Literal> bodyLiterals = nonGroundRule.getBodyLiterals();
+		HashSet<VariableTerm> boundVariables = new HashSet<>();
+		boundVariables.addAll(startingLiteral.getBindingVariables());
+		LinkedHashSet<Literal> remainingLiterals = new LinkedHashSet<>(bodyLiterals);
+		remainingLiterals.remove(startingLiteral);
+		ArrayList<Literal> literalsOrder;
+		if (fixedGroundingInstantiation) {
+			literalsOrder = new ArrayList<>(bodyLiterals.size());
+			literalsOrder.add(startingLiteral);
+		} else {
+			literalsOrder = new ArrayList<>(bodyLiterals.size() - 1);
+		}
+		
+		int position = 0;
+		int positionLastVarBound = -1;
+		while (!remainingLiterals.isEmpty()) {
+			Literal nextGroundingLiteral = selectNextGroundingLiteral(remainingLiterals, boundVariables);
+			if (nextGroundingLiteral == null) {
+				throw new RuntimeException("Could not find a grounding order for rule " + nonGroundRule + " with starting literal: " + startingLiteral + ". Rule is not safe.");
+			}
+			remainingLiterals.remove(nextGroundingLiteral);
+			boolean boundNewVars = boundVariables.addAll(nextGroundingLiteral.getBindingVariables());
+			if (boundNewVars) {
+				positionLastVarBound = position;
+			}
+			literalsOrder.add(nextGroundingLiteral);
+			position++;
+		}
+		if (fixedGroundingInstantiation) {
+			fixedGroundingOrder = new RuleGroundingOrder(null, literalsOrder, positionLastVarBound, nonGroundRule.getRule().isGround());
+		}
+		groundingOrders.put(startingLiteral, new RuleGroundingOrder(startingLiteral, literalsOrder, positionLastVarBound, nonGroundRule.getRule().isGround()));
+	}
+
+	private Literal selectNextGroundingLiteral(LinkedHashSet<Literal> remainingLiterals, Set<VariableTerm> boundVariables) {
+		Float bestSelectivity = Float.MAX_VALUE;
+		Literal bestLiteral = null;
+		boolean bestLiteralSharesVariables = false;
+		// Find the best literal whose nonbinding variables are already bound and whose selectivity is highest.
+		// To avoid cross products, select those first that have some of their variables already bound.
+		for (Literal literal : remainingLiterals) {
+			if (!boundVariables.containsAll(literal.getNonBindingVariables())) {
+				// Only consider literals whose nonbinding variables are already bound.
+				continue;
+			}
+			Float selectivity = literalSelectivity.get(literal);
+			boolean sharesVariables = sharesVariables(boundVariables, literal.getBindingVariables(), literal.getNonBindingVariables());
+			if (bestLiteral == null
+				|| sharesVariables && selectivity < bestSelectivity
+				|| sharesVariables && !bestLiteralSharesVariables) {
+				bestLiteral = literal;
+				bestSelectivity = selectivity;
+				bestLiteralSharesVariables = sharesVariables;
+			}
+		}
+		return bestLiteral;
+	}
+
+	private boolean sharesVariables(Collection<VariableTerm> set1, Collection<VariableTerm> set2part1, Collection<VariableTerm> set2part2) {
+		return !Collections.disjoint(set1, set2part1) || !Collections.disjoint(set1, set2part2);
+	}
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java
index 1f0fbd97e..b859cb501 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Substitution.java
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2016-2018, the Alpha Team.
+ * Copyright (c) 2016-2019, the Alpha Team.
  * All rights reserved.
  *
  * Additional changes made by Siemens.
@@ -41,7 +41,10 @@
 import org.antlr.v4.runtime.RecognitionException;
 import org.antlr.v4.runtime.misc.ParseCancellationException;
 
-import java.util.*;
+import java.util.Collections;
+import java.util.Map;
+import java.util.Objects;
+import java.util.TreeMap;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
 
@@ -224,7 +227,7 @@ public boolean equals(Object o) {
 
 		Substitution that = (Substitution) o;
 
-		return substitution != null ? substitution.equals(that.substitution) : that.substitution == null;
+		return Objects.equals(substitution, that.substitution);
 	}
 
 	@Override
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/heuristics/GrounderHeuristicsConfiguration.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/heuristics/GrounderHeuristicsConfiguration.java
new file mode 100644
index 000000000..5cc1fa448
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/heuristics/GrounderHeuristicsConfiguration.java
@@ -0,0 +1,149 @@
+/**
+ * Copyright (c) 2019 Siemens AG
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+package at.ac.tuwien.kr.alpha.grounder.heuristics;
+
+import at.ac.tuwien.kr.alpha.grounder.Grounder;
+
+/**
+ * Contains configuration parameters for heuristics used by {@link Grounder}s.
+ * 
+ * Both parameters {@link #toleranceConstraints} and {@link #toleranceRules} are interpreted as follows:
+ * A rule (or constraint) is grounded if the following conditions are satisfied:
+ * <ul>
+ * 	<li>All variables in the rule are bound (either by positive body literals that are already
+ *      satisfied, or because the whole rule is ground).</li>
+ * 	<li>No atom occurring positively in the body is assigned F, and no atom occurring negatively
+ *      in the body is assigned T or MBT (because this would make the rule irrelevant in the current
+ *      part of the search space).</li>
+ * 	<li>At most {@code N} atoms occurring positively in the body are still unassigned.</li>
+ * </ul>
+ * 
+ * The parameter {@link #toleranceConstraints} specifies {@code N} for constraints, while {@link #toleranceRules}
+ * specifies {@code N} for all other rules. Infinity is represented by the value {@code -1}.
+ * The default value for both parameters is {@code 0}, which means that only those rules and constraints are
+ * grounded whose positive body is already satisfied.
+ *
+ * The additional parameter {@link #disableInstanceRemoval} is a switch for the accumulator grounding strategy
+ * which disables the removal of instances from the grounder memory in certain cases.
+ *
+ */
+public class GrounderHeuristicsConfiguration {
+
+	public static final String STRICT_STRING = "strict";
+	public static final int STRICT_INT = 0;
+	public static final String LAX_STRING = "lax";
+	public static final int LAX_INT = -1;
+	
+	private int toleranceConstraints;
+	private int toleranceRules;
+	private boolean disableInstanceRemoval;
+	
+	public GrounderHeuristicsConfiguration() {
+		super();
+		this.toleranceConstraints = STRICT_INT;
+		this.toleranceRules = STRICT_INT;
+	}
+	
+	/**
+	 * @param toleranceConstraints
+	 * @param toleranceRules
+	 */
+	private GrounderHeuristicsConfiguration(int toleranceConstraints, int toleranceRules) {
+		super();
+		this.toleranceConstraints = toleranceConstraints;
+		this.toleranceRules = toleranceRules;
+	}
+
+	/**
+	 * @return the tolerance for constraints
+	 */
+	public int getToleranceConstraints() {
+		return toleranceConstraints;
+	}
+
+	/**
+	 * @return the tolerance for rules that are not constraints
+	 */
+	public int getToleranceRules() {
+		return toleranceRules;
+	}
+
+	/**
+	 * @param ruleIsConstraint {@code true} iff the parameter for constraints shall be returned
+	 * @return {@link #getToleranceConstraints()} if {@code ruleIsConstraint}, otherwise {@link #getToleranceRules()}
+	 */
+	public int getTolerance(boolean ruleIsConstraint) {
+		return ruleIsConstraint ? getToleranceConstraints() : getToleranceRules();
+	}
+
+	/**
+	 * @param ruleIsConstraint {@code true} iff the parameter for constraints shall be returned
+	 * @return {@code true} iff the tolerance is not 0
+	 */
+	public boolean isLax(boolean ruleIsConstraint) {
+		return getTolerance(ruleIsConstraint) != STRICT_INT;
+	}
+
+	public boolean isDisableInstanceRemoval() {
+		return disableInstanceRemoval;
+	}
+
+	public void setDisableInstanceRemoval(boolean disableInstanceRemoval) {
+		this.disableInstanceRemoval = disableInstanceRemoval;
+	}
+
+	public static GrounderHeuristicsConfiguration strict() {
+		return new GrounderHeuristicsConfiguration(STRICT_INT, STRICT_INT);
+	}
+	
+	public static GrounderHeuristicsConfiguration lax() {
+		return new GrounderHeuristicsConfiguration(LAX_INT, LAX_INT);
+	}
+	
+	public static GrounderHeuristicsConfiguration getInstance(int toleranceConstraints, int toleranceRules) {
+		return new GrounderHeuristicsConfiguration(toleranceConstraints, toleranceRules);
+	}
+
+	public static GrounderHeuristicsConfiguration getInstance(String toleranceConstraints, String toleranceRules) {
+		return getInstance(parseTolerance(toleranceConstraints), parseTolerance(toleranceRules));
+	}
+
+	private static int parseTolerance(String tolerance) {
+		if (STRICT_STRING.equalsIgnoreCase(tolerance)) {
+			return STRICT_INT;
+		} else if (LAX_STRING.equalsIgnoreCase(tolerance)) {
+			return LAX_INT;
+		} else {
+			return Integer.parseInt(tolerance);
+		}
+	}
+	
+	@Override
+	public String toString() {
+		return this.getClass().getSimpleName() + "(toleranceConstraints=" + toleranceConstraints + ",toleranceRules=" + toleranceRules + ",disableInstanceRemoval=" + disableInstanceRemoval + ")";
+	}
+
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
index 8f17cbe11..c6666b2ba 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java
@@ -2,7 +2,10 @@
 
 import at.ac.tuwien.kr.alpha.common.*;
 import at.ac.tuwien.kr.alpha.common.atoms.*;
-import at.ac.tuwien.kr.alpha.grounder.*;
+import at.ac.tuwien.kr.alpha.grounder.Instance;
+import at.ac.tuwien.kr.alpha.grounder.NonGroundRule;
+import at.ac.tuwien.kr.alpha.grounder.Unification;
+import at.ac.tuwien.kr.alpha.grounder.Unifier;
 import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java
new file mode 100644
index 000000000..8db7941e2
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java
@@ -0,0 +1,31 @@
+package at.ac.tuwien.kr.alpha.grounder.structure;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+
+/**
+ * Stores and provides relationships between ordinary atoms and those that represent choice points.
+ *
+ * Copyright (c) 2019, the Alpha Team.
+ */
+public class AtomChoiceRelation {
+	private final ArrayList<ArrayList<Integer>> atomToChoiceAtoms = new ArrayList<>();
+
+	public void addRelation(int atom, int bodyRepresentingAtom) {
+		while (atom > atomToChoiceAtoms.size() - 1) {
+			atomToChoiceAtoms.add(new ArrayList<>());
+		}
+		atomToChoiceAtoms.get(atom).add(bodyRepresentingAtom);
+	}
+
+	public List<Integer> getRelatedChoiceAtoms(int atom) {
+		return Collections.unmodifiableList(atomToChoiceAtoms.get(atom));
+	}
+
+	public void growForMaxAtomId(int maxAtomId) {
+		while (maxAtomId > atomToChoiceAtoms.size() - 1) {
+			atomToChoiceAtoms.add(new ArrayList<>());
+		}
+	}
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java
index c3111fd84..7ae3cfe7c 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java
@@ -196,8 +196,10 @@ void recomputeActive() {
 				changed = true;
 				LOGGER.debug("Deactivating choice point for atom {}", this.atom);
 			}
-			if (changed && activityListener != null) {
-				activityListener.callbackOnChanged(atom, isActive);
+			if (changed
+				//&& isActive // FIXME: not sure if this should be in, apparently bugs VSIDS.
+				&& activityListener != null) {
+				activityListener.callbackOnChange(atom);
 			}
 		}
 
@@ -207,8 +209,8 @@ public String toString() {
 		}
 	}
 	
-	public static interface ActivityListener {
-		void callbackOnChanged(int atom, boolean active);
+	public interface ActivityListener {
+		void callbackOnChange(int atom);
 	}
 
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java
index 2ee2b11d4..fe1cae973 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java
@@ -67,6 +67,7 @@ public class DefaultSolver extends AbstractSolver implements SolverMaintainingSt
 	private final WritableAssignment assignment;
 
 	private final GroundConflictNoGoodLearner learner;
+	private final MixedRestartStrategy restartStrategy;
 
 	private final BranchingHeuristic branchingHeuristic;
 
@@ -86,10 +87,16 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store,
 		this.store = store;
 		this.choiceManager = new ChoiceManager(assignment, store);
 		this.learner = new GroundConflictNoGoodLearner(assignment, atomStore);
+		LearnedNoGoodDeletion learnedNoGoodDeletion = this.store instanceof NoGoodStoreAlphaRoaming ? ((NoGoodStoreAlphaRoaming)store).getLearnedNoGoodDeletion() : null;
+		if (config.areRestartsEnabled() && this.store instanceof NoGoodStoreAlphaRoaming) {
+			this.restartStrategy = new MixedRestartStrategy(learnedNoGoodDeletion);
+		} else {
+			this.restartStrategy = null;
+		}
 		this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration);
 		this.disableJustifications = config.isDisableJustificationSearch();
 		this.disableNoGoodDeletion = config.isDisableNoGoodDeletion();
-		this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000);
+		this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, restartStrategy, learnedNoGoodDeletion, branchingHeuristic, 1000);
 	}
 
 	private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) {
@@ -148,9 +155,18 @@ protected boolean tryAdvance(Consumer<? super AnswerSet> action) {
 			ConflictCause conflictCause = store.propagate();
 			didChange |= store.didPropagate();
 			LOGGER.trace("Assignment after propagation is: {}", assignment);
-			if (!disableNoGoodDeletion && conflictCause == null) {
-				// Run learned NoGood deletion strategy.
-				store.cleanupLearnedNoGoods();
+			if (conflictCause == null) {
+				if (!disableNoGoodDeletion) {
+					// Run learned NoGood deletion strategy.
+					store.cleanupLearnedNoGoods();
+				}
+				if (restartStrategy != null && restartStrategy.shouldRestart()) {
+					// Restart if necessary.
+					LOGGER.trace("Restarting search.");
+					choiceManager.backjump(0);
+					restartStrategy.onRestart();
+					continue;
+				}
 			}
 			if (conflictCause != null) {
 				// Learn from conflict.
@@ -244,6 +260,9 @@ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) {
 		}
 
 		branchingHeuristic.analyzedConflict(analysisResult);
+		if (restartStrategy != null) {
+			restartStrategy.newConflictWithLbd(analysisResult.lbd);
+		}
 
 		if (analysisResult.learnedNoGood != null) {
 			choiceManager.backjump(analysisResult.backjumpLevel);
@@ -281,7 +300,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()));
@@ -449,6 +468,7 @@ private boolean ingest(Map<Integer, NoGood> obtained) {
 		int maxAtomId = atomStore.getMaxAtomId();
 		store.growForMaxAtomId(maxAtomId);
 		branchingHeuristic.growForMaxAtomId(maxAtomId);
+		choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies());
 		branchingHeuristic.newNoGoods(obtained.values());
 
 		LinkedList<Map.Entry<Integer, NoGood>> noGoodsToAdd = new LinkedList<>(obtained.entrySet());
@@ -498,7 +518,6 @@ private NoGood fixContradiction(Map.Entry<Integer, NoGood> noGoodEntry, Conflict
 	}
 
 	private boolean choose() {
-		choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies());
 		choiceManager.updateAssignments();
 
 		// Hint: for custom heuristics, evaluate them here and pick a value if the heuristics suggests one.
@@ -554,6 +573,11 @@ public int getNumberOfDeletedNoGoods() {
 		return ((NoGoodStoreAlphaRoaming)store).getLearnedNoGoodDeletion().getNumberOfDeletedNoGoods();
 	}
 
+	@Override
+	public NoGoodCounter getNoGoodCounter() {
+		return store.getNoGoodCounter();
+	}
+
 	private void logStats() {
 		if (LOGGER.isDebugEnabled()) {
 			LOGGER.debug(getStatisticsString());
@@ -563,6 +587,9 @@ private void logStats() {
 					LOGGER.debug(heuristicToDecisionCounter.getKey() + ": " + heuristicToDecisionCounter.getValue());
 				}
 			}
+			NoGoodCounter noGoodCounter = store.getNoGoodCounter();
+			LOGGER.debug("Number of NoGoods by type: " + noGoodCounter.getStatsByType());
+			LOGGER.debug("Number of NoGoods by cardinality: " + noGoodCounter.getStatsByCardinality());
 		}
 	}
 }
\ No newline at end of file
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java
index a17264654..d4fa14d4c 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java
@@ -25,6 +25,7 @@ class LearnedNoGoodDeletion {
 	private final NoGoodStoreAlphaRoaming store;
 	private final Assignment assignment;
 	private int conflictCounter;
+	private int totalConflictsCounter;
 	private int cleanupCounter;
 	private int numberOfDeletedNoGoods;
 
@@ -36,6 +37,7 @@ class LearnedNoGoodDeletion {
 	void reset() {
 		learnedNoGoods.clear();
 		conflictCounter = 0;
+		totalConflictsCounter = 0;
 		cleanupCounter = 0;
 		numberOfDeletedNoGoods = 0;
 	}
@@ -62,6 +64,7 @@ boolean needToRunNoGoodDeletion() {
 	}
 
 	void runNoGoodDeletion() {
+		totalConflictsCounter += conflictCounter;
 		conflictCounter = 0;
 		cleanupCounter++;
 		// Reset the sequence after enough growth cycles.
@@ -113,4 +116,8 @@ private boolean isLocked(WatchedNoGood noGood, Assignment assignment) {
 	public int getNumberOfDeletedNoGoods() {
 		return numberOfDeletedNoGoods;
 	}
+
+	int getNumTotalConflicts() {
+		return totalConflictsCounter + conflictCounter;
+	}
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java
new file mode 100644
index 000000000..56cf97125
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java
@@ -0,0 +1,81 @@
+package at.ac.tuwien.kr.alpha.solver;
+
+import static at.ac.tuwien.kr.alpha.Util.oops;
+import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE;
+
+/**
+ * A restart strategy that mixes dynamic restarts and Luby sequence-based restarts.
+ *
+ * Copyright (c) 2019, the Alpha Team.
+ */
+public class MixedRestartStrategy {
+	private final LearnedNoGoodDeletion learnedNoGoodDeletion;
+
+	// Variables for dynamic restarts.
+	private long fast;
+	private long slow;
+	private long currentConflictsLimit;
+	private int numTotalRestarts;
+
+	// Variables for Luby-based restarts.
+	private int un = 1;
+	private int vn = 1;
+	private static final int LUBY_FACTOR = 32;
+	private int lubyLimit = LUBY_FACTOR;
+
+
+	MixedRestartStrategy(LearnedNoGoodDeletion learnedNoGoodDeletion) {
+		this.learnedNoGoodDeletion = learnedNoGoodDeletion;
+		reset();
+	}
+
+	private void reset() {
+		fast = 0;
+		slow = 0;
+		currentConflictsLimit = 50;
+		numTotalRestarts = 0;
+		un = 1;
+		vn = 1;
+	}
+
+	boolean shouldRestart() {
+		long numTotalConflicts = learnedNoGoodDeletion.getNumTotalConflicts();
+		return (numTotalConflicts > currentConflictsLimit && fast / 125 > slow / 100)
+			|| numTotalConflicts > lubyLimit;
+	}
+
+	void onRestart() {
+		currentConflictsLimit = learnedNoGoodDeletion.getNumTotalConflicts() + 50;
+		nextLuby();
+		numTotalRestarts++;
+	}
+
+	void newConflictWithLbd(int lbd) {
+		/// Below is a fast 64-bit fixed point implementation of the following:
+		// slow += (lbd - slow)/(double)(1<<14);
+		// fast += (lbd - fast)/(double)(1<<5);
+		// See Armin Biere's POS'15 slides.
+		if (lbd == LBD_NO_VALUE) {
+			throw oops("Conflict has no LBD value.");
+		}
+		fast -= fast >> 5;
+		fast += lbd << (32 - 5);
+		slow -= slow >> 14;
+		slow += lbd << (32 - 14);
+	}
+
+	int getTotalRestarts() {
+		return numTotalRestarts;
+	}
+
+	private void nextLuby() {
+		// Compute Luby-sequence [Knuth'12]-style.
+		if ((un & -un) == vn) {
+			un++;
+			vn = 1;
+		} else {
+			vn <<= 1;
+		}
+		lubyLimit = vn * LUBY_FACTOR + learnedNoGoodDeletion.getNumTotalConflicts();
+	}
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java
index 5c479b6f0..d80272a94 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java
@@ -1,3 +1,30 @@
+/**
+ * Copyright (c) 2017-2019, the Alpha Team.
+ * All rights reserved.
+ *
+ * Additional changes made by Siemens.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ *
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
 package at.ac.tuwien.kr.alpha.solver;
 
 import at.ac.tuwien.kr.alpha.common.NoGood;
@@ -14,6 +41,7 @@ public class NaiveNoGoodStore implements NoGoodStore {
 
 	private HashMap<Integer, NoGood> delegate = new HashMap<>();
 	private final WritableAssignment assignment;
+	private final NoGoodCounter counter = new NoGoodCounter();
 
 	private boolean hasInferredAssignments;
 
@@ -28,6 +56,7 @@ void clear() {
 
 	@Override
 	public ConflictCause add(int id, NoGood noGood, int lbd) {
+		counter.count(noGood);
 		if (assignment.violates(noGood)) {
 			return new ConflictCause(noGood.asAntecedent());
 		}
@@ -104,6 +133,11 @@ public void backtrack() {
 	public void growForMaxAtomId(int maxAtomId) {
 	}
 
+	@Override
+	public NoGoodCounter getNoGoodCounter() {
+		return counter;
+	}
+
 	@Override
 	public void cleanupLearnedNoGoods() {
 	}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java
new file mode 100644
index 000000000..cba561e2c
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodCounter.java
@@ -0,0 +1,119 @@
+/**
+ * Copyright (c) 2019 Siemens AG
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+package at.ac.tuwien.kr.alpha.solver;
+
+import at.ac.tuwien.kr.alpha.common.NoGood;
+import at.ac.tuwien.kr.alpha.common.NoGood.Type;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * Maintains statistics on numbers of various types of {@link NoGood}s.
+ */
+public class NoGoodCounter {
+
+	private static final int CARD_NARY = 0;
+	private static final int CARD_UNARY = 1;
+	private static final int CARD_BINARY = 2;
+	
+	private int[] countByType = new int[NoGood.Type.values().length];
+	private int[] countByCardinality = new int[3];
+	
+	/**
+	 * Increases counters for the types of the given NoGood
+	 * @param noGood
+	 */
+	void count(NoGood noGood) {
+		countByType[noGood.getType().ordinal()]++;
+		countByCardinality[getAbstractCardinality(noGood)]++;
+	}
+
+	private int getAbstractCardinality(NoGood noGood) {
+		if (noGood.isUnary()) {
+			return CARD_UNARY;
+		}
+		if (noGood.isBinary()) {
+			return CARD_BINARY;
+		}
+		return CARD_NARY;
+	}
+	
+	/**
+	 * @param type
+	 * @return the number of nogoods of the given type
+	 */
+	public int getNumberOfNoGoods(NoGood.Type type) {
+		return countByType[type.ordinal()];
+	}
+	
+	/**
+	 * @return the number of unary nogoods
+	 */
+	public int getNumberOfUnaryNoGoods() {
+		return countByCardinality[CARD_UNARY];
+	}
+	
+	/**
+	 * @return the number of binary nogoods
+	 */
+	public int getNumberOfBinaryNoGoods() {
+		return countByCardinality[CARD_BINARY];
+	}
+	
+	/**
+	 * @return the number of nogoods that are neither unary nor binary
+	 */
+	public int getNumberOfNAryNoGoods() {
+		return countByCardinality[CARD_NARY];
+	}
+	
+	/**
+	 * @return {@code true} iff there is at least one binary nogood
+	 */
+	public boolean hasBinaryNoGoods() {
+		return countByCardinality[CARD_BINARY] > 0;
+	}
+
+	/**
+	 * @return a string giving statistics on numbers of nogoods by type
+	 */
+	public String getStatsByType() {
+		List<String> statsList = new ArrayList<>(Type.values().length);
+		for (Type type : Type.values()) {
+			statsList.add(type.name() + ": " + countByType[type.ordinal()]);
+		}
+		return String.join(" ", statsList);
+	}
+
+	/**
+	 * @return a string giving statistics on numbers of nogoods by cardinality
+	 */
+	public String getStatsByCardinality() {
+		return "unary: " + getNumberOfUnaryNoGoods() + " binary: " + getNumberOfBinaryNoGoods() + " larger: " + getNumberOfNAryNoGoods();
+	}
+	
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java
index 3b3b184cd..7cd516b40 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java
@@ -53,4 +53,6 @@ public interface NoGoodStore {
 	 * necessary.
 	 */
 	void cleanupLearnedNoGoods();
+
+	NoGoodCounter getNoGoodCounter();
 }
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java
index 95e4e0aef..453b45a3a 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java
@@ -70,6 +70,8 @@ public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropaga
 	private boolean didPropagate;
 	private boolean hasBinaryNoGoods;
 
+	private final NoGoodCounter counter = new NoGoodCounter();
+
 	public NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) {
 		this.assignment = assignment;
 		this.checksEnabled = checksEnabled;
@@ -133,6 +135,11 @@ public void growForMaxAtomId(int maxAtomId) {
 		this.maxAtomId = maxAtomId;
 	}
 
+	@Override
+	public NoGoodCounter getNoGoodCounter() {
+		return counter;
+	}
+
 	@Override
 	public void cleanupLearnedNoGoods() {
 		if (learnedNoGoodDeletion.needToRunNoGoodDeletion()) {
@@ -173,6 +180,7 @@ private void addAlphaWatch(WatchedNoGood wng) {
 	@Override
 	public ConflictCause add(int id, NoGood noGood, int lbd) {
 		LOGGER.trace("Adding {}", noGood);
+		counter.count(noGood);
 
 		if (noGood.isUnary()) {
 			return addUnary(noGood);
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java
index 9c4d74601..a84b45c69 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java
@@ -25,28 +25,39 @@
  */
 package at.ac.tuwien.kr.alpha.solver;
 
+import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristic;
+import at.ac.tuwien.kr.alpha.solver.heuristics.ChainedBranchingHeuristics;
+import at.ac.tuwien.kr.alpha.solver.heuristics.VSIDSWithPhaseSaving;
 import org.slf4j.Logger;
 
 /**
- * Collects performance data (mainly number of decisions per second) and outputs them on demand.
+ * Collects performance data and outputs them on demand.
+ *
+ * Copyright (c) 2019, the Alpha Team.
  */
 public class PerformanceLog {
 
-	private ChoiceManager choiceManager;
-	private TrailAssignment assignment;
+	private final ChoiceManager choiceManager;
+	private final TrailAssignment assignment;
+	private final MixedRestartStrategy restartStrategy;
+	private final LearnedNoGoodDeletion learnedNoGoodDeletion;
+	private final BranchingHeuristic branchingHeuristic;
 	private long msBetweenOutputs;
 	
 	private Long timeFirstEntry;
 	private Long timeLastPerformanceLog;
 	private int numberOfChoicesLastPerformanceLog;
+	private int numberOfRestartsLastPerformanceLog;
+	private int numberOfConflictsLastPerformanceLog;
+	private int numberOfDeletedNoGoodsLastPerformanceLog;
 
-	/**
-	 * @param msBetweenOutputs
-	 */
-	public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, long msBetweenOutputs) {
+	public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, MixedRestartStrategy restartStrategy, LearnedNoGoodDeletion learnedNoGoodDeletion, BranchingHeuristic branchingHeuristic, long msBetweenOutputs) {
 		super();
 		this.choiceManager = choiceManager;
 		this.assignment = assignment;
+		this.restartStrategy = restartStrategy;
+		this.learnedNoGoodDeletion = learnedNoGoodDeletion;
+		this.branchingHeuristic = branchingHeuristic;
 		this.msBetweenOutputs = msBetweenOutputs;
 	}
 
@@ -60,14 +71,51 @@ public void initialize() {
 	 */
 	public void infoIfTimeForOutput(Logger logger) {
 		long currentTime = System.currentTimeMillis();
+		if (currentTime < timeLastPerformanceLog + msBetweenOutputs) {
+			return;
+		}
 		int currentNumberOfChoices = choiceManager.getChoices();
-		if (currentTime >= timeLastPerformanceLog + msBetweenOutputs) {
-			logger.info("Decisions in {}s: {}", (currentTime - timeLastPerformanceLog) / 1000.0f, currentNumberOfChoices - numberOfChoicesLastPerformanceLog);
-			timeLastPerformanceLog = currentTime;
-			numberOfChoicesLastPerformanceLog = currentNumberOfChoices;
-			float overallTime = (currentTime - timeFirstEntry) / 1000.0f;
-			float decisionsPerSec = currentNumberOfChoices / overallTime;
-			logger.info("Overall performance: {} decisions in {}s or {} decisions per sec. Overall replayed assignments: {}.", currentNumberOfChoices, overallTime, decisionsPerSec, assignment.replayCounter);
+		float timeSinceLastLog = (currentTime - timeLastPerformanceLog) / 1000.0f;
+		logger.info("Decisions in {}s: {}", timeSinceLastLog, currentNumberOfChoices - numberOfChoicesLastPerformanceLog);
+		timeLastPerformanceLog = currentTime;
+		numberOfChoicesLastPerformanceLog = currentNumberOfChoices;
+		float overallTime = (currentTime - timeFirstEntry) / 1000.0f;
+		float decisionsPerSec = currentNumberOfChoices / overallTime;
+		logger.info("Overall performance: {} decisions in {}s or {} decisions per sec. Overall replayed assignments: {}.", currentNumberOfChoices, overallTime, decisionsPerSec, assignment.replayCounter);
+		if (restartStrategy != null) {
+			int totalRestarts = restartStrategy.getTotalRestarts();
+			int currentNumberOfRestarts = totalRestarts - numberOfRestartsLastPerformanceLog;
+			logStatsPerTime(logger, "Restarts", timeSinceLastLog, overallTime, totalRestarts, currentNumberOfRestarts);
+			numberOfRestartsLastPerformanceLog = totalRestarts;
+		}
+		if (branchingHeuristic != null && branchingHeuristic instanceof ChainedBranchingHeuristics) {
+			BranchingHeuristic firstHeuristic = ((ChainedBranchingHeuristics) branchingHeuristic).getFirstElement();
+			if (firstHeuristic instanceof VSIDSWithPhaseSaving) {
+				VSIDSWithPhaseSaving vsidsWithPhaseSaving = (VSIDSWithPhaseSaving) firstHeuristic;
+				long numThrownAway = vsidsWithPhaseSaving.getNumThrownAway();
+				long numNoChoicePoint = vsidsWithPhaseSaving.getNumNoChoicePoint();
+				long numNotActiveChoicePoint = vsidsWithPhaseSaving.getNumNotActiveChoicePoint();
+				double activityDecrease = vsidsWithPhaseSaving.getActivityDecrease();
+				logger.info("Heuristic threw away {} preferred choices ({} no choice, {} not active choice points) averaging {} thrown away per choice done.", numThrownAway, numNoChoicePoint, numNotActiveChoicePoint, (float) numThrownAway / currentNumberOfChoices);
+				logger.info("HeapOfActiveAtoms had {} choices added due to increased activity.", vsidsWithPhaseSaving.getNumAddedToHeapByActivity());
+				logger.info("Atom activity decreased overall by {} or {} per choice on average", activityDecrease, activityDecrease / currentNumberOfChoices);
+			}
 		}
+		if (learnedNoGoodDeletion != null) {
+			int totalConflicts = learnedNoGoodDeletion.getNumTotalConflicts();
+			int currentNumConflicts = totalConflicts - numberOfConflictsLastPerformanceLog;
+			int totalDeletedNogoods = learnedNoGoodDeletion.getNumberOfDeletedNoGoods();
+			int currenDeletedNoGoods = totalDeletedNogoods - numberOfDeletedNoGoodsLastPerformanceLog;
+			logStatsPerTime(logger, "Conflicts", timeSinceLastLog, overallTime, totalConflicts, currentNumConflicts);
+			logStatsPerTime(logger, "Deleted NoGoods", timeSinceLastLog, overallTime, totalDeletedNogoods, currenDeletedNoGoods);
+			numberOfConflictsLastPerformanceLog = totalConflicts;
+			numberOfDeletedNoGoodsLastPerformanceLog = totalDeletedNogoods;
+		}
+	}
+
+	private void logStatsPerTime(Logger logger, String statName, float timeSinceLastLog, float overallTime, int total, int differenceSinceLast) {
+		logger.info(statName + " in {}s: {}", timeSinceLastLog, differenceSinceLast);
+		logger.info("Overall performance: {} " + statName + " in {}s or {} " + statName + " per sec", total, overallTime, total / overallTime);
+
 	}
 }
\ No newline at end of file
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java
index 36bbe668d..755ad8012 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java
@@ -32,6 +32,7 @@
 import at.ac.tuwien.kr.alpha.grounder.Grounder;
 import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfigurationBuilder;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 
 import java.util.Random;
 
@@ -42,7 +43,9 @@ public static Solver getInstance(SystemConfig config, AtomStore atomStore, Groun
 		final Random random = new Random(config.getSeed());
 		final boolean debugInternalChecks = config.isDebugInternalChecks();
 		final HeuristicsConfiguration heuristicsConfiguration = buildHeuristicsConfiguration(config);
-		final WritableAssignment assignment = new TrailAssignment(atomStore, debugInternalChecks);
+		final PhaseInitializerFactory.PhaseInitializer phaseInitializer =
+			PhaseInitializerFactory.getInstance(config.getPhaseInitializerName(), random);
+		final WritableAssignment assignment = new TrailAssignment(atomStore, phaseInitializer, debugInternalChecks);
 
 		NoGoodStore store;
 
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java
index 861830582..0c29abef7 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java
@@ -46,6 +46,8 @@ public interface SolverMaintainingStatistics {
 	 */
 	int getNumberOfConflictsAfterClosing();
 
+	NoGoodCounter getNoGoodCounter();
+
 	default String getStatisticsString() {
 		return "g=" + getNumberOfChoices() + ", bt=" + getNumberOfBacktracks() + ", bj=" + getNumberOfBackjumps() + ", bt_within_bj="
 				+ getNumberOfBacktracksWithinBackjumps() + ", mbt=" + getNumberOfBacktracksDueToRemnantMBTs() + ", cac=" + getNumberOfConflictsAfterClosing()
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java
index 9c4640d01..be87a0730 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java
@@ -30,6 +30,7 @@
 import at.ac.tuwien.kr.alpha.common.Assignment;
 import at.ac.tuwien.kr.alpha.common.AtomStore;
 import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -49,7 +50,7 @@
  */
 public class TrailAssignment implements WritableAssignment, Checkable {
 	private static final Logger LOGGER = LoggerFactory.getLogger(TrailAssignment.class);
-	public static final Antecedent CLOSING_INDICATOR_ANTECEDENT = new Antecedent() {
+	static final Antecedent CLOSING_INDICATOR_ANTECEDENT = new Antecedent() {
 		int[] literals = new int[0];
 
 		@Override
@@ -69,6 +70,7 @@ public void decreaseActivity() {
 
 	private final AtomStore atomStore;
 	private ChoiceManager choiceManagerCallback;
+	private final PhaseInitializerFactory.PhaseInitializer phaseInitializer;
 
 	/**
 	 * Contains for each known atom a value whose two least
@@ -81,6 +83,8 @@ public void decreaseActivity() {
 	private int[] strongDecisionLevels;
 	private Antecedent[] impliedBy;
 	private boolean[] callbackUponChange;
+	private boolean[] phase;
+	private boolean[] hasPhaseSet;
 	private ArrayList<OutOfOrderLiteral> outOfOrderLiterals = new ArrayList<>();
 	private int highestDecisionLevelContainingOutOfOrderLiterals;
 	private ArrayList<Integer> trail = new ArrayList<>();
@@ -94,13 +98,16 @@ public void decreaseActivity() {
 	private boolean checksEnabled;
 	int replayCounter;
 
-	public TrailAssignment(AtomStore atomStore, boolean checksEnabled) {
+	public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitializer phaseInitializer, boolean checksEnabled) {
+		this.phaseInitializer = phaseInitializer;
 		this.checksEnabled = checksEnabled;
 		this.atomStore = atomStore;
 		this.values = new int[0];
 		this.strongDecisionLevels = new int[0];
 		this.impliedBy = new Antecedent[0];
 		this.callbackUponChange = new boolean[0];
+		this.phase = new boolean[0];
+		this.hasPhaseSet = new boolean[0];
 		this.trailIndicesOfDecisionLevels.add(0);
 		nextPositionInTrail = 0;
 		newAssignmentsIterator = 0;
@@ -108,8 +115,8 @@ public TrailAssignment(AtomStore atomStore, boolean checksEnabled) {
 		assignmentsForChoicePosition = 0;
 	}
 
-	public TrailAssignment(AtomStore atomStore) {
-		this(atomStore, false);
+	public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitializer phaseInitializer) {
+		this(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue(), false);
 	}
 
 	@Override
@@ -119,6 +126,8 @@ public void clear() {
 		Arrays.fill(strongDecisionLevels, -1);
 		Arrays.fill(impliedBy, null);
 		Arrays.fill(callbackUponChange, false);
+		Arrays.fill(phase, false);
+		Arrays.fill(hasPhaseSet, false);
 		outOfOrderLiterals = new ArrayList<>();
 		highestDecisionLevelContainingOutOfOrderLiterals = 0;
 		trail = new ArrayList<>();
@@ -142,7 +151,7 @@ public void setCallback(ChoiceManager choiceManager) {
 
 	@Override
 	public boolean isAssigned(int atom) {
-		return values[atom] != 0;
+		return values.length > atom && values[atom] != 0;
 	}
 
 	@Override
@@ -353,6 +362,8 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent im
 			trail.add(atomToLiteral(atom, value.toBoolean()));
 			values[atom] = (getDecisionLevel() << 2) | translateTruth(value);
 			this.impliedBy[atom] = impliedBy;
+			this.phase[atom] = value.toBoolean();
+			this.hasPhaseSet[atom] = true;
 			// Adjust MBT counter.
 			if (value == MBT) {
 				mbtCount++;
@@ -445,6 +456,14 @@ public Antecedent getImpliedBy(int atom) {
 		return impliedBy[atom];
 	}
 
+	@Override
+	public boolean getLastValue(int atom) {
+		if (hasPhaseSet[atom]) {
+			return phase[atom];
+		}
+		return phaseInitializer.getNextInitialPhase();
+	}
+
 	@Override
 	public Set<Integer> getTrueAssignments() {
 		Set<Integer> result = new HashSet<>();
@@ -533,6 +552,8 @@ public void growForMaxAtomId() {
 		strongDecisionLevels = Arrays.copyOf(strongDecisionLevels, newCapacity);
 		Arrays.fill(strongDecisionLevels, oldLength, strongDecisionLevels.length, -1);
 		impliedBy = Arrays.copyOf(impliedBy, newCapacity);
+		phase = Arrays.copyOf(phase, newCapacity);
+		hasPhaseSet = Arrays.copyOf(hasPhaseSet, newCapacity);
 		callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity);
 	}
 
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java
index 74fa5352a..ee87890d4 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java
@@ -6,7 +6,7 @@
 import java.util.Iterator;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
-import static at.ac.tuwien.kr.alpha.common.Literals.*;
+import static at.ac.tuwien.kr.alpha.common.Literals.literalToString;
 
 public final class WatchedNoGood implements NoGoodInterface, Antecedent, Iterable<Integer> {
 	private int activity;
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java
index 52df83cd4..06d8cf20e 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java
@@ -36,6 +36,8 @@
 import java.util.Set;
 import java.util.stream.Stream;
 
+import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral;
+
 /**
  * A variant of {@link DependencyDrivenHeuristic} that prefers to choose atoms representing bodies of rules whose heads
  * are assigned {@link at.ac.tuwien.kr.alpha.solver.ThriceTruth#MBT}.
@@ -60,7 +62,7 @@ public int chooseLiteral() {
 				.max(Comparator.comparingDouble(bodyActivity::get));
 		if (mostActiveBody.isPresent()) {
 			rememberedAtom = mostActiveBody.get();
-			return rememberedAtom;
+			return atomToLiteral(rememberedAtom);
 		}
 		return super.chooseLiteral();
 	}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java
index b54cfdd53..93a23f018 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java
@@ -26,6 +26,7 @@
 package at.ac.tuwien.kr.alpha.solver.heuristics;
 
 import at.ac.tuwien.kr.alpha.grounder.Grounder;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import at.ac.tuwien.kr.alpha.solver.ChoiceManager;
 import at.ac.tuwien.kr.alpha.solver.WritableAssignment;
 import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProviderFactory.BodyActivityType;
@@ -56,7 +57,8 @@ public enum Heuristic {
 		ALPHA_ACTIVE_RULE,
 		ALPHA_HEAD_MBT,
 		VSIDS,
-		GDD_VSIDS;
+		GDD_VSIDS,
+		VSIDS_PHASE_SAVING;
 
 		/**
 		 * @return a comma-separated list of names of known heuristics
@@ -117,6 +119,9 @@ private static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfigurati
 			return new VSIDS(assignment, choiceManager, heuristicsConfiguration.getMomsStrategy());
 		case GDD_VSIDS:
 			return new DependencyDrivenVSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy());
+		case VSIDS_PHASE_SAVING:
+			AtomChoiceRelation atomChoiceRelation = grounder.getAtomChoiceRelation();
+			return new VSIDSWithPhaseSaving(assignment, choiceManager, atomChoiceRelation, heuristicsConfiguration.getMomsStrategy());
 		}
 		throw new IllegalArgumentException("Unknown branching heuristic requested.");
 	}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java
index b8cfb0919..56ed9660d 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java
@@ -1,17 +1,17 @@
 /**
  * Copyright (c) 2018-2019 Siemens AG
  * All rights reserved.
- * 
+ *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
- * 
+ *
  * 1) Redistributions of source code must retain the above copyright notice, this
  *    list of conditions and the following disclaimer.
- * 
+ *
  * 2) Redistributions in binary form must reproduce the above copyright notice,
  *    this list of conditions and the following disclaimer in the documentation
  *    and/or other materials provided with the distribution.
- * 
+ *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
@@ -28,10 +28,7 @@
 import at.ac.tuwien.kr.alpha.common.NoGood;
 import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult;
 
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
 
@@ -96,6 +93,9 @@ public void add(BranchingHeuristic element) {
 			throw oops("Cycle detected in chain of branching heuristics");
 		}
 		chain.add(element);
+		if (decisionCounters != null) {
+			decisionCounters = Arrays.copyOf(decisionCounters, decisionCounters.length + 1);
+		}
 	}
 
 	public BranchingHeuristic getLastElement() {
@@ -106,6 +106,10 @@ public static ChainedBranchingHeuristics chainOf(BranchingHeuristic... branching
 		return new ChainedBranchingHeuristics(branchingHeuristics);
 	}
 
+	public BranchingHeuristic getFirstElement() {
+		return chain.get(0);
+	}
+
 	/**
 	 * Returns a mapping from individual heuristics to number of decisions made by them.
 	 */
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java
index 5ff32fc06..5182c0948 100644
--- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java
@@ -38,6 +38,7 @@
 import java.util.Comparator;
 import java.util.PriorityQueue;
 
+import static at.ac.tuwien.kr.alpha.Util.arrayGrowthSize;
 import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
 
 /**
@@ -53,22 +54,24 @@ public class HeapOfActiveAtoms {
 
 	private static final double NORMALIZATION_THRESHOLD = 1E100;
 	private static final double INCREMENT_TO_AVOID_DENORMALS = Double.MIN_VALUE * NORMALIZATION_THRESHOLD;
-	private static final double SCORE_EPSILON = 1E-100;
+	static final double SCORE_EPSILON = 1E-100;
 
-	private boolean[] incrementedActivityScores = new boolean[0];
-	protected double[] activityScores = new double[0];
-	protected final PriorityQueue<Integer> heap = new PriorityQueue<>(new AtomActivityComparator().reversed());
+	boolean[] incrementedActivityScores = new boolean[0];
+	boolean[] occursInHeap = new boolean[0];
+	double[] activityScores = new double[0];
+	final PriorityQueue<Integer> heap = new PriorityQueue<>(new AtomActivityComparator().reversed());
 
 	protected ChoiceManager choiceManager;
 	private int decayPeriod;
 	private double decayFactor;
 	private int stepsSinceLastDecay;
 	private double currentActivityIncrement = 1.0;
-	private int numberOfNormalizations;
+	int numberOfNormalizations;
+	private long numAddedToHeapByActivity;
 	
-	private final MOMs moms;
+	final MOMs moms;
 
-	public HeapOfActiveAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager) {
+	HeapOfActiveAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager) {
 		this.decayPeriod = decayPeriod;
 		this.decayFactor = decayFactor;
 		this.choiceManager = choiceManager;
@@ -102,6 +105,10 @@ public double getDecayFactor() {
 		return decayFactor;
 	}
 
+	double getCurrentActivityIncrement() {
+		return currentActivityIncrement;
+	}
+
 	/**
 	 * @see #getDecayFactor()
 	 */
@@ -144,7 +151,7 @@ protected void analyzeNewNoGood(NoGood newNoGood) {
 	/**
 	 * Computes and stores initial activity values for the atoms occurring in the given nogood.
 	 */
-	protected void initActivity(NoGood newNoGood) {
+	private void initActivity(NoGood newNoGood) {
 		if (moms != null) {
 			initActivityMOMs(newNoGood);
 		} else {
@@ -159,7 +166,7 @@ protected void initActivity(NoGood newNoGood) {
 	 * 1.01 is added to avoid computing the logarithm of a number between 0 and 1 (input scores have to be greater or equal to 0!)
 	 * @param newNoGood a new nogood, the atoms occurring in which will be initialized
 	 */
-	private void initActivityMOMs(NoGood newNoGood) {
+	protected void initActivityMOMs(NoGood newNoGood) {
 		LOGGER.debug("Initializing activity scores with MOMs");
 		for (int literal : newNoGood) {
 			int atom = atomOf(literal);
@@ -181,6 +188,19 @@ private void initActivityMOMs(NoGood newNoGood) {
 	void growToCapacity(int newCapacity) {
 		activityScores = Arrays.copyOf(activityScores, newCapacity);
 		incrementedActivityScores = Arrays.copyOf(incrementedActivityScores, newCapacity);
+		occursInHeap = Arrays.copyOf(occursInHeap, newCapacity);
+	}
+
+	void growForMaxAtomId(int maxAtomId) {
+		// Grow arrays only if needed.
+		if (activityScores.length > maxAtomId) {
+			return;
+		}
+		int newCapacity = arrayGrowthSize(activityScores.length);
+		if (newCapacity < maxAtomId + 1) {
+			newCapacity = maxAtomId + 1;
+		}
+		growToCapacity(newCapacity);
 	}
 
 	private void initActivityNaive(NoGood newNoGood) {
@@ -194,8 +214,12 @@ private void initActivityNaive(NoGood newNoGood) {
 	/**
 	 * Returns the atom with the highest activity score and removes it from the heap.
 	 */
-	public Integer getMostActiveAtom() {
-		return heap.poll();
+	Integer getMostActiveAtom() {
+		Integer mostActiveAtom = heap.poll();
+		if (mostActiveAtom != null) {
+			occursInHeap[mostActiveAtom] = false;
+		}
+		return mostActiveAtom;
 	}
 
 	/**
@@ -204,7 +228,7 @@ public Integer getMostActiveAtom() {
 	 * by adding to it the current activity increment times the increment factor.
 	 * If the new value exceeds a certain threshold, all activity scores are normalized.
 	 */
-	public void incrementActivity(int atom) {
+	void incrementActivity(int atom) {
 		incrementActivity(atom, currentActivityIncrement);
 	}
 	
@@ -215,7 +239,7 @@ protected void incrementActivity(int atom, double increment) {
 		incrementedActivityScores[atom] = true;
 	}
 
-	private void setActivity(int atom, double newActivity) {
+	void setActivity(int atom, double newActivity) {
 		activityScores[atom] = newActivity;
 		LOGGER.trace("Activity of atom {} set to {}", atom, newActivity);
 
@@ -223,7 +247,11 @@ private void setActivity(int atom, double newActivity) {
 			normalizeActivityScores();
 		}
 
-		heap.add(atom); // ignores the fact that atom may already be in the heap for performance reasons (may be revised in future)
+		if (choiceManager.isActiveChoiceAtom(atom)) {
+			numAddedToHeapByActivity++;
+			occursInHeap[atom] = true;
+			heap.add(atom); // ignores the fact that atom may already be in the heap for performance reasons (may be revised in future)
+		}
 	}
 
 	/**
@@ -240,13 +268,17 @@ private void normalizeActivityScores() {
 		}
 	}
 
-	private double normalizeNewActivityScore(double newActivity) {
+	double normalizeNewActivityScore(double newActivity) {
 		for (int i = 0; i < numberOfNormalizations; i++) {
 			newActivity = (newActivity + INCREMENT_TO_AVOID_DENORMALS) / NORMALIZATION_THRESHOLD;
 		}
 		return newActivity;
 	}
 
+	long getNumAddedToHeapByActivity() {
+		return numAddedToHeapByActivity;
+	}
+
 	private class AtomActivityComparator implements Comparator<Integer> {
 
 		@Override
@@ -259,19 +291,18 @@ public int compare(Integer a1, Integer a2) {
 	private class ChoicePointActivityListener implements ChoiceInfluenceManager.ActivityListener {
 
 		@Override
-		public void callbackOnChanged(int atom, boolean active) {
-			if (active && choiceManager.isActiveChoiceAtom(atom)) {
-				if (atom < activityScores.length) {
-					/* if atom has no activity score, probably the atom is still being buffered
-					   by DependencyDrivenVSIDSHeuristic and will get an initial activity
-					   when the buffer is ingested */
-					heap.add(atom);
-				}
+		public void callbackOnChange(int atom) {
+			if (!occursInHeap[atom] && atom < activityScores.length) {
+				/* if atom has no activity score, probably the atom is still being buffered
+				   by DependencyDrivenVSIDSHeuristic and will get an initial activity
+				   when the buffer is ingested */
+				occursInHeap[atom] = true;
+				heap.add(atom);
 			}
 		}
 	}
 
-	public void setMOMsStrategy(BinaryNoGoodPropagationEstimation.Strategy momsStrategy) {
+	void setMOMsStrategy(BinaryNoGoodPropagationEstimation.Strategy momsStrategy) {
 		if (moms != null) {
 			moms.setStrategy(momsStrategy);
 		}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java
new file mode 100644
index 000000000..28dc52f31
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java
@@ -0,0 +1,42 @@
+package at.ac.tuwien.kr.alpha.solver.heuristics;
+
+import at.ac.tuwien.kr.alpha.common.NoGood;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
+import at.ac.tuwien.kr.alpha.solver.ChoiceManager;
+
+import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
+
+/**
+ * A heap of active choice points that uses {@link AtomChoiceRelation} for initializing activities of related choice points.
+ *
+ * Copyright (c) 2019, the Alpha Team.
+ */
+public class HeapOfRelatedChoiceAtoms extends HeapOfActiveAtoms {
+	private final AtomChoiceRelation atomChoiceRelation;
+
+	HeapOfRelatedChoiceAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation) {
+		super(decayPeriod, decayFactor, choiceManager);
+		this.atomChoiceRelation = atomChoiceRelation;
+	}
+
+	@Override
+	protected void initActivityMOMs(NoGood newNoGood) {
+		LOGGER.debug("Initializing activity scores with MOMs");
+		for (int literal : newNoGood) {
+			for (Integer relatedChoiceAtom : atomChoiceRelation.getRelatedChoiceAtoms(atomOf(literal))) {
+				if (!incrementedActivityScores[relatedChoiceAtom]) { // update initial value as long as not incremented yet by VSIDS
+					double score = moms.getScore(relatedChoiceAtom);
+					if (score > 0.0) {
+						double newActivity = 1 - 1 / (Math.log(score + 1.01));
+						if (newActivity - activityScores[relatedChoiceAtom] > SCORE_EPSILON) {        // avoid computation overhead if score does not increase
+							if (numberOfNormalizations > 0) {
+								newActivity = normalizeNewActivityScore(newActivity);
+							}
+							setActivity(relatedChoiceAtom, newActivity);
+						}
+					}
+				}
+			}
+		}
+	}
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java
new file mode 100644
index 000000000..095f1435f
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java
@@ -0,0 +1,57 @@
+package at.ac.tuwien.kr.alpha.solver.heuristics;
+
+import java.util.Random;
+
+/**
+ * Factory returning atom phase initializers, which determine the initial phase given to atoms that were previously
+ * unassigned.
+ *
+ * Copyright (c) 2019, the Alpha Team.
+ */
+public abstract class PhaseInitializerFactory {
+
+	public abstract static class PhaseInitializer {
+		public abstract boolean getNextInitialPhase();
+	}
+
+	public static PhaseInitializer getInstance(String phaseInitializerName, Random random) {
+		switch (phaseInitializerName.toLowerCase()) {
+			case "alltrue":
+				return getPhaseInitializerAllTrue();
+			case "allfalse":
+				return getPhaseInitializerAllFalse();
+			case "random":
+				return getPhaseInitializerRandom(random);
+			default:
+				throw new IllegalArgumentException("Unknown phase initializer requested:" + phaseInitializerName);
+		}
+	}
+
+	public static PhaseInitializer getPhaseInitializerAllTrue() {
+		return new PhaseInitializer() {
+			@Override
+			public boolean getNextInitialPhase() {
+				return true;
+			}
+		};
+	}
+
+	private static PhaseInitializer getPhaseInitializerAllFalse() {
+		return new PhaseInitializer() {
+			@Override
+			public boolean getNextInitialPhase() {
+				return false;
+			}
+		};
+	}
+
+	private static PhaseInitializer getPhaseInitializerRandom(Random random) {
+		return new PhaseInitializer() {
+			private final Random rand = random;
+			@Override
+			public boolean getNextInitialPhase() {
+				return rand.nextBoolean();
+			}
+		};
+	}
+}
diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java
new file mode 100644
index 000000000..c5d35da34
--- /dev/null
+++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java
@@ -0,0 +1,226 @@
+/**
+ * Copyright (c) 2018-2019 Siemens AG
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+package at.ac.tuwien.kr.alpha.solver.heuristics;
+
+import at.ac.tuwien.kr.alpha.common.Assignment;
+import at.ac.tuwien.kr.alpha.common.NoGood;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
+import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation;
+import at.ac.tuwien.kr.alpha.solver.ChoiceManager;
+import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
+import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.util.ArrayList;
+import java.util.Collection;
+
+import static at.ac.tuwien.kr.alpha.Util.oops;
+import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
+import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral;
+
+/**
+ * This implementation is like {@link VSIDS} but uses the saved phase for the truth of the chosen atom.
+ *
+ * Copyright (c) 2019, the Alpha Team.
+ */
+public class VSIDSWithPhaseSaving implements ActivityBasedBranchingHeuristic {
+	protected static final Logger LOGGER = LoggerFactory.getLogger(VSIDSWithPhaseSaving.class);
+
+	private static final int DEFAULT_DECAY_PERIOD = 1;
+
+	/**
+	 * The default factor by which VSID's activity increment will be multiplied when the decay period has expired.
+	 * The value is taken from clasp's tweety configuration which clasp uses by default.
+	 */
+	private static final double DEFAULT_DECAY_FACTOR = 1 / 0.92;
+
+	protected final Assignment assignment;
+	protected final ChoiceManager choiceManager;
+	private final AtomChoiceRelation atomChoiceRelation;
+	private final HeapOfActiveAtoms heapOfActiveAtoms;
+	private final Collection<NoGood> bufferedNoGoods = new ArrayList<>();
+
+	private double activityDecrease;
+	private long numThrownAway;
+	private long numNoChoicePoint;
+	private long numNotActiveChoicePoint;
+
+	private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) {
+		this.assignment = assignment;
+		this.choiceManager = choiceManager;
+		this.atomChoiceRelation = atomChoiceRelation;
+		this.heapOfActiveAtoms = heapOfActiveAtoms;
+		this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy);
+	}
+
+	private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) {
+		this(assignment, choiceManager, atomChoiceRelation, new HeapOfRelatedChoiceAtoms(decayPeriod, decayFactor, choiceManager, atomChoiceRelation),  momsStrategy);
+	}
+
+	VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) {
+		this(assignment, choiceManager, atomChoiceRelation, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR,  momsStrategy);
+	}
+
+	@Override
+	public void violatedNoGood(NoGood violatedNoGood) {
+	}
+
+	@Override
+	public void analyzedConflict(ConflictAnalysisResult analysisResult) {
+		ingestBufferedNoGoods();	//analysisResult may contain new atoms whose activity must be initialized
+		for (int resolutionAtom : analysisResult.resolutionAtoms) {
+			incrementActivityOfRelatedChoiceAtoms(resolutionAtom);
+		}
+		if (analysisResult.learnedNoGood != null) {
+			for (int literal : analysisResult.learnedNoGood) {
+				incrementActivityOfRelatedChoiceAtoms(atomOf(literal));
+			}
+		}
+		heapOfActiveAtoms.decayIfTimeHasCome();
+	}
+
+	private void incrementActivityOfRelatedChoiceAtoms(int toAtom) {
+		if (atomChoiceRelation == null) {
+			heapOfActiveAtoms.incrementActivity(toAtom);
+			return;
+		}
+		for (Integer relatedChoiceAtom : atomChoiceRelation.getRelatedChoiceAtoms(toAtom)) {
+			if (!choiceManager.isAtomChoice(relatedChoiceAtom)) {
+				throw oops("Related atom is no choice.");
+			}
+			heapOfActiveAtoms.incrementActivity(relatedChoiceAtom);
+		}
+	}
+
+	@Override
+	public void newNoGood(NoGood newNoGood) {
+		this.bufferedNoGoods.add(newNoGood);
+	}
+
+	@Override
+	public void newNoGoods(Collection<NoGood> newNoGoods) {
+		this.bufferedNoGoods.addAll(newNoGoods);
+	}
+
+	private void ingestBufferedNoGoods() {
+		heapOfActiveAtoms.newNoGoods(bufferedNoGoods);
+		bufferedNoGoods.clear();
+	}
+
+	public double getActivityDecrease() {
+		return activityDecrease;
+	}
+
+	public long getNumThrownAway() {
+		return numThrownAway;
+	}
+
+	public long getNumNoChoicePoint() {
+		return numNoChoicePoint;
+	}
+
+	public long getNumNotActiveChoicePoint() {
+		return numNotActiveChoicePoint;
+	}
+
+	public long getNumAddedToHeapByActivity() {
+		return heapOfActiveAtoms.getNumAddedToHeapByActivity();
+	}
+
+	/**
+	 * {@link VSIDSWithPhaseSaving} works like {@link VSIDS} for selecting an atom but uses the saved phase to
+	 * determine the truth value to choose.
+	 */
+	@Override
+	public int chooseLiteral() {
+		int atom = chooseAtom();
+		if (atom == DEFAULT_CHOICE_ATOM) {
+			return DEFAULT_CHOICE_LITERAL;
+		}
+		boolean sign = chooseSign(atom);
+		return atomToLiteral(atom, sign);
+	}
+
+	private int chooseAtom() {
+		ingestBufferedNoGoods();
+		Integer mostActiveAtom;
+		double maxActivity = 0.0f;
+		while ((mostActiveAtom = heapOfActiveAtoms.getMostActiveAtom()) != null) {
+			double activity = heapOfActiveAtoms.getActivity(atomToLiteral(mostActiveAtom));
+			if (activity > maxActivity) {
+				maxActivity = activity;
+			}
+			if (choiceManager.isActiveChoiceAtom(mostActiveAtom)) {
+				if (maxActivity > activity) {
+					double lostActitivyNormalized = (maxActivity - activity) / heapOfActiveAtoms.getCurrentActivityIncrement();
+					activityDecrease += lostActitivyNormalized;
+				}
+				return mostActiveAtom;
+			}
+			if (choiceManager.isAtomChoice(mostActiveAtom)) {
+				numNotActiveChoicePoint++;
+			} else {
+				numNoChoicePoint++;
+			}
+			numThrownAway++;
+		}
+		return DEFAULT_CHOICE_ATOM;
+	}
+
+	/**
+	 * Chooses a sign (truth value) to assign to the given atom;
+	 * uses the last value (saved phase) to determine its truth value.
+	 * 
+	 * @param atom
+	 *          the chosen atom
+	 * @return the truth value to assign to the given atom
+	 */
+	private boolean chooseSign(int atom) {
+		if (assignment.getTruth(atom) == ThriceTruth.MBT) {
+			return true;
+		}
+		return assignment.getLastValue(atom);
+	}
+
+	public void growForMaxAtomId(int maxAtomId) {
+		heapOfActiveAtoms.growForMaxAtomId(maxAtomId);
+		if (atomChoiceRelation != null) {
+			atomChoiceRelation.growForMaxAtomId(maxAtomId);
+		}
+	}
+
+	@Override
+	public double getActivity(int literal) {
+		return heapOfActiveAtoms.getActivity(literal);
+	}
+
+	@Override
+	public String toString() {
+		return this.getClass().getSimpleName();
+	}
+
+}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java b/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java
new file mode 100644
index 000000000..a7c249a46
--- /dev/null
+++ b/src/test/java/at/ac/tuwien/kr/alpha/TestUtil.java
@@ -0,0 +1,81 @@
+/**
+ * Copyright (c) 2019 Siemens AG
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+package at.ac.tuwien.kr.alpha;
+
+import at.ac.tuwien.kr.alpha.common.AtomStore;
+import at.ac.tuwien.kr.alpha.common.NoGood;
+import at.ac.tuwien.kr.alpha.common.Predicate;
+import at.ac.tuwien.kr.alpha.common.atoms.Atom;
+import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
+import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm;
+import at.ac.tuwien.kr.alpha.common.terms.Term;
+import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
+import org.apache.commons.lang3.StringUtils;
+
+import java.util.Collection;
+import java.util.stream.Collectors;
+
+/**
+ * Provides utility methods for test cases
+ *
+ */
+public class TestUtil {
+	
+	public static Literal literal(String predicateName, String... termStrings) {
+		return atom(predicateName, termStrings).toLiteral();
+	}
+
+	public static Atom atom(String predicateName, String... termStrings) {
+		Term[] terms = new Term[termStrings.length];
+		for (int i = 0; i < termStrings.length; i++) {
+			String termString = termStrings[i];
+			if (StringUtils.isAllUpperCase(termString.substring(0, 1))) {
+				terms[i] = VariableTerm.getInstance(termString);
+			} else {
+				terms[i] = ConstantTerm.getInstance(termString);
+			}
+		}
+		return new BasicAtom(Predicate.getInstance(predicateName, terms.length), terms);
+	}
+	
+	public static Literal literal(String predicateName, int... termInts) {
+		return atom(predicateName, termInts).toLiteral();
+	}
+
+	public static Atom atom(String predicateName, int... termInts) {
+		Term[] terms = new Term[termInts.length];
+		for (int i = 0; i < termInts.length; i++) {
+			terms[i] = ConstantTerm.getInstance(termInts[i]);
+		}
+		return new BasicAtom(Predicate.getInstance(predicateName, terms.length), terms);
+	}
+	
+	public static void printNoGoods(AtomStore atomStore, Collection<NoGood> noGoods) {
+		System.out.println(noGoods.stream().map(atomStore::noGoodToString).collect(Collectors.toSet()));
+	}
+
+}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java b/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java
index 4bb6623b8..22c093ec0 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java
@@ -28,13 +28,19 @@
 package at.ac.tuwien.kr.alpha.config;
 
 import org.apache.commons.cli.ParseException;
-import org.junit.Assert;
 import org.junit.Test;
 
 import java.util.Arrays;
+import java.util.function.Consumer;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertTrue;
 
 public class CommandLineParserTest {
 
+	private static final String DEFAULT_COMMAND_LINE = "java -jar Alpha-bundled.jar";
+	private static final Consumer<String> DEFAULT_ABORT_ACTION = (msg) -> { };
+
 	/**
 	 * Tests that a help message is written to the consumer configured in the
 	 * parser.
@@ -44,67 +50,102 @@ public class CommandLineParserTest {
 	@Test
 	public void help() throws ParseException {
 		StringBuilder bld = new StringBuilder();
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> bld.append(msg));
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, (msg) -> bld.append(msg));
 		parser.parseCommandLine(new String[] {"-h"});
-		Assert.assertTrue(!(bld.toString().isEmpty()));
+		assertTrue(!(bld.toString().isEmpty()));
 	}
 
 	@Test
 	public void basicUsageWithFile() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		AlphaConfig ctx = parser.parseCommandLine(new String[] {"-i", "someFile.asp", "-i", "someOtherFile.asp"});
-		Assert.assertEquals(Arrays.asList(new String[] {"someFile.asp", "someOtherFile.asp"}), ctx.getInputConfig().getFiles());
+		assertEquals(Arrays.asList(new String[] {"someFile.asp", "someOtherFile.asp"}), ctx.getInputConfig().getFiles());
 	}
 
 	@Test
 	public void basicUsageWithString() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		AlphaConfig ctx = parser.parseCommandLine(new String[] {"-str", "b :- a.", "-str", "c :- a, b."});
-		Assert.assertEquals(Arrays.asList(new String[] {"b :- a.", "c :- a, b."}), ctx.getInputConfig().getAspStrings());
+		assertEquals(Arrays.asList(new String[] {"b :- a.", "c :- a, b."}), ctx.getInputConfig().getAspStrings());
 	}
 
 	@Test(expected = ParseException.class)
 	public void invalidUsageNoInput() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		parser.parseCommandLine(new String[] {});
 	}
 
 	@Test
 	public void moreThanOneInputSource() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		parser.parseCommandLine(new String[] {"-i", "a.b", "-i", "b.c", "-str", "aString."});
 	}
 
 	@Test(expected = ParseException.class)
 	public void invalidUsageMissingInputFlag() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		parser.parseCommandLine(new String[] {"-i", "a.b", "b.c"});
 	}
 
 	@Test
 	public void numAnswerSets() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java-jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		AlphaConfig ctx = parser.parseCommandLine(new String[] {"-str", "aString.", "-n", "00435"});
-		Assert.assertEquals(435, ctx.getInputConfig().getNumAnswerSets());
+		assertEquals(435, ctx.getInputConfig().getNumAnswerSets());
 	}
 	
 	@Test(expected = ParseException.class)
 	public void noInputGiven() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java -jar Alpha--bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		parser.parseCommandLine(new String[] {});
 	}
 
 	@Test
 	public void replay() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java -jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-rc", "\"1,2, 3\""});
-		Assert.assertEquals(Arrays.asList(1, 2, 3), alphaConfig.getAlphaConfig().getReplayChoices());
+		assertEquals(Arrays.asList(1, 2, 3), alphaConfig.getAlphaConfig().getReplayChoices());
 	}
 
 	@Test(expected = ParseException.class)
 	public void replayWithNonNumericLiteral() throws ParseException {
-		CommandLineParser parser = new CommandLineParser("java -jar Alpha-bundled.jar", (msg) -> { });
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
 		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-rc", "\"1, 2, x\""});
 	}
 
+	@Test
+	public void grounderToleranceConstraints_numeric() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-gtc", "-1"});
+		assertEquals("-1", alphaConfig.getAlphaConfig().getGrounderToleranceConstraints());
+	}
+
+	@Test
+	public void grounderToleranceConstraints_string() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-gtc", "strict"});
+		assertEquals("strict", alphaConfig.getAlphaConfig().getGrounderToleranceConstraints());
+	}
+
+	@Test
+	public void grounderToleranceRules_numeric() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-gtr", "1"});
+		assertEquals("1", alphaConfig.getAlphaConfig().getGrounderToleranceRules());
+	}
+
+	@Test
+	public void grounderToleranceRules_string() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-gtr", "lax"});
+		assertEquals("lax", alphaConfig.getAlphaConfig().getGrounderToleranceRules());
+	}
+
+	@Test
+	public void noInstanceRemoval() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-dir"});
+		assertTrue(alphaConfig.getAlphaConfig().isDisableInstanceRemoval());
+	}
+
 }
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java
index 30df8b212..5583b3617 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java
@@ -32,6 +32,7 @@
 import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.ChoiceAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import org.apache.commons.lang3.tuple.ImmutablePair;
 import org.apache.commons.lang3.tuple.Pair;
 
@@ -102,6 +103,7 @@ public class ChoiceGrounder implements Grounder {
 	private static Atom atomEnBR2 = ChoiceAtom.on(2);
 	private static Atom atomDisBR1 = ChoiceAtom.off(3);
 	private static Atom atomDisBR2 = ChoiceAtom.off(4);
+	private static AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation();
 	private final AtomStore atomStore;
 	private boolean returnedAllNogoods;
 
@@ -115,6 +117,10 @@ public ChoiceGrounder(AtomStore atomStore, java.util.function.Predicate<Predicat
 		this.atomStore = atomStore;
 		this.filter = filter;
 		Arrays.asList(atomAA, atomBB, rule1, rule2, atomEnBR1, atomEnBR2, atomDisBR1, atomDisBR2).forEach(atomStore::putIfAbsent);
+		atomChoiceRelation.addRelation(atomStore.get(atomAA), atomStore.get(rule1));
+		atomChoiceRelation.addRelation(atomStore.get(atomBB), atomStore.get(rule1));
+		atomChoiceRelation.addRelation(atomStore.get(atomBB), atomStore.get(rule2));
+		atomChoiceRelation.addRelation(atomStore.get(atomAA), atomStore.get(rule2));
 	}
 
 	@Override
@@ -179,6 +185,11 @@ public void updateAssignment(Iterator<Integer> it) {
 	public void forgetAssignment(int[] atomIds) {
 	}
 
+	@Override
+	public AtomChoiceRelation getAtomChoiceRelation() {
+		return atomChoiceRelation;
+	}
+
 	private int solverDerivedNoGoodIdCounter = 20;
 	private Map<NoGood, Integer> solverDerivedNoGoods = new HashMap<>();
 
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java
index 418eb0ae6..621ee195a 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java
@@ -31,6 +31,7 @@
 import at.ac.tuwien.kr.alpha.common.atoms.Atom;
 import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import org.apache.commons.lang3.tuple.ImmutablePair;
 import org.apache.commons.lang3.tuple.Pair;
 
@@ -74,6 +75,7 @@ public class DummyGrounder implements Grounder {
 	private static Atom atomCC = new BasicAtom(Predicate.getInstance("c", 0));
 	private static Rule ruleABC = new Rule(new DisjunctiveHead(Collections.singletonList(atomCC)), Arrays.asList(atomAA.toLiteral(), atomBB.toLiteral()));
 	private static Atom rule1 = new RuleAtom(NonGroundRule.constructNonGroundRule(ruleABC), new Substitution());
+	private static AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation();
 	private Set<Integer> returnedNogoods = new HashSet<>();
 
 	public DummyGrounder(AtomStore atomStore) {
@@ -104,6 +106,11 @@ public int register(NoGood noGood) {
 		return solverDerivedNoGoods.get(noGood);
 	}
 
+	@Override
+	public AtomChoiceRelation getAtomChoiceRelation() {
+		return atomChoiceRelation;
+	}
+
 	@Override
 	public AnswerSet assignmentToAnswerSet(Iterable<Integer> trueAtoms) {
 		// Note: This grounder only deals with 0-ary predicates, i.e., every atom is a predicate and there is
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java
index aadf8c8f0..09236b940 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2018 Siemens AG
+ * Copyright (c) 2018-2019 Siemens AG
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -27,8 +27,15 @@
 
 import at.ac.tuwien.kr.alpha.common.*;
 import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom;
+import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm;
+import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser;
+import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
 import at.ac.tuwien.kr.alpha.solver.TrailAssignment;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
+import org.junit.Before;
+import org.junit.Ignore;
 import org.junit.Test;
 
 import java.util.Arrays;
@@ -36,15 +43,26 @@
 import java.util.Collections;
 import java.util.Map;
 
-import static org.junit.Assert.assertTrue;
-import static org.junit.Assert.fail;
+import static at.ac.tuwien.kr.alpha.TestUtil.atom;
+import static at.ac.tuwien.kr.alpha.TestUtil.literal;
+import static org.junit.Assert.*;
 
 /**
  * Tests {@link NaiveGrounder}
+ *
+ * Some test cases use atoms of the something/1 predicate to trick the grounder
+ * into believing that other atoms might become true. This is fragile because future implementations
+ * of preprocessing techniques might render this trick useless.
+ * If unit tests in this class begin to fail due to such improvements to preprocessing, this issue must be addressed.
  */
 public class NaiveGrounderTest {
 	private static final ProgramParser PARSER = new ProgramParser();
-	
+
+	@Before
+	public void resetRuleIdGenerator() {
+		NonGroundRule.ID_GENERATOR.resetGenerator();
+	}
+
 	/**
 	 * Asserts that a ground rule whose positive body is not satisfied by the empty assignment
 	 * is grounded immediately.
@@ -54,10 +72,10 @@ public void groundRuleAlreadyGround() {
 		Program program = PARSER.parse("a :- not b. "
 				+ "b :- not a. "
 				+ "c :- b.");
-		
+
 		AtomStore atomStore = new AtomStoreImpl();
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true);
-		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore));
+		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()));
 		int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false);
 		int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))));
 		assertExistsNoGoodContaining(noGoods.values(), litCNeg);
@@ -74,10 +92,10 @@ public void groundRuleWithLongerBodyAlreadyGround() {
 				+ "b :- not a. "
 				+ "c :- b. "
 				+ "d :- b, c. ");
-		
+
 		AtomStore atomStore = new AtomStoreImpl();
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true);
-		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore));
+		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()));
 		int litANeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("a", 0))), false);
 		int litBNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))), false);
 		int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false);
@@ -87,7 +105,7 @@ public void groundRuleWithLongerBodyAlreadyGround() {
 		assertExistsNoGoodContaining(noGoods.values(), litCNeg);
 		assertExistsNoGoodContaining(noGoods.values(), litDNeg);
 	}
-	
+
 	/**
 	 * Asserts that a ground constraint whose positive body is not satisfied by the empty assignment
 	 * is grounded immediately.
@@ -97,14 +115,175 @@ public void groundConstraintAlreadyGround() {
 		Program program = PARSER.parse("a :- not b. "
 				+ "b :- not a. "
 				+ ":- b.");
-		
+
 		AtomStore atomStore = new AtomStoreImpl();
 		Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true);
-		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore));
+		Map<Integer, NoGood> noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()));
 		int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))));
-		assertTrue(noGoods.containsValue(NoGood.fromConstraint(Arrays.asList(litB), Collections.emptyList())));
+		assertTrue(noGoods.containsValue(NoGood.fromConstraint(Collections.singletonList(litB), Collections.emptyList())));
+	}
+
+	@Test
+	public void avoidDeadEndsWithLaxGrounderHeuristic() {
+		RuleGroundingOrder groundingOrderP1 = new RuleGroundingOrder(literal("p1", "X"),
+				Arrays.asList(literal("p2", "X"), literal("q2", "Y"), literal("q1", "Y")), -1, false);
+		RuleGroundingOrder groundingOrderQ1 = new RuleGroundingOrder(literal("q1", "Y"),
+				Arrays.asList(literal("q2", "Y"), literal("p2", "X"), literal("p1", "X")), -1, false);
+		testDeadEnd(groundingOrderP1, groundingOrderQ1, true);
+	}
+
+	@Test
+	public void noDeadEndWithLaxGrounderHeuristic() {
+		RuleGroundingOrder groundingOrderP1 = new RuleGroundingOrder(literal("p1", "X"),
+				Arrays.asList(literal("p2", "X"), literal("q1", "Y"), literal("q2", "Y")), -1, false);
+		RuleGroundingOrder groundingOrderQ1 = new RuleGroundingOrder(literal("q1", "Y"),
+				Arrays.asList(literal("q2", "Y"), literal("p1", "X"), literal("p2", "X")), -1, false);
+		testDeadEnd(groundingOrderP1, groundingOrderQ1, true);
+	}
+
+	private void testDeadEnd(RuleGroundingOrder groundingOrderP1, RuleGroundingOrder groundingOrderQ1, boolean expectNoGoods) {
+		Program program = PARSER.parse("p1(1). q1(1). "
+				+ "x :- p1(X), p2(X), q1(Y), q2(Y). "
+				+ "p2(X) :- something(X). "
+				+ "q2(X) :- something(X). ");
+
+		AtomStore atomStore = new AtomStoreImpl();
+		NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, GrounderHeuristicsConfiguration.lax(), true);
+
+		NonGroundRule nonGroundRule = grounder.getNonGroundRule(0);
+		final Literal litP1X = literal("p1", "X");
+		final Literal litQ1Y = literal("q1", "Y");
+		nonGroundRule.groundingOrder.groundingOrders.put(litP1X, groundingOrderP1);
+		nonGroundRule.groundingOrder.groundingOrders.put(litQ1Y, groundingOrderQ1);
+
+		grounder.bootstrap();
+		TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
+		final Substitution substP1X1 = Substitution.unify(litP1X, new Instance(ConstantTerm.getInstance(1)), new Substitution());
+		final Substitution substQ1Y1 = Substitution.unify(litQ1Y, new Instance(ConstantTerm.getInstance(1)), new Substitution());
+		final NaiveGrounder.BindingResult bindingResultP1 = grounder.bindNextAtomInRule(nonGroundRule, groundingOrderP1, substP1X1, currentAssignment);
+		final NaiveGrounder.BindingResult bindingResultQ1 = grounder.bindNextAtomInRule(nonGroundRule, groundingOrderQ1, substQ1Y1, currentAssignment);
+
+		assertEquals(expectNoGoods, bindingResultP1.size() > 0);
+		assertEquals(expectNoGoods, bindingResultQ1.size() > 0);
+	}
+
+	@Test
+	public void testGroundingOfRuleSwitchedOffByFalsePositiveBody() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X). "
+				+ "b(X) :- something(X). ");
+		testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.FALSE, false);
+	}
+
+	@Test
+	public void testGroundingOfRuleNotSwitchedOffByTruePositiveBody() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X). "
+				+ "b(X) :- something(X). ");
+		testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.TRUE, true);
+	}
+
+	@Test
+	@Ignore("Currently, rule grounding is not switched off by a true negative body atom")
+	public void testGroundingOfRuleSwitchedOffByTrueNegativeBody() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), not b(X). "
+				+ "b(X) :- something(X). ");
+		testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.TRUE, false);
 	}
-	
+
+	@Test
+	public void testGroundingOfRuleNotSwitchedOffByFalseNegativeBody() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), not b(X). "
+				+ "b(X) :- something(X). ");
+
+		testIfGrounderGroundsRule(program, 0, literal("a", "X"), 1, ThriceTruth.FALSE, true);
+	}
+
+	private void testIfGrounderGroundsRule(Program program, int ruleID, Literal startingLiteral, int startingInstance, ThriceTruth bTruth, boolean expectNoGoods) {
+		AtomStore atomStore = new AtomStoreImpl();
+		TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
+		NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, GrounderHeuristicsConfiguration.lax(), true);
+
+		int b = atomStore.putIfAbsent(atom("b", 1));
+		currentAssignment.growForMaxAtomId();
+		currentAssignment.assign(b, bTruth);
+
+		grounder.bootstrap();
+		final NonGroundRule nonGroundRule = grounder.getNonGroundRule(ruleID);
+		final Substitution substStartingLiteral = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(startingInstance)), new Substitution());
+		final NaiveGrounder.BindingResult bindingResult = grounder.bindNextAtomInRule(nonGroundRule, nonGroundRule.groundingOrder.groundingOrders.get(startingLiteral), substStartingLiteral, currentAssignment);
+		assertEquals(expectNoGoods, bindingResult.size() > 0);
+	}
+
+	@Test
+	public void testLaxGrounderHeuristicTolerance_0_reject() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X). "
+				+ "b(X) :- something(X).");
+		testLaxGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 0, 0, false);
+	}
+
+	@Test
+	public void testLaxGrounderHeuristicTolerance_1_accept() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X). "
+				+ "b(X) :- something(X).");
+		testLaxGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 1, 0, true);
+	}
+
+	@Test
+	public void testLaxGrounderHeuristicTolerance_1_reject() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X), b(X+1). "
+				+ "b(X) :- something(X).");
+		testLaxGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 1, 0, false);
+	}
+
+	@Test
+	public void testLaxGrounderHeuristicTolerance_2_accept() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X), b(X+1). "
+				+ "b(X) :- something(X).");
+		testLaxGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 2, 0, true);
+	}
+
+	@Test
+	public void testLaxGrounderHeuristicTolerance_2_reject() {
+		Program program = PARSER.parse("a(1). "
+				+ "c(X) :- a(X), b(X), b(X+1), b(X+2). "
+				+ "b(X) :- something(X).");
+		testLaxGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 2, 0, false);
+	}
+
+	@Test
+	public void testLaxGrounderHeuristicTolerance_2_accept_multiple_facts_of_same_variable() {
+		Program program = PARSER.parse("a(1). b(1). "
+				+ "c(X) :- a(X), b(X), b(X+1), b(X+2). "
+				+ "b(X) :- something(X).");
+		testLaxGrounderHeuristicTolerance(program, 0, literal("a", "X"), 1, 2, 0, true);
+	}
+
+	private void testLaxGrounderHeuristicTolerance(Program program, int ruleID, Literal startingLiteral, int startingInstance, int tolerance, int nTrueBs, boolean expectNoGoods) {
+		AtomStore atomStore = new AtomStoreImpl();
+		TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
+		GrounderHeuristicsConfiguration heuristicConfiguration = GrounderHeuristicsConfiguration.getInstance(tolerance, tolerance);
+		NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, heuristicConfiguration, true);
+
+		for (int i = 1; i <= nTrueBs; i++) {
+			int b = atomStore.putIfAbsent(atom("b", i));
+			currentAssignment.growForMaxAtomId();
+			currentAssignment.assign(b, ThriceTruth.TRUE);
+		}
+
+		grounder.bootstrap();
+		final NonGroundRule nonGroundRule = grounder.getNonGroundRule(ruleID);
+		final Substitution substStartingLiteral = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(startingInstance)), new Substitution());
+		final NaiveGrounder.BindingResult bindingResult = grounder.bindNextAtomInRule(nonGroundRule, nonGroundRule.groundingOrder.groundingOrders.get(startingLiteral), substStartingLiteral, currentAssignment);
+		assertEquals(expectNoGoods, bindingResult.size() > 0);
+	}
+
 	private void assertExistsNoGoodContaining(Collection<NoGood> noGoods, int literal) {
 		for (NoGood noGood : noGoods) {
 			for (int literalInNoGood : noGood) {
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java
index 219a55045..8c6b53c41 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrderTest.java
@@ -1,18 +1,46 @@
+/**
+ * Copyright (c) 2017-2019, the Alpha Team.
+ * All rights reserved.
+ * 
+ * Additional changes made by Siemens.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
 package at.ac.tuwien.kr.alpha.grounder;
 
 import at.ac.tuwien.kr.alpha.common.Program;
 import at.ac.tuwien.kr.alpha.common.Rule;
+import at.ac.tuwien.kr.alpha.common.atoms.Literal;
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser;
 import at.ac.tuwien.kr.alpha.grounder.transformation.VariableEqualityRemoval;
 import org.junit.Test;
 
 import java.io.IOException;
 
-import static org.junit.Assert.assertEquals;
-import static org.junit.Assert.assertTrue;
+import static at.ac.tuwien.kr.alpha.TestUtil.literal;
+import static org.junit.Assert.*;
 
 /**
- * Copyright (c) 2017, the Alpha Team.
+ * Copyright (c) 2017-2019, the Alpha Team.
  */
 public class RuleGroundingOrderTest {
 
@@ -27,19 +55,19 @@ public void groundingOrder() throws IOException {
 		new VariableEqualityRemoval().transform(program);
 		Rule rule0 = program.getRules().get(0);
 		NonGroundRule nonGroundRule0 = NonGroundRule.constructNonGroundRule(rule0);
-		RuleGroundingOrder rgo0 = new RuleGroundingOrder(nonGroundRule0);
+		RuleGroundingOrders rgo0 = new RuleGroundingOrders(nonGroundRule0);
 		rgo0.computeGroundingOrders();
 		assertEquals(4, rgo0.getStartingLiterals().size());
 
 		Rule rule1 = program.getRules().get(1);
 		NonGroundRule nonGroundRule1 = NonGroundRule.constructNonGroundRule(rule1);
-		RuleGroundingOrder rgo1 = new RuleGroundingOrder(nonGroundRule1);
+		RuleGroundingOrders rgo1 = new RuleGroundingOrders(nonGroundRule1);
 		rgo1.computeGroundingOrders();
 		assertEquals(4, rgo1.getStartingLiterals().size());
 
 		Rule rule2 = program.getRules().get(2);
 		NonGroundRule nonGroundRule2 = NonGroundRule.constructNonGroundRule(rule2);
-		RuleGroundingOrder rgo2 = new RuleGroundingOrder(nonGroundRule2);
+		RuleGroundingOrders rgo2 = new RuleGroundingOrders(nonGroundRule2);
 		rgo2.computeGroundingOrders();
 		assertTrue(rgo2.fixedInstantiation());
 	}
@@ -48,10 +76,66 @@ public void groundingOrder() throws IOException {
 	public void groundingOrderUnsafe() throws IOException {
 		Program program = parser.parse("h(X,C) :- X = Y, Y = C .. 3, C = X.");
 		new VariableEqualityRemoval().transform(program);
-		Rule rule0 = program.getRules().get(0);
-		NonGroundRule nonGroundRule0 = NonGroundRule.constructNonGroundRule(rule0);
-		RuleGroundingOrder rgo0 = new RuleGroundingOrder(nonGroundRule0);
-		rgo0.computeGroundingOrders();
+		computeGroundingOrdersForRule(program, 0);
+	}
+	
+	@Test
+	public void testPositionFromWhichAllVarsAreBound_ground() {
+		Program program = parser.parse("a :- b, not c.");
+		RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0);
+		assertEquals(0, rgo0.getFixedGroundingOrder().getPositionFromWhichAllVarsAreBound());
+	}
+	
+	@Test
+	public void testPositionFromWhichAllVarsAreBound_simpleNonGround() {
+		Program program = parser.parse("a(X) :- b(X), not c(X).");
+		RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0);
+		assertEquals(1, rgo0.getStartingLiterals().size());
+		for (Literal startingLiteral : rgo0.getStartingLiterals()) {
+			assertEquals(0, rgo0.orderStartingFrom(startingLiteral).getPositionFromWhichAllVarsAreBound());
+		}
+	}
+
+	@Test
+	public void testPositionFromWhichAllVarsAreBound_longerSimpleNonGround() {
+		Program program = parser.parse("a(X) :- b(X), c(X), d(X), not e(X).");
+		RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0);
+		assertEquals(3, rgo0.getStartingLiterals().size());
+		for (Literal startingLiteral : rgo0.getStartingLiterals()) {
+			assertEquals(0, rgo0.orderStartingFrom(startingLiteral).getPositionFromWhichAllVarsAreBound());
+		}
+	}
+
+	@Test
+	public void testToString_longerSimpleNonGround() {
+		Program program = parser.parse("a(X) :- b(X), c(X), d(X), not e(X).");
+		RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0);
+		assertEquals(3, rgo0.getStartingLiterals().size());
+		for (Literal startingLiteral : rgo0.getStartingLiterals()) {
+			switch (startingLiteral.getPredicate().getName()) {
+				case "b": assertEquals("b(X) : | c(X), d(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); break;
+				case "c": assertEquals("c(X) : | b(X), d(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); break;
+				case "d": assertEquals("d(X) : | b(X), c(X), not e(X)", rgo0.orderStartingFrom(startingLiteral).toString()); break;
+				default: fail("Unexpected starting literal: " + startingLiteral);
+			}
+		}
+	}
+
+	@Test
+	public void testPositionFromWhichAllVarsAreBound_joinedNonGround() {
+		Program program = parser.parse("a(X) :- b(X), c(X,Y), d(X,Z), not e(X).");
+		RuleGroundingOrders rgo0 = computeGroundingOrdersForRule(program, 0);
+		assertTrue(2 <= rgo0.orderStartingFrom(literal("b", "X")).getPositionFromWhichAllVarsAreBound());
+		assertTrue(1 <= rgo0.orderStartingFrom(literal("c", "X", "Y")).getPositionFromWhichAllVarsAreBound());
+		assertTrue(1 <= rgo0.orderStartingFrom(literal("d", "X", "Z")).getPositionFromWhichAllVarsAreBound());
+	}
+
+	private RuleGroundingOrders computeGroundingOrdersForRule(Program program, int ruleIndex) {
+		Rule rule = program.getRules().get(ruleIndex);
+		NonGroundRule nonGroundRule = NonGroundRule.constructNonGroundRule(rule);
+		RuleGroundingOrders rgo = new RuleGroundingOrders(nonGroundRule);
+		rgo.computeGroundingOrders();
+		return rgo;
 	}
 
 }
\ No newline at end of file
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/heuristics/GrounderHeuristicConfigurationTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/heuristics/GrounderHeuristicConfigurationTest.java
new file mode 100644
index 000000000..6f9e2240c
--- /dev/null
+++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/heuristics/GrounderHeuristicConfigurationTest.java
@@ -0,0 +1,93 @@
+/**
+ * Copyright (c) 2019 Siemens AG
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ *    list of conditions and the following disclaimer.
+ * 
+ * 2) Redistributions in binary form must reproduce the above copyright notice,
+ *    this list of conditions and the following disclaimer in the documentation
+ *    and/or other materials provided with the distribution.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+package at.ac.tuwien.kr.alpha.grounder.heuristics;
+
+import org.junit.Test;
+
+import static at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration.LAX_STRING;
+import static at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration.STRICT_STRING;
+import static org.junit.Assert.*;
+
+/**
+ * Tests {@link GrounderHeuristicsConfiguration}
+ */
+public class GrounderHeuristicConfigurationTest {
+
+	@Test
+	public void testGetInstanceStrictStrict() {
+		GrounderHeuristicsConfiguration grounderHeuristicsConfiguration = GrounderHeuristicsConfiguration.getInstance(STRICT_STRING, STRICT_STRING);
+		assertFalse(grounderHeuristicsConfiguration.isLax(true));
+		assertFalse(grounderHeuristicsConfiguration.isLax(false));
+		assertEquals(0, grounderHeuristicsConfiguration.getToleranceConstraints());
+		assertEquals(0, grounderHeuristicsConfiguration.getToleranceRules());
+	}
+
+	@Test
+	public void testGetInstanceStrictLax() {
+		GrounderHeuristicsConfiguration grounderHeuristicsConfiguration = GrounderHeuristicsConfiguration.getInstance(STRICT_STRING, LAX_STRING);
+		assertFalse(grounderHeuristicsConfiguration.isLax(true));
+		assertTrue(grounderHeuristicsConfiguration.isLax(false));
+		assertEquals(0, grounderHeuristicsConfiguration.getToleranceConstraints());
+		assertEquals(-1, grounderHeuristicsConfiguration.getToleranceRules());
+	}
+
+	@Test
+	public void testGetInstanceLaxStrict() {
+		GrounderHeuristicsConfiguration grounderHeuristicsConfiguration = GrounderHeuristicsConfiguration.getInstance(LAX_STRING, STRICT_STRING);
+		assertTrue(grounderHeuristicsConfiguration.isLax(true));
+		assertFalse(grounderHeuristicsConfiguration.isLax(false));
+		assertEquals(-1, grounderHeuristicsConfiguration.getToleranceConstraints());
+		assertEquals(0, grounderHeuristicsConfiguration.getToleranceRules());
+	}
+
+	@Test
+	public void testGetInstanceLaxLax() {
+		GrounderHeuristicsConfiguration grounderHeuristicsConfiguration = GrounderHeuristicsConfiguration.getInstance(LAX_STRING, LAX_STRING);
+		assertTrue(grounderHeuristicsConfiguration.isLax(true));
+		assertTrue(grounderHeuristicsConfiguration.isLax(false));
+		assertEquals(-1, grounderHeuristicsConfiguration.getToleranceConstraints());
+		assertEquals(-1, grounderHeuristicsConfiguration.getToleranceRules());
+	}
+
+	@Test
+	public void testGetInstanceIntInt() {
+		GrounderHeuristicsConfiguration grounderHeuristicsConfiguration = GrounderHeuristicsConfiguration.getInstance(5, 1);
+		assertTrue(grounderHeuristicsConfiguration.isLax(true));
+		assertTrue(grounderHeuristicsConfiguration.isLax(false));
+		assertEquals(5, grounderHeuristicsConfiguration.getToleranceConstraints());
+		assertEquals(1, grounderHeuristicsConfiguration.getToleranceRules());
+	}
+
+	@Test
+	public void testGetInstanceStringIntStringInt() {
+		GrounderHeuristicsConfiguration grounderHeuristicsConfiguration = GrounderHeuristicsConfiguration.getInstance("5", "1");
+		assertTrue(grounderHeuristicsConfiguration.isLax(true));
+		assertTrue(grounderHeuristicsConfiguration.isLax(false));
+		assertEquals(5, grounderHeuristicsConfiguration.getToleranceConstraints());
+		assertEquals(1, grounderHeuristicsConfiguration.getToleranceRules());
+	}
+
+}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java
index efe8b1baf..3889603c3 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java
@@ -39,6 +39,7 @@
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser;
 import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
 import at.ac.tuwien.kr.alpha.solver.TrailAssignment;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Test;
 
 import java.util.Arrays;
@@ -67,7 +68,7 @@ public void justifySimpleRules() {
 		AtomStore atomStore = new AtomStoreImpl();
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true);
 		grounder.getNoGoods(null);
-		TrailAssignment assignment = new TrailAssignment(atomStore);
+		TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		int rId = atomStore.get(new BasicAtom(Predicate.getInstance("r", 0)));
 		int nrId = atomStore.get(new BasicAtom(Predicate.getInstance("nr", 0)));
 		assignment.growForMaxAtomId();
@@ -92,7 +93,7 @@ public void justifyLargerRules() {
 		AtomStore atomStore = new AtomStoreImpl();
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true);
 		grounder.getNoGoods(null);
-		TrailAssignment assignment = new TrailAssignment(atomStore);
+		TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		Atom p1 = parser.parse("p(1).").getFacts().get(0);
 		Atom r2 = parser.parse("r(2).").getFacts().get(0);
 		Atom s12 = parser.parse("s(1,2).").getFacts().get(0);
@@ -129,7 +130,7 @@ public void justifyMultipleReasons() {
 		AtomStore atomStore = new AtomStoreImpl();
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true);
 		grounder.getNoGoods(null);
-		TrailAssignment assignment = new TrailAssignment(atomStore);
+		TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		Atom qa = parser.parse("q(a).").getFacts().get(0);
 		Atom qb = parser.parse("q(b).").getFacts().get(0);
 		Atom qc = parser.parse("q(c).").getFacts().get(0);
@@ -185,7 +186,7 @@ public void justifyNegatedFactsRemovedFromReasons() {
 		AtomStore atomStore = new AtomStoreImpl();
 		NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true);
 		grounder.getNoGoods(null);
-		TrailAssignment assignment = new TrailAssignment(atomStore);
+		TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		int rId = atomStore.get(new BasicAtom(Predicate.getInstance("r", 0)));
 		int nrId = atomStore.get(new BasicAtom(Predicate.getInstance("nr", 0)));
 		assignment.growForMaxAtomId();
@@ -200,4 +201,4 @@ public void justifyNegatedFactsRemovedFromReasons() {
 			assertNotEquals(literal.getPredicate(), Predicate.getInstance("forbidden", 2));
 		}
 	}
-}
\ No newline at end of file
+}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java
index 9fc0ec829..96a819b3b 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java
@@ -91,7 +91,7 @@ private static String[] getProperty(String subKey, String def) {
 		return System.getProperty("test." + subKey, def).split(",");
 	}
 
-	@Parameters(name = "{0}/{1}/{2}/{3}")
+	@Parameters(name = "{0}/{1}/{2}/{3}/seed={4}/checks={5}/gtc={6}/gtr={7}/dir={8}")
 	public static Collection<Object[]> parameters() {
 		// Check whether we are running in a CI environment.
 		boolean ci = Boolean.valueOf(System.getenv("CI"));
@@ -100,6 +100,9 @@ public static Collection<Object[]> parameters() {
 		String[] grounders = getProperty("grounders", "naive");
 		String[] stores = getProperty("stores", ci ? "alpharoaming,naive" : "alpharoaming");
 		String[] heuristics = getProperty("heuristics", ci ? "ALL" : "NAIVE,VSIDS");
+		String[] gtcValues = getProperty("grounderToleranceConstraints", "strict,lax");
+		String[] gtrValues = getProperty("grounderToleranceRules", "strict");
+		String[] dirValues = getProperty("disableInstanceRemoval", ci ? "false,true" : "false");
 
 		// "ALL" is a magic value that will be expanded to contain all heuristics.
 		if ("ALL".equals(heuristics[0])) {
@@ -128,9 +131,15 @@ public static Collection<Object[]> parameters() {
 			for (String grounder : grounders) {
 				for (String store : stores) {
 					for (String heuristic : heuristics) {
-						factories.add(new Object[]{
-							solver, grounder, store, BranchingHeuristicFactory.Heuristic.valueOf(heuristic), seed, checks
-						});
+						for (String gtc : gtcValues) {
+							for (String gtr : gtrValues) {
+								for (String dir : dirValues) {
+									factories.add(new Object[]{
+											solver, grounder, store, BranchingHeuristicFactory.Heuristic.valueOf(heuristic), seed, checks, gtc, gtr, Boolean.valueOf(dir)
+									});
+								}
+							}
+						}
 					}
 				}
 			}
@@ -157,6 +166,15 @@ public static Collection<Object[]> parameters() {
 	@Parameter(5)
 	public boolean checks;
 
+	@Parameter(6)
+	public String grounderToleranceConstraints;
+
+	@Parameter(7)
+	public String grounderToleranceRules;
+
+	@Parameter(8)
+	public boolean disableInstanceRemoval;
+
 	protected Solver getInstance(AtomStore atomStore, Grounder grounder) {
 		return SolverFactory.getInstance(buildSystemConfig(), atomStore, grounder);
 	}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/AggregatesTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/AggregatesTest.java
index f00f54183..1876400dd 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/AggregatesTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/AggregatesTest.java
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2018 Siemens AG
+ * Copyright (c) 2018-2019 Siemens AG
  * All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
@@ -29,6 +29,7 @@
 import at.ac.tuwien.kr.alpha.common.AtomStoreImpl;
 import at.ac.tuwien.kr.alpha.common.Program;
 import at.ac.tuwien.kr.alpha.grounder.GrounderFactory;
+import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.grounder.transformation.CardinalityNormalization;
 import at.ac.tuwien.kr.alpha.grounder.transformation.SumNormalization;
 import org.junit.Test;
@@ -165,7 +166,7 @@ public void testAggregate_Sum_GlobalVariable() throws IOException {
 	@Override
 	protected Solver getInstance(Program program) {
 		AtomStore atomStore = new AtomStoreImpl();
-		return getInstance(atomStore, GrounderFactory.getInstance(grounderName, program, atomStore, p->true, useCountingGridNormalization(), true));
+		return getInstance(atomStore, GrounderFactory.getInstance(grounderName, program, atomStore, p->true, new GrounderHeuristicsConfiguration(), useCountingGridNormalization(), true));
 	}
 	
 	protected abstract boolean useCountingGridNormalization();
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java
index 682ddb425..49e06f571 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java
@@ -33,6 +33,7 @@
 import at.ac.tuwien.kr.alpha.grounder.NaiveGrounder;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Before;
 import org.junit.Test;
 
@@ -53,7 +54,7 @@ public void setUp() throws IOException {
 		Program parsedProgram = new ProgramParser().parse(testProgram);
 		this.atomStore = new AtomStoreImpl();
 		this.grounder = new NaiveGrounder(parsedProgram, atomStore, true);
-		WritableAssignment assignment = new TrailAssignment(atomStore);
+		WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment);
 		this.choiceManager = new ChoiceManager(assignment, store);
 	}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java
index 1d9f4cbc5..2ec460f14 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java
@@ -31,6 +31,7 @@
 import at.ac.tuwien.kr.alpha.common.AtomStoreImpl;
 import at.ac.tuwien.kr.alpha.common.AtomStoreTest;
 import at.ac.tuwien.kr.alpha.common.NoGood;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Before;
 import org.junit.Test;
 
@@ -47,7 +48,7 @@ public class LearnedNoGoodDeletionTest {
 	public LearnedNoGoodDeletionTest() {
 		AtomStore atomStore = new AtomStoreImpl();
 		AtomStoreTest.fillAtomStore(atomStore, 200);
-		WritableAssignment assignment = new TrailAssignment(atomStore);
+		WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		assignment.growForMaxAtomId();
 		store = new NoGoodStoreAlphaRoaming(assignment);
 		learnedNoGoodDeletion = store.getLearnedNoGoodDeletion();
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java
index 33a069469..5bc9477ca 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java
@@ -1,6 +1,7 @@
 package at.ac.tuwien.kr.alpha.solver;
 
 import at.ac.tuwien.kr.alpha.common.*;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Before;
 import org.junit.Ignore;
 import org.junit.Test;
@@ -22,7 +23,7 @@ public class NaiveNoGoodStoreTest {
 
 	public NaiveNoGoodStoreTest() {
 		atomStore = new AtomStoreImpl();
-		assignment = new TrailAssignment(atomStore);
+		assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		store = new NaiveNoGoodStore(assignment);
 	}
 
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java
index 0f6d73acf..20f18ce43 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java
@@ -1,6 +1,7 @@
 package at.ac.tuwien.kr.alpha.solver;
 
 import at.ac.tuwien.kr.alpha.common.*;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Before;
 import org.junit.Ignore;
 import org.junit.Test;
@@ -24,7 +25,7 @@ public class NoGoodStoreAlphaRoamingTest {
 	public NoGoodStoreAlphaRoamingTest() {
 		atomStore = new AtomStoreImpl();
 		AtomStoreTest.fillAtomStore(atomStore, 200);
-		assignment = new TrailAssignment(atomStore);
+		assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		assignment.growForMaxAtomId();
 		store = new NoGoodStoreAlphaRoaming(assignment);
 	}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java
index 418412e2d..48c9857b9 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java
@@ -1,17 +1,17 @@
 /**
  * Copyright (c) 2017 Siemens AG
  * All rights reserved.
- * 
+ *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
- * 
+ *
  * 1) Redistributions of source code must retain the above copyright notice, this
  *    list of conditions and the following disclaimer.
- * 
+ *
  * 2) Redistributions in binary form must reproduce the above copyright notice,
  *    this list of conditions and the following disclaimer in the documentation
  *    and/or other materials provided with the distribution.
- * 
+ *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
@@ -26,6 +26,7 @@
 package at.ac.tuwien.kr.alpha.solver;
 
 import at.ac.tuwien.kr.alpha.common.AnswerSet;
+import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory;
 import org.junit.Ignore;
 import org.junit.Test;
 
@@ -36,44 +37,51 @@
 import java.util.stream.Collectors;
 
 import static org.junit.Assert.assertEquals;
+import static org.junit.Assume.assumeTrue;
 
 /**
  * Tests {@link AbstractSolver} using some pigeon-hole test cases (see https://en.wikipedia.org/wiki/Pigeonhole_principle).
- *
  */
 public class PigeonHoleTest extends AbstractSolverTests {
-	@Test(timeout = 1000)
+	@Test(timeout = 5000)
 	public void test2Pigeons2Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(2, 2);
 	}
 
-	@Test(timeout = 1000)
+	@Test(timeout = 5000)
 	public void test3Pigeons2Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(3, 2);
 	}
 
-	@Test(timeout = 1000)
+	@Test(timeout = 5000)
 	public void test2Pigeons3Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(2, 3);
 	}
 
-	@Test(timeout = 1000)
+	@Test(timeout = 10000)
 	public void test3Pigeons3Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(3, 3);
 	}
 
-	@Test(timeout = 3000)
+	@Test(timeout = 10000)
 	public void test4Pigeons3Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(4, 3);
 	}
 
-	@Test(timeout = 3000)
+	@Test(timeout = 10000)
 	public void test3Pigeons4Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(3, 4);
 	}
 
-	@Test(timeout = 3000)
+	@Test(timeout = 10000)
 	public void test4Pigeons4Holes() throws IOException {
+		assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS);
 		testPigeonsHoles(4, 4);
 	}
 
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java
index a4c7999aa..706ee08ee 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java
@@ -31,32 +31,75 @@
 import java.util.Set;
 
 import static org.junit.Assert.assertEquals;
+import static org.junit.Assume.assumeTrue;
 
 public class SolverStatisticsTests extends AbstractSolverTests {
 
 	@Test
 	public void checkStatsStringZeroChoices() {
 		Solver solver = getInstance("a.");
+		assumeTrue(solver instanceof SolverMaintainingStatistics);
 		collectAnswerSetsAndCheckStats(solver, 1, 0, 0, 0, 0, 0, 0, 0);
 	}
 
 	@Test
 	public void checkStatsStringOneChoice() {
 		Solver solver = getInstance("a :- not b. b :- not a.");
+		assumeTrue(solver instanceof SolverMaintainingStatistics);
 		collectAnswerSetsAndCheckStats(solver, 2, 1, 1, 1, 1, 0, 0, 0);
 	}
 
+	@Test
+	public void checkNoGoodCounterStatsByTypeZeroChoices() {
+		Solver solver = getInstance("a.");
+		assumeTrue(solver instanceof SolverMaintainingStatistics);
+		collectAnswerSetsAndCheckNoGoodCounterStatsByType(solver, 0, 0, 0, 0);
+	}
+
+	@Test
+	public void checkNoGoodCounterStatsByTypeOneChoice() {
+		Solver solver = getInstance("a :- not b. b :- not a.");
+		assumeTrue(solver instanceof SolverMaintainingStatistics);
+		collectAnswerSetsAndCheckNoGoodCounterStatsByType(solver, 7, 2, 0, 4);
+	}
+
+	@Test
+	public void checkNoGoodCounterStatsByCardinalityZeroChoices() {
+		Solver solver = getInstance("a.");
+		assumeTrue(solver instanceof SolverMaintainingStatistics);
+		collectAnswerSetsAndCheckNoGoodCounterStatsByCardinality(solver, 0, 0, 0);
+	}
+
+	@Test
+	public void checkNoGoodCounterStatsByCardinalityOneChoice() {
+		Solver solver = getInstance("a :- not b. b :- not a.");
+		assumeTrue(solver instanceof SolverMaintainingStatistics);
+		collectAnswerSetsAndCheckNoGoodCounterStatsByCardinality(solver, 3, 10, 0);
+	}
+
 	private void collectAnswerSetsAndCheckStats(Solver solver, int expectedNumberOfAnswerSets, int expectedNumberOfGuesses, int expectedTotalNumberOfBacktracks,
 			int expectedNumberOfBacktracksWithinBackjumps, int expectedNumberOfBackjumps, int expectedNumberOfMBTs, int expectedNumberOfConflictsAfterClosing, int expectedNumberOfDeletedNoGoods) {
 		Set<AnswerSet> answerSets = solver.collectSet();
 		assertEquals(expectedNumberOfAnswerSets, answerSets.size());
-		if (solver instanceof SolverMaintainingStatistics) {
-			SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver;
-			assertEquals(
-					String.format("g=%d, bt=%d, bj=%d, bt_within_bj=%d, mbt=%d, cac=%d, del_ng=%d", expectedNumberOfGuesses, expectedTotalNumberOfBacktracks, expectedNumberOfBackjumps,
-							expectedNumberOfBacktracksWithinBackjumps, expectedNumberOfMBTs, expectedNumberOfConflictsAfterClosing, expectedNumberOfDeletedNoGoods),
-					solverMaintainingStatistics.getStatisticsString());
-		}
+		SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver;
+		assertEquals(
+				String.format("g=%d, bt=%d, bj=%d, bt_within_bj=%d, mbt=%d, cac=%d, del_ng=%d", expectedNumberOfGuesses, expectedTotalNumberOfBacktracks, expectedNumberOfBackjumps,
+						expectedNumberOfBacktracksWithinBackjumps, expectedNumberOfMBTs, expectedNumberOfConflictsAfterClosing, expectedNumberOfDeletedNoGoods),
+				solverMaintainingStatistics.getStatisticsString());
+	}
+
+	private void collectAnswerSetsAndCheckNoGoodCounterStatsByType(Solver solver, int expectedNumberOfStaticNoGoods, int expectedNumberOfSupportNoGoods, int expectedNumberOfLearntNoGoods, int expectedNumberOfInternalNoGoods) {
+		solver.collectSet();
+		SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver;
+		final NoGoodCounter noGoodCounter =  solverMaintainingStatistics.getNoGoodCounter();
+		assertEquals("STATIC: " + expectedNumberOfStaticNoGoods + " SUPPORT: " + expectedNumberOfSupportNoGoods + " LEARNT: " + expectedNumberOfLearntNoGoods + " INTERNAL: " + expectedNumberOfInternalNoGoods, noGoodCounter.getStatsByType());
+	}
+
+	private void collectAnswerSetsAndCheckNoGoodCounterStatsByCardinality(Solver solver, int expectedNumberOfUnaryNoGoods, int expectedNumberOfBinaryNoGoods, int expectedNumberOfNAryNoGoods) {
+		solver.collectSet();
+		SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver;
+		final NoGoodCounter noGoodCounter =  solverMaintainingStatistics.getNoGoodCounter();
+		assertEquals("unary: " + expectedNumberOfUnaryNoGoods + " binary: " + expectedNumberOfBinaryNoGoods + " larger: " + expectedNumberOfNAryNoGoods, noGoodCounter.getStatsByCardinality());
 	}
 
 }
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java
index 119e3a0db..f90c7bc05 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java
@@ -31,6 +31,7 @@
 import at.ac.tuwien.kr.alpha.common.AtomStore;
 import at.ac.tuwien.kr.alpha.common.AtomStoreImpl;
 import at.ac.tuwien.kr.alpha.common.AtomStoreTest;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Before;
 import org.junit.Test;
 
@@ -51,7 +52,7 @@ public class TrailAssignmentTest {
 	public TrailAssignmentTest() {
 		AtomStore atomStore = new AtomStoreImpl();
 		AtomStoreTest.fillAtomStore(atomStore, 20);
-		assignment = new TrailAssignment(atomStore);
+		assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 	}
 
 	@Before
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java
index ab891ae23..4c325280e 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java
@@ -73,7 +73,7 @@ public void setUp() throws IOException {
 		Program parsedProgram = new ProgramParser().parse(testProgram);
 		this.atomStore = new AtomStoreImpl();
 		this.grounder = new NaiveGrounder(parsedProgram, atomStore, true);
-		this.assignment = new TrailAssignment(atomStore);
+		this.assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		this.choiceManager = new TestableChoiceManager(assignment, new NaiveNoGoodStore(assignment));
 	}
 
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java
index 29227058f..5d660946e 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java
@@ -62,7 +62,7 @@ public class BerkMinTest {
 	public void setUp() {
 		AtomStore atomStore = new AtomStoreImpl();
 		AtomStoreTest.fillAtomStore(atomStore, 2);
-		WritableAssignment assignment = new TrailAssignment(atomStore);
+		WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		assignment.growForMaxAtomId();
 		this.berkmin = new BerkMin(
 			assignment,
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java
index 519f14169..8254e889d 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java
@@ -48,7 +48,7 @@ public class BranchingHeuristicFactoryTest {
 	@Before
 	public void setUp() {
 		AtomStore atomStore = new AtomStoreImpl();
-		WritableAssignment assignment = new TrailAssignment(atomStore);
+		WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks);
 		this.choiceManager = new ChoiceManager(assignment, store);
 	}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java
index a73882ed5..a8955bd78 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java
@@ -55,7 +55,7 @@ public class HeapOfActiveAtomsTest {
 	@Before
 	public void setUp() {
 		atomStore = new AtomStoreImpl();
-		assignment = new TrailAssignment(atomStore);
+		assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		noGoodStore = new NoGoodStoreAlphaRoaming(assignment);
 		ChoiceManager choiceManager = new PseudoChoiceManager(assignment, noGoodStore);
 		this.vsids = new VSIDS(assignment, choiceManager, MOMs.DEFAULT_STRATEGY);
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java
index 81ec7bbd1..d6b8796a5 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java
@@ -48,7 +48,7 @@ public class ReplayHeuristicTest {
 	@Before
 	public void setUp() {
 		AtomStore atomStore = new AtomStoreImpl();
-		WritableAssignment assignment = new TrailAssignment(atomStore);
+		WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks);
 		this.choiceManager = new PseudoChoiceManager(assignment, store);
 	}
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java
index e4f4f714f..71f10e96c 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java
@@ -68,7 +68,7 @@ public class VSIDSTest {
 	public void setUp() {
 		atomStore = new AtomStoreImpl();
 		AtomStoreTest.fillAtomStore(atomStore, 4);
-		assignment = new TrailAssignment(atomStore);
+		assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		assignment.growForMaxAtomId();
 		noGoodStore = new NoGoodStoreAlphaRoaming(assignment);
 		this.vsids = new VSIDS(
diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java
index 238894bbd..9ec7ecfdf 100644
--- a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java
+++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java
@@ -5,6 +5,7 @@
 import at.ac.tuwien.kr.alpha.common.AtomStoreTest;
 import at.ac.tuwien.kr.alpha.common.NoGood;
 import at.ac.tuwien.kr.alpha.solver.*;
+import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory;
 import org.junit.Ignore;
 import org.junit.Test;
 
@@ -24,7 +25,7 @@ public class GroundConflictNoGoodLearnerTest {
 	public GroundConflictNoGoodLearnerTest() {
 		atomStore = new AtomStoreImpl();
 		AtomStoreTest.fillAtomStore(atomStore, 20);
-		this.assignment = new TrailAssignment(atomStore);
+		this.assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue());
 		this.assignment.growForMaxAtomId();
 		this.store = new NoGoodStoreAlphaRoaming(assignment);
 		this.store.growForMaxAtomId(20);