diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/RebootStrategyEnum.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/RebootStrategyEnum.java
new file mode 100644
index 000000000..483925416
--- /dev/null
+++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/RebootStrategyEnum.java
@@ -0,0 +1,22 @@
+package at.ac.tuwien.kr.alpha.api.config;
+
+import java.util.Arrays;
+import java.util.stream.Collectors;
+
+/**
+ * The available reboot strategies.
+ */
+public enum RebootStrategyEnum {
+	FIXED,
+	GEOM,
+	LUBY,
+	ASSIGN,
+	ANSWER;
+
+	/**
+	 * @return a comma-separated list of names of known reboot strategies
+	 */
+	public static String listAllowedValues() {
+		return Arrays.stream(values()).map(RebootStrategyEnum::toString).collect(Collectors.joining(", "));
+	}
+}
diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java
index 27019ce10..2b54c84c9 100644
--- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java
+++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java
@@ -36,7 +36,7 @@
 
 /**
  * Config structure for {@link Alpha} instances.
- * 
+ *
  * Copyright (c) 2021, the Alpha Team.
  */
 public class SystemConfig {
@@ -49,6 +49,12 @@ public class SystemConfig {
 	public static final String DEFAULT_NOGOOD_STORE_NAME = "alphaRoaming";
 	public static final Heuristic DEFAULT_BRANCHING_HEURISTIC = Heuristic.VSIDS;
 	public static final BinaryNoGoodPropagationEstimationStrategy DEFAULT_MOMS_STRATEGY = BinaryNoGoodPropagationEstimationStrategy.CountBinaryWatches;
+	public static final boolean DEFAULT_REBOOT_ENABLED = false;
+	public static final boolean DEFAULT_DISABLE_REBOOT_REPEAT = false;
+	public static final RebootStrategyEnum DEFAULT_REBOOT_STRATEGY = RebootStrategyEnum.ANSWER;
+	public static final int DEFAULT_REBOOT_STRATEGY_INTERVAL = 10000;
+	public static final double DEFAULT_REBOOT_STRATEGY_BASE = 1.5;
+	public static final double DEFAULT_REBOOT_STRATEGY_FACTOR = 2;
 	public static final long DEFAULT_SEED = System.nanoTime();
 	public static final boolean DEFAULT_DETERMINISTIC = false;
 	public static final boolean DEFAULT_PRINT_STATS = false;
@@ -73,6 +79,12 @@ public class SystemConfig {
 	private boolean debugInternalChecks = DEFAULT_DEBUG_INTERNAL_CHECKS;
 	private Heuristic branchingHeuristic = DEFAULT_BRANCHING_HEURISTIC;
 	private BinaryNoGoodPropagationEstimationStrategy momsStrategy = DEFAULT_MOMS_STRATEGY;
+	private boolean rebootEnabled = DEFAULT_REBOOT_ENABLED;
+	private boolean disableRebootRepeat = DEFAULT_DISABLE_REBOOT_REPEAT;
+	private RebootStrategyEnum rebootStrategy = DEFAULT_REBOOT_STRATEGY;
+	private int rebootStrategyInterval = DEFAULT_REBOOT_STRATEGY_INTERVAL;
+	private double rebootStrategyBase = DEFAULT_REBOOT_STRATEGY_BASE;
+	private double rebootStrategyFactor = DEFAULT_REBOOT_STRATEGY_FACTOR;
 	private boolean quiet = DEFAULT_QUIET;
 	private boolean printStats = DEFAULT_PRINT_STATS;
 	private boolean disableJustificationSearch = DEFAULT_DISABLE_JUSTIFICATION_SEARCH;
@@ -119,6 +131,58 @@ public void setNogoodStoreName(String nogoodStoreName) {
 		this.nogoodStoreName = nogoodStoreName;
 	}
 
+	public boolean isRebootEnabled() {
+		return this.rebootEnabled;
+	}
+
+	public void setRebootEnabled(boolean rebootEnabled) {
+		this.rebootEnabled = rebootEnabled;
+	}
+
+	public boolean isDisableRebootRepeat() {
+		return this.disableRebootRepeat;
+	}
+
+	public void setDisableRebootRepeat(boolean disableRebootRepeat) {
+		this.disableRebootRepeat = disableRebootRepeat;
+	}
+
+	public RebootStrategyEnum getRebootStrategy() {
+		return this.rebootStrategy;
+	}
+
+	public void setRebootStrategy(RebootStrategyEnum rebootStrategy) {
+		this.rebootStrategy = rebootStrategy;
+	}
+
+	public void setRebootStrategyName(String rebootStrategyName) {
+		this.rebootStrategy = RebootStrategyEnum.valueOf(rebootStrategyName.replace("-", "_").toUpperCase());
+	}
+
+	public int getRebootStrategyInterval() {
+		return this.rebootStrategyInterval;
+	}
+
+	public void setRebootStrategyInterval(int rebootStrategyInterval) {
+		this.rebootStrategyInterval = rebootStrategyInterval;
+	}
+
+	public double getRebootStrategyBase() {
+		return this.rebootStrategyBase;
+	}
+
+	public void setRebootStrategyBase(double rebootStrategyBase) {
+		this.rebootStrategyBase = rebootStrategyBase;
+	}
+
+	public double getRebootStrategyFactor() {
+		return this.rebootStrategyFactor;
+	}
+
+	public void setRebootStrategyFactor(double rebootStrategyFactor) {
+		this.rebootStrategyFactor = rebootStrategyFactor;
+	}
+
 	public boolean isDeterministic() {
 		return this.deterministic;
 	}
diff --git a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java
index 857705f97..7d7cad2d0 100644
--- a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java
+++ b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java
@@ -34,6 +34,7 @@
 import java.util.Map;
 import java.util.function.Consumer;
 
+import at.ac.tuwien.kr.alpha.api.config.*;
 import org.apache.commons.cli.CommandLine;
 import org.apache.commons.cli.DefaultParser;
 import org.apache.commons.cli.HelpFormatter;
@@ -45,13 +46,6 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import at.ac.tuwien.kr.alpha.api.config.AggregateRewritingConfig;
-import at.ac.tuwien.kr.alpha.api.config.AlphaConfig;
-import at.ac.tuwien.kr.alpha.api.config.BinaryNoGoodPropagationEstimationStrategy;
-import at.ac.tuwien.kr.alpha.api.config.Heuristic;
-import at.ac.tuwien.kr.alpha.api.config.InputConfig;
-import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
-
 /**
  * Parses given argument lists (as passed when Alpha is called from command line) into {@link SystemConfig}s and
  * {@link InputConfig}s.
@@ -98,6 +92,21 @@ public class CommandLineParser {
 			.desc("the solver implementation to use (default: " + SystemConfig.DEFAULT_SOLVER_NAME + ")").build();
 	private static final Option OPT_NOGOOD_STORE = Option.builder("r").longOpt("store").hasArg(true).argName("store")
 			.desc("the nogood store to use (default: " + SystemConfig.DEFAULT_NOGOOD_STORE_NAME + ")").build();
+	private static final Option OPT_REBOOT_ENABLED = Option.builder("rbt").longOpt("enableReboot")
+			.desc("enable solver reboots (default: " + SystemConfig.DEFAULT_REBOOT_ENABLED + ")").build();
+	private static final Option OPT_NO_REBOOT_REPEAT = Option.builder("drr").longOpt("disableRebootRepeat")
+			.desc("disables repeated reboots resulting in at most one reboot during solving, only effective if reboot is enabled (default: " + SystemConfig.DEFAULT_DISABLE_REBOOT_REPEAT + ")").build();
+	private static final Option OPT_REBOOT_STRATEGY = Option.builder("rbs").longOpt("rebootStrategy").hasArg(true).argName("strategy")
+			.desc("the reboot strategy to use (default: " + SystemConfig.DEFAULT_REBOOT_STRATEGY.name() + ")").build();
+	private static final Option OPT_REBOOT_STRATEGY_INTERVAL = Option.builder("rsi").longOpt("rebootStrategyInterval")
+			.hasArg(true).argName("number").type(Integer.class)
+			.desc("the size of the interval between reboots for a fixed reboot strategy (default: " + SystemConfig.DEFAULT_REBOOT_STRATEGY_INTERVAL + ")").build();
+	private static final Option OPT_REBOOT_STRATEGY_BASE = Option.builder("rsb").longOpt("rebootStrategyBase")
+			.hasArg(true).argName("number").type(Double.class)
+			.desc("the base value of a reboot strategy (default: " + SystemConfig.DEFAULT_REBOOT_STRATEGY_BASE + ")").build();
+	private static final Option OPT_REBOOT_STRATEGY_FACTOR = Option.builder("rsf").longOpt("rebootStrategyFactor")
+			.hasArg(true).argName("number").type(Double.class)
+			.desc("the scaling factor of a reboot strategy (default: " + SystemConfig.DEFAULT_REBOOT_STRATEGY_FACTOR + ")").build();
 	private static final Option OPT_SORT = Option.builder("sort").longOpt("sort").hasArg(false)
 			.desc("sort answer sets (default: " + SystemConfig.DEFAULT_SORT_ANSWER_SETS + ")").build();
 	private static final Option OPT_DETERMINISTIC = Option.builder("d").longOpt("deterministic").hasArg(false)
@@ -174,6 +183,12 @@ public class CommandLineParser {
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_SOLVER);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NOGOOD_STORE);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REBOOT_ENABLED);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_REBOOT_REPEAT);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REBOOT_STRATEGY);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REBOOT_STRATEGY_INTERVAL);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REBOOT_STRATEGY_BASE);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REBOOT_STRATEGY_FACTOR);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_SORT);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_DETERMINISTIC);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_SEED);
@@ -232,6 +247,12 @@ private void initializeGlobalOptionHandlers() {
 		this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER.getOpt(), this::handleGrounder);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_SOLVER.getOpt(), this::handleSolver);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_NOGOOD_STORE.getOpt(), this::handleNogoodStore);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_REBOOT_ENABLED.getOpt(), this::handleRebootEnabled);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_NO_REBOOT_REPEAT.getOpt(), this::handleDisableRebootRepeat);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_REBOOT_STRATEGY.getOpt(), this::handleRebootStrategy);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_REBOOT_STRATEGY_INTERVAL.getOpt(), this::handleRebootStrategyInterval);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_REBOOT_STRATEGY_BASE.getOpt(), this::handleRebootStrategyBase);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_REBOOT_STRATEGY_FACTOR.getOpt(), this::handleRebootStrategyFactor);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_SORT.getOpt(), this::handleSort);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_DETERMINISTIC.getOpt(), this::handleDeterministic);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_SEED.getOpt(), this::handleSeed);
@@ -353,6 +374,57 @@ private void handleNogoodStore(Option opt, SystemConfig cfg) {
 		cfg.setNogoodStoreName(opt.getValue(SystemConfig.DEFAULT_NOGOOD_STORE_NAME));
 	}
 
+	private void handleRebootEnabled(Option opt, SystemConfig cfg) {
+		cfg.setRebootEnabled(true);
+	}
+
+	private void handleDisableRebootRepeat(Option opt, SystemConfig cfg) {
+		cfg.setDisableRebootRepeat(true);
+	}
+
+	private void handleRebootStrategy(Option opt, SystemConfig cfg) throws ParseException {
+		String rebootStrategyName = opt.getValue(SystemConfig.DEFAULT_REBOOT_STRATEGY.name());
+		try {
+			cfg.setRebootStrategyName(rebootStrategyName);
+		} catch (IllegalArgumentException e) {
+			throw new ParseException(
+					"Unknown reboot strategy: " + rebootStrategyName + ". Please try one of the following: " + RebootStrategyEnum.listAllowedValues());
+		}
+	}
+
+	private void handleRebootStrategyInterval(Option opt, SystemConfig cfg) {
+		String optVal = opt.getValue();
+		int limit;
+		if (optVal != null) {
+			limit = Integer.parseInt(optVal);
+			cfg.setRebootStrategyInterval(limit);
+		} else {
+			cfg.setRebootStrategyInterval(SystemConfig.DEFAULT_REBOOT_STRATEGY_INTERVAL);
+		}
+	}
+
+	private void handleRebootStrategyBase(Option opt, SystemConfig cfg) {
+		String optVal = opt.getValue();
+		double limit;
+		if (optVal != null) {
+			limit = Double.parseDouble(optVal);
+			cfg.setRebootStrategyBase(limit);
+		} else {
+			cfg.setRebootStrategyBase(SystemConfig.DEFAULT_REBOOT_STRATEGY_BASE);
+		}
+	}
+
+	private void handleRebootStrategyFactor(Option opt, SystemConfig cfg) {
+		String optVal = opt.getValue();
+		double limit;
+		if (optVal != null) {
+			limit = Double.parseDouble(optVal);
+			cfg.setRebootStrategyFactor(limit);
+		} else {
+			cfg.setRebootStrategyFactor(SystemConfig.DEFAULT_REBOOT_STRATEGY_FACTOR);
+		}
+	}
+
 	private void handleFilters(Option opt, InputConfig cfg) {
 		String pred = opt.getValue().trim();
 		cfg.getDesiredPredicates().add(pred);
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java
index c02edbd48..3585329ce 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStore.java
@@ -116,4 +116,9 @@ default <T extends NoGoodInterface> String noGoodToString(T noGood) {
 	}
 
 	AtomCounter getAtomCounter();
+
+	/**
+	 * Clears all data within the atom store and resets it to its initial empty state.
+	 */
+	void reset();
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStoreImpl.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStoreImpl.java
index 646a172a1..edab1d88b 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStoreImpl.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/AtomStoreImpl.java
@@ -129,4 +129,19 @@ public int get(Atom atom) {
 	public AtomCounter getAtomCounter() {
 		return atomCounter;
 	}
+
+	@Override
+	public void reset() {
+		atomIdsToInternalBasicAtoms.clear();
+		atomIdsToInternalBasicAtoms.add(null);
+
+		predicateInstancesToAtomIds.clear();
+
+		atomIdGenerator.resetGenerator();
+		atomIdGenerator.getNextId();
+
+		releasedAtomIds.clear();
+
+		atomCounter.reset();
+	}
 }
\ No newline at end of file
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceRecorder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceRecorder.java
index 375bf6410..400411a1d 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceRecorder.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceRecorder.java
@@ -71,7 +71,6 @@ public Map<Integer, Set<Integer>> getAndResetHeadsToBodies() {
 		return currentHeadsToBodies;
 	}
 
-	
 	public List<NoGood> generateChoiceNoGoods(final List<Integer> posLiterals, final List<Integer> negLiterals, final int bodyRepresentingLiteral) {
 		// Obtain an ID for this new choice.
 		final int choiceId = ID_GENERATOR.getNextId();
@@ -94,7 +93,7 @@ private NoGood generatePos(final int atomOn, List<Integer> posLiterals) {
 		return NoGood.fromBodyInternal(posLiterals, emptyList(), literalOn);
 	}
 
-	private List<NoGood> generateNeg(final int atomOff, List<Integer> negLiterals)  {
+	private List<NoGood> generateNeg(final int atomOff, List<Integer> negLiterals) {
 		final int negLiteralOff = negateLiteral(atomToLiteral(atomOff));
 
 		final List<NoGood> noGoods = new ArrayList<>(negLiterals.size() + 1);
@@ -115,6 +114,12 @@ public void addHeadToBody(int headId, int bodyId) {
 		existingBodies.add(bodyId);
 	}
 
+	public void reset() {
+		ID_GENERATOR.resetGenerator();
+		newChoiceAtoms = new ImmutablePair<>(new LinkedHashMap<>(), new LinkedHashMap<>());
+		newHeadsToBodies = new LinkedHashMap<>();
+	}
+
 	@Override
 	public String toString() {
 		StringBuilder sb = new StringBuilder("[enablers: ");
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java
index 2675337ce..e0bfbdd31 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java
@@ -43,6 +43,7 @@
 import java.util.SortedSet;
 import java.util.TreeSet;
 
+import at.ac.tuwien.kr.alpha.api.programs.terms.ConstantTerm;
 import org.apache.commons.lang3.tuple.ImmutablePair;
 import org.apache.commons.lang3.tuple.Pair;
 import org.slf4j.Logger;
@@ -82,7 +83,7 @@
  *
  * Copyright (c) 2016-2020, the Alpha Team.
  */
-public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGrounder {
+public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGrounder, RebootableGrounder {
 	private static final Logger LOGGER = LoggerFactory.getLogger(NaiveGrounder.class);
 
 	private final WorkingMemory workingMemory = new WorkingMemory();
@@ -139,6 +140,7 @@ private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeur
 
 		this.debugInternalChecks = debugInternalChecks;
 
+
 		// Initialize RuleInstantiator and instantiation strategy. Note that the instantiation strategy also
 		// needs the current assignment, which is set with every call of getGroundInstantiations.
 		this.instantiationStrategy = new DefaultLazyGroundingInstantiationStrategy(this.workingMemory, this.atomStore, this.factsFromProgram,
@@ -364,7 +366,7 @@ public Map<Integer, NoGood> getNoGoods(Assignment currentAssignment) {
 			modifiedWorkingMemory.markRecentlyAddedInstancesDone();
 		}
 
-		workingMemory.reset();
+		workingMemory.resetModified();
 		for (Atom removeAtom : removeAfterObtainingNewNoGoods) {
 			final IndexedInstanceStorage storage = workingMemory.get(removeAtom, true);
 			Instance instance = new Instance(removeAtom.getTerms());
@@ -412,6 +414,37 @@ public int register(NoGood noGood) {
 		return registry.register(noGood);
 	}
 
+	@Override
+	public void reboot(Assignment currentAssignment) {
+		workingMemory.reset();
+		registry.reset();
+		noGoodGenerator.reset();
+		choiceRecorder.reset();
+		analyzeUnjustified.reset();
+		rulesUsingPredicateWorkingMemory.clear();
+		removeAfterObtainingNewNoGoods = new LinkedHashSet<>();
+		instantiationStrategy.setStaleWorkingMemoryEntries(removeAfterObtainingNewNoGoods);
+		instantiationStrategy.setCurrentAssignment(currentAssignment);
+		fixedRules = new ArrayList<>();
+		initializeFactsAndRules();
+	}
+
+	@Override
+	public Map<Integer, NoGood> forceRuleGrounding(RuleAtom atom) {
+		Map<Integer, NoGood> newNoGoods = new LinkedHashMap<>();
+
+		// Translate RuleAtom back to NonGroundRule + Substitution.
+		RuleAtom.RuleAtomData ruleAtomData = (RuleAtom.RuleAtomData) ((ConstantTerm<?>)(atom.getTerms().get(0))).getObject();
+		CompiledRule nonGroundRule = ruleAtomData.getNonGroundRule();
+		Substitution groundingSubstitution = ruleAtomData.getSubstitution();
+
+		// Generate the rules that correspond to the RuleAtom
+		List<NoGood> generatedNoGoods = noGoodGenerator.generateNoGoodsFromGroundSubstitution(
+				nonGroundRule, groundingSubstitution);
+		registry.register(generatedNoGoods, newNoGoods);
+		return newNoGoods;
+	}
+
 	// Ideally, this method should be private. It's only visible because NaiveGrounderTest needs to access it.
 	BindingResult getGroundInstantiations(CompiledRule rule, RuleGroundingOrder groundingOrder, Substitution partialSubstitution,
 			Assignment currentAssignment) {
@@ -438,7 +471,7 @@ BindingResult getGroundInstantiations(CompiledRule rule, RuleGroundingOrder grou
 	}
 
 	/**
-	 * Helper method used by {@link NaiveGrounder#bindNextAtomInRule(RuleGroundingOrderImpl, int, int, int, BasicSubstitution)}.
+	 * Helper method used by {@link NaiveGrounder#bindNextAtomInRule(RuleGroundingOrder, int, int, int, Substitution)}.
 	 *
 	 * Takes an <code>ImmutablePair</code> of a {@link BasicSubstitution} and an accompanying {@link AssignmentStatus} and calls
 	 * <code>bindNextAtomInRule</code> for the next literal in the grounding order.
@@ -620,7 +653,7 @@ public Set<Literal> justifyAtom(int atomToJustify, Assignment currentAssignment)
 
 	/**
 	 * Checks that every nogood not marked as {@link NoGoodInterface.Type#INTERNAL} contains only
-	 * atoms which are not {@link PredicateImpl#isSolverInternal()} (except {@link RuleAtom}s, which are allowed).
+	 * atoms which are not {@link Predicate#isSolverInternal()} (except {@link RuleAtom}s, which are allowed).
 	 *
 	 * @param newNoGoods
 	 */
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java
index 1b06cdec3..97efa5597 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java
@@ -63,6 +63,7 @@ public class NoGoodGenerator {
 	private final Map<Predicate, LinkedHashSet<Instance>> factsFromProgram;
 	private final CompiledProgram programAnalysis;
 	private final Set<CompiledRule> uniqueGroundRulePerGroundHead;
+	private final Set<RuleAtom> groundRuleAtoms;
 
 	NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map<Predicate, LinkedHashSet<Instance>> factsFromProgram, CompiledProgram programAnalysis, Set<CompiledRule> uniqueGroundRulePerGroundHead) {
 		this.atomStore = atomStore;
@@ -70,6 +71,7 @@ public class NoGoodGenerator {
 		this.factsFromProgram = factsFromProgram;
 		this.programAnalysis = programAnalysis;
 		this.uniqueGroundRulePerGroundHead = uniqueGroundRulePerGroundHead;
+		this.groundRuleAtoms = new HashSet<>();
 	}
 
 	/**
@@ -103,14 +105,14 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final CompiledRule nonGroundR
 		// Prepare atom representing the rule body.
 		final RuleAtom bodyAtom = new RuleAtom(nonGroundRule, substitution);
 
-		// Check uniqueness of ground rule by testing whether the
-		// body representing atom already has an id.
-		if (atomStore.contains(bodyAtom)) {
+		// Check uniqueness of ground rule.
+		if (groundRuleAtoms.contains(bodyAtom)) {
 			// The current ground instance already exists,
 			// therefore all nogoods have already been created.
 			return emptyList();
 		}
 
+		groundRuleAtoms.add(bodyAtom);
 		final int bodyRepresentingLiteral = atomToLiteral(atomStore.putIfAbsent(bodyAtom));
 		final int headLiteral = atomToLiteral(atomStore.putIfAbsent(nonGroundRule.getHeadAtom().substitute(substitution)));
 
@@ -162,6 +164,10 @@ List<Integer> collectNegLiterals(final CompiledRule nonGroundRule, final Substit
 		return bodyLiteralsNegative;
 	}
 
+	void reset() {
+		groundRuleAtoms.clear();
+	}
+
 	private List<Integer> collectPosLiterals(final CompiledRule nonGroundRule, final Substitution substitution) {
 		final List<Integer> bodyLiteralsPositive = new ArrayList<>();
 		for (Literal lit  : nonGroundRule.getPositiveBody()) {
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NogoodRegistry.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NogoodRegistry.java
index 970ab86e6..c6b164675 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NogoodRegistry.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NogoodRegistry.java
@@ -11,6 +11,13 @@ public class NogoodRegistry {
 
 	private Map<NoGood, Integer> registeredIdentifiers = new LinkedHashMap<>();
 
+	/**
+	 * Clears all registered identifiers.
+	 */
+	public void reset() {
+		registeredIdentifiers = new LinkedHashMap<>();
+	}
+
 	/**
 	 * Helper methods to analyze average nogood length.
 	 * @return
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/RebootableGrounder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/RebootableGrounder.java
new file mode 100644
index 000000000..cb56fd0db
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/RebootableGrounder.java
@@ -0,0 +1,47 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.grounder;
+
+import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.core.common.Assignment;
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+
+import java.util.Map;
+
+public interface RebootableGrounder extends Grounder {
+	/**
+	 * Reboots the grounder, returning it to its initial state.
+	 */
+	void reboot(Assignment currentAssignment);
+
+	/**
+	 * Grounds the rule corresponding to the given {@link RuleAtom} and generates the respective {@link NoGood}s
+	 * for this ground rule.
+	 * @param ruleAtom the {@link RuleAtom} to ground the corresponding rule for.
+	 * @return the nogoods resulting from the grounding of the rule.
+	 */
+	Map<Integer, NoGood> forceRuleGrounding(RuleAtom ruleAtom);
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WorkingMemory.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WorkingMemory.java
index 549feddf0..9bd9eb068 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WorkingMemory.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WorkingMemory.java
@@ -27,10 +27,7 @@
  */
 package at.ac.tuwien.kr.alpha.core.grounder;
 
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.LinkedHashSet;
-import java.util.Set;
+import java.util.*;
 
 import org.apache.commons.lang3.tuple.ImmutablePair;
 
@@ -104,11 +101,28 @@ public void addInstances(Predicate predicate, boolean value, Iterable<Instance>
 		}
 	}
 
-	public void reset() {
+	/**
+	 * Resets the modified working memory entries.
+	 */
+	public void resetModified() {
 		modifiedWorkingMemories = new LinkedHashSet<>();
 	}
 
+	/**
+	 * Returns all recently modified working memory entries.
+	 * @return the set of working memory entries that were modified since the last call
+	 * to {@link WorkingMemory#resetModified}.
+	 */
 	public Set<IndexedInstanceStorage> modified() {
 		return modifiedWorkingMemories;
 	}
+
+	/**
+	 * Resets the modified working memory entries using {@link WorkingMemory#resetModified} and
+	 * clears the whole working memory.
+	 */
+	public void reset() {
+		resetModified();
+		workingMemory = new LinkedHashMap<>();
+	}
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustified.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustified.java
index 751f68599..00de465b6 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustified.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AnalyzeUnjustified.java
@@ -80,6 +80,11 @@ public Set<Literal> analyze(int atomToJustify, Assignment currentAssignment) {
 		return analyze((BasicAtom) atom, currentAssignment);
 	}
 
+	public void reset() {
+		renamingCounter = 0;
+		padDepth = 0;
+	}
+
 	private Set<Literal> analyze(BasicAtom atom, Assignment currentAssignment) {
 		log(pad("Starting analyze, current assignment is: {}"), currentAssignment);
 		LinkedHashSet<Literal> vL = new LinkedHashSet<>();
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java
index 34fed23dc..fe7799a6a 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java
@@ -80,7 +80,7 @@ public InternalProgram apply(AnalyzedProgram inputProgram) {
 			}
 		}
 
-		workingMemory.reset();
+		workingMemory.resetModified();
 
 		// Set up literal instantiator.
 		literalInstantiator = new LiteralInstantiator(new WorkingMemoryBasedInstantiationStrategy(workingMemory));
@@ -150,7 +150,7 @@ private void evaluateComponent(ComponentGraph.SCComponent comp) {
 	}
 
 	private void evaluateRules(Set<CompiledRule> rules, boolean isInitialRun) {
-		workingMemory.reset();
+		workingMemory.resetModified();
 		LOGGER.debug("Starting component evaluation run...");
 		for (CompiledRule r : rules) {
 			evaluateRule(r, !isInitialRun);
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounter.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounter.java
index 753f04a8a..21197d5dd 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounter.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCounter.java
@@ -66,4 +66,8 @@ public String getStatsByType() {
 		return String.join(" ", statsList);
 	}
 
+	public void reset() {
+		countByType.clear();
+	}
+
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java
index 8ab9088d3..f7c1f5816 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java
@@ -181,6 +181,15 @@ void setActivityListener(ActivityListener listener) {
 		this.activityListener = listener;
 	}
 
+	/**
+	 * Clear all active choice point and influencer information.
+	 */
+	public void reset() {
+		activeChoicePoints.clear();
+		activeChoicePointsAtoms.clear();
+		influencers = new ChoicePoint[0];
+	}
+
 	private class ChoicePoint {
 		final Integer atom;
 		final int enabler;
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java
index 343fe2eab..527bffd82 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java
@@ -30,14 +30,8 @@
 import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
 import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral;
 
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Map;
+import java.util.*;
 import java.util.Map.Entry;
-import java.util.Set;
-import java.util.Stack;
 import java.util.stream.Collectors;
 
 import org.apache.commons.lang3.tuple.Pair;
@@ -262,6 +256,40 @@ public BinaryNoGoodPropagationEstimation getBinaryNoGoodPropagationEstimation()
 		return bnpEstimation;
 	}
 
+	/**
+	 * Returns the current choice stack as a list of choices containing atom ids.
+	 * @return a list of the choices on the current choice stack ordered from oldest to newest.
+	 */
+	public List<Choice> getChoiceList() {
+		return new ArrayList<>(choiceStack);
+	}
+
+	/**
+	 * Reset the current choice influence manager. Then clear the current choice stack and mappings
+	 * between rule heads and bodies.
+	 */
+	public void reset() {
+		choicePointInfluenceManager.reset();
+		choiceStack.clear();
+		headsToBodies.clear();
+		bodiesToHeads.clear();
+	}
+
+	/**
+	 * Make the given choice if its atom is an active choice atom.
+	 *
+	 * @param choice the choice to make.
+	 * @return whether the atom of the given choice was an active choice atom.
+	 */
+	public boolean replayChoice(Choice choice) {
+		if (isActiveChoiceAtom(choice.getAtom())) {
+			choose(choice);
+			return true;
+		} else {
+			return false;
+		}
+	}
+
 	/**
 	 * A helper class for halting the debugger when certain assignments occur on the choice stack.
 	 *
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java
index ab5642ad8..ebf73c375 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java
@@ -35,17 +35,15 @@
 import static at.ac.tuwien.kr.alpha.core.solver.heuristics.BranchingHeuristic.DEFAULT_CHOICE_LITERAL;
 import static at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult.UNSAT;
 
-import java.util.ArrayList;
-import java.util.Iterator;
-import java.util.LinkedHashMap;
-import java.util.LinkedHashSet;
-import java.util.LinkedList;
-import java.util.Map;
+import java.util.*;
 import java.util.Map.Entry;
-import java.util.Random;
-import java.util.Set;
 import java.util.function.Consumer;
 
+import at.ac.tuwien.kr.alpha.core.common.Assignment;
+import at.ac.tuwien.kr.alpha.core.grounder.RebootableGrounder;
+import at.ac.tuwien.kr.alpha.core.solver.reboot.AtomizedChoice;
+import at.ac.tuwien.kr.alpha.core.solver.reboot.RebootManager;
+import at.ac.tuwien.kr.alpha.core.solver.reboot.strategies.*;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -81,9 +79,13 @@ public class DefaultSolver extends AbstractSolver implements StatisticsReporting
 
 	private final NoGoodStore store;
 	private final ChoiceManager choiceManager;
+	private final RebootManager rebootManager;
 	private final WritableAssignment assignment;
 	private final GroundConflictNoGoodLearner learner;
 	private final BranchingHeuristic branchingHeuristic;
+	private final RebootStrategy rebootStrategy;
+	private boolean rebootEnabled;
+	private final boolean disableRebootRepeat;
 
 	private int mbtAtFixpoint;
 	private int conflictsAfterClosing;
@@ -101,7 +103,7 @@ private static class SearchState {
 	private final SearchState searchState = new SearchState();
 
 	private final PerformanceLog performanceLog;
-	
+
 	public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, WritableAssignment assignment, Random random, SystemConfig config, HeuristicsConfiguration heuristicsConfiguration) {
 		super(atomStore, grounder);
 
@@ -109,11 +111,22 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store,
 		this.store = store;
 		this.choiceManager = new ChoiceManager(assignment, store);
 		this.choiceManager.setChecksEnabled(config.isDebugInternalChecks());
+		this.rebootManager = new RebootManager(atomStore);
 		this.learner = new GroundConflictNoGoodLearner(assignment, atomStore);
 		this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration);
 		this.disableJustifications = config.isDisableJustificationSearch();
 		this.disableNoGoodDeletion = config.isDisableNoGoodDeletion();
+
+		this.rebootEnabled = config.isRebootEnabled();
+		this.disableRebootRepeat = config.isDisableRebootRepeat();
+		this.rebootStrategy = RebootStrategyFactory.getRebootStrategy(config);
+
 		this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000);
+
+		if (this.rebootEnabled && !(grounder instanceof RebootableGrounder)) {
+			this.rebootEnabled = false;
+			LOGGER.warn("Reboot was disabled since grounder does not support it.");
+		}
 	}
 
 	private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) {
@@ -136,6 +149,7 @@ protected boolean tryAdvance(Consumer<? super AnswerSet> action) {
 		}
 		// Try all assignments until grounder reports no more NoGoods and all of them are satisfied
 		while (true) {
+			rebootStrategy.nextIteration();
 			performanceLog.writeIfTimeForLogging(LOGGER);
 			if (searchState.isSearchSpaceCompletelyExplored) {
 				LOGGER.debug("Search space has been fully explored, there are no more answer-sets.");
@@ -146,19 +160,26 @@ protected boolean tryAdvance(Consumer<? super AnswerSet> action) {
 			if (conflictCause != null) {
 				LOGGER.debug("Conflict encountered, analyzing conflict.");
 				learnFromConflict(conflictCause);
+				rebootStrategy.conflictEncountered();
 			} else if (assignment.didChange()) {
 				LOGGER.debug("Updating grounder with new assignments and (potentially) obtaining new NoGoods.");
-				grounder.updateAssignment(assignment.getNewPositiveAssignmentsIterator());
-				getNoGoodsFromGrounderAndIngest();
+				syncWithGrounder();
+			} else if (rebootEnabled && rebootStrategy.isRebootScheduled()) {
+				reboot();
+				rebootStrategy.rebootPerformed();
+				disableRebootIfNoRepeat();
 			} else if (choose()) {
 				LOGGER.debug("Did choice.");
+				rebootStrategy.decisionMade();
 			} else if (close()) {
 				LOGGER.debug("Closed unassigned known atoms (assigning FALSE).");
 			} else if (assignment.getMBTCount() == 0) {
 				provideAnswerSet(action);
+				rebootStrategy.answerSetFound();
 				return true;
 			} else {
 				backtrackFromMBTsRemaining();
+				rebootStrategy.backtrackJustified();
 			}
 		}
 	}
@@ -170,6 +191,15 @@ private void initializeSearch() {
 		searchState.hasBeenInitialized = true;
 	}
 
+	/**
+	 * Updates the assignment for the grounder and then gets new {@link NoGood}s from the grounder
+	 * by calling {@link DefaultSolver#getNoGoodsFromGrounderAndIngest()}.
+	 */
+	private void syncWithGrounder() {
+		grounder.updateAssignment(assignment.getNewPositiveAssignmentsIterator());
+		getNoGoodsFromGrounderAndIngest();
+	}
+
 	private void prepareForSubsequentAnswerSet() {
 		// We already found one Answer-Set and are requested to find another one.
 		searchState.afterAllAtomsAssigned = false;
@@ -192,6 +222,8 @@ private void prepareForSubsequentAnswerSet() {
 		// Backjump instead of backtrackSlow, enumerationNoGood will invert last choice.
 		choiceManager.backjump(backjumpLevel - 1);
 		LOGGER.debug("Adding enumeration nogood: {}", enumerationNoGood);
+		rebootManager.newEnumerationNoGood(enumerationNoGood);
+		rebootStrategy.newEnumerationNoGood(enumerationNoGood);
 		if (!addAndBackjumpIfNecessary(grounder.register(enumerationNoGood), enumerationNoGood, Integer.MAX_VALUE)) {
 			searchState.isSearchSpaceCompletelyExplored = true;
 		}
@@ -199,6 +231,7 @@ private void prepareForSubsequentAnswerSet() {
 
 	private void getNoGoodsFromGrounderAndIngest() {
 		Map<Integer, NoGood> obtained = grounder.getNoGoods(assignment);
+		rebootStrategy.newNoGoods(obtained.values());
 		if (!ingest(obtained)) {
 			searchState.isSearchSpaceCompletelyExplored = true;
 		}
@@ -266,7 +299,7 @@ private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd)
 			}
 			choiceManager.backjump(backjumpLevel);
 			if (store.propagate() != null) {
-				throw  oops("Violated NoGood after backtracking.");
+				throw oops("Violated NoGood after backtracking.");
 			}
 		}
 		return true;
@@ -294,6 +327,8 @@ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) {
 
 		choiceManager.backjump(analysisResult.backjumpLevel);
 		final NoGood learnedNoGood = analysisResult.learnedNoGood;
+		rebootManager.newLearnedNoGood(learnedNoGood);
+		rebootStrategy.newLearnedNoGood(learnedNoGood);
 		int noGoodId = grounder.register(learnedNoGood);
 		return addAndBackjumpIfNecessary(noGoodId, learnedNoGood, analysisResult.lbd);
 	}
@@ -322,6 +357,7 @@ private boolean justifyMbtAndBacktrack() {
 		int noGoodID = grounder.register(noGood);
 		Map<Integer, NoGood> obtained = new LinkedHashMap<>();
 		obtained.put(noGoodID, noGood);
+		rebootStrategy.newJustificationNoGood(noGood);
 		LOGGER.debug("Learned NoGood is: {}", atomStore.noGoodToString(noGood));
 		// Add NoGood and trigger backjumping.
 		if (!ingest(obtained)) {
@@ -379,8 +415,8 @@ private boolean treatConflictAfterClosing(Antecedent violatedNoGood) {
 			// For RuleAtoms in toJustify the corresponding ground body contains BasicAtoms that have been assigned FALSE in the closing.
 			// First, get NonGroundRule + Substitution, stored in the RuleAtom's single term.
 			RuleAtom.RuleAtomData ruleAtomData = (RuleAtom.RuleAtomData) ((ConstantTerm<?>)(atom.getTerms().get(0))).getObject();
-			Substitution groundingSubstitution = ruleAtomData.getSubstitution();
 			CompiledRule nonGroundRule = ruleAtomData.getNonGroundRule();
+			Substitution groundingSubstitution = ruleAtomData.getSubstitution();
 			// Find ground literals in the body that have been assigned false and justify those.
 			for (Literal bodyLiteral : nonGroundRule.getBody()) {
 				Atom groundAtom = bodyLiteral.getAtom().substitute(groundingSubstitution);
@@ -412,7 +448,10 @@ private boolean treatConflictAfterClosing(Antecedent violatedNoGood) {
 			return false;
 		}
 		// Add newly obtained noGoods.
-		if (!ingest(obtained)) {
+		boolean success = ingest(obtained);
+		rebootManager.newLearnedNoGoods(obtained.values());
+		rebootStrategy.newLearnedNoGoods(obtained.values());
+		if (!success) {
 			logStats();
 			return false;
 		}
@@ -458,11 +497,7 @@ private boolean backtrack() {
 	}
 
 	private boolean ingest(Map<Integer, NoGood> obtained) {
-		assignment.growForMaxAtomId();
-		int maxAtomId = atomStore.getMaxAtomId();
-		store.growForMaxAtomId(maxAtomId);
-		choiceManager.growForMaxAtomId(maxAtomId);
-		branchingHeuristic.growForMaxAtomId(maxAtomId);
+		growForMaxAtomId();
 		branchingHeuristic.newNoGoods(obtained.values());
 
 		LinkedList<Map.Entry<Integer, NoGood>> noGoodsToAdd = new LinkedList<>(obtained.entrySet());
@@ -524,7 +559,150 @@ private boolean choose() {
 		choiceManager.choose(new Choice(literal, false));
 		return true;
 	}
-	
+
+	/**
+	 * Performs a reboot of the solving process while preserving the current assignment - and thus the progress made.
+	 * {@link NoGoodStore} and {@link Grounder} are reset. Then the {@link AtomStore} is emptied and the current
+	 * assignment is reconstructed.
+	 */
+	private void reboot() {
+		LOGGER.info("Performing solver and grounder reboot.");
+
+		RebootableGrounder rebootableGrounder = (RebootableGrounder) grounder;
+		Stack<AtomizedChoice> atomizedChoiceStack = getAtomizedChoiceStack();
+
+		store.reset();
+		branchingHeuristic.reset();
+		assignment.clear();
+		rebootableGrounder.reboot(assignment);
+		atomStore.reset();
+		choiceManager.reset();
+
+		syncWithGrounder();
+		ingestNoGoodCollection(rebootManager.getEnumerationNoGoods());
+		ingestNoGoodCollection(rebootManager.getLearnedNoGoods());
+		ingestNoGoodsFromRulesOfRuleAtoms(rebootManager.getDiscoveredRuleAtoms());
+		replayAtomizedChoiceStack(atomizedChoiceStack);
+
+		LOGGER.info("Solver and grounder reboot finished.");
+	}
+
+	/**
+	 * Extracts the current choice stack with atom ids replaced by the respective {@link Atom}s.
+	 * @return the choice stack containing {@link Atom}s instead of atom ids.
+	 */
+	private Stack<AtomizedChoice> getAtomizedChoiceStack() {
+		List<Choice> choiceList = choiceManager.getChoiceList();
+		Stack<AtomizedChoice> choiceStack = new Stack<>();
+		for (Choice choice : choiceList) {
+			Atom atom = atomStore.get(choice.getAtom());
+			choiceStack.push(new AtomizedChoice(atom, choice.getTruthValue(), choice.isBacktracked()));
+		}
+		return choiceStack;
+	}
+
+	/**
+	 * Converts the given choice stack into one containing atom ids instead of atoms and applies
+	 * the choices to the resulting choice stack using the {@link DefaultSolver#choiceManager}.
+	 * Propagation is performed initially and after each choice.
+	 * @param atomizedChoiceStack the stack of choices containing atoms.
+	 */
+	private void replayAtomizedChoiceStack(Stack<AtomizedChoice> atomizedChoiceStack) {
+		if (propagate() != null) {
+			throw oops("Conflict in replay during reboot");
+		}
+
+		for (AtomizedChoice atomizedChoice : atomizedChoiceStack) {
+			Atom atom = atomizedChoice.getAtom();
+			atomStore.putIfAbsent(atom);
+		}
+		growForMaxAtomId();
+
+		for (AtomizedChoice atomizedChoice : atomizedChoiceStack) {
+			replayAtomizedChoice(atomizedChoice);
+		}
+	}
+
+	/**
+	 * Applies a given {@link AtomizedChoice} to the current choice stack using the {@link DefaultSolver#choiceManager}.
+	 * Propagation and grounding are performed after the choice.
+	 * @param atomizedChoice the choice to apply.
+	 */
+	private void replayAtomizedChoice(AtomizedChoice atomizedChoice) {
+		Atom atom = atomizedChoice.getAtom();
+		int atomId = atomStore.get(atom);
+		Choice choice = new Choice(atomId, atomizedChoice.getTruthValue(), atomizedChoice.isBacktracked());
+
+		choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies());
+		choiceManager.updateAssignments();
+		boolean activeChoice = choiceManager.replayChoice(choice);
+
+		if (activeChoice) {
+			if (propagate() != null) {
+				throw oops("Conflict in replay during reboot");
+			}
+			syncWithGrounder();
+			if (propagate() != null) {
+				throw oops("Conflict in replay during reboot");
+			}
+		}
+	}
+
+	/**
+	 * Grows the current {@link Assignment}, {@link NoGoodStore}, {@link ChoiceManager} and {@link BranchingHeuristic}
+	 * by calling {@link Assignment#growForMaxAtomId()}, {@link NoGoodStore#growForMaxAtomId(int)},
+	 * {@link ChoiceManager#growForMaxAtomId(int)} and {@link BranchingHeuristic#growForMaxAtomId(int)} respectively.
+	 */
+	private void growForMaxAtomId() {
+		assignment.growForMaxAtomId();
+		int maxAtomId = atomStore.getMaxAtomId();
+		store.growForMaxAtomId(maxAtomId);
+		choiceManager.growForMaxAtomId(maxAtomId);
+		branchingHeuristic.growForMaxAtomId(maxAtomId);
+	}
+
+	/**
+	 * Registers the given collection of {@link NoGood}s at the {@link Grounder}
+	 * and calls {@link DefaultSolver#ingest(Map)} with the resulting ids as keys.
+	 * @param noGoods the {@link NoGood}s to register and ingest.
+	 */
+	private void ingestNoGoodCollection(Collection<NoGood> noGoods) {
+		Map<Integer, NoGood> newNoGoods = new LinkedHashMap<>();
+		for (NoGood noGood : noGoods) {
+			newNoGoods.put(grounder.register(noGood), noGood);
+		}
+		if (!ingest(newNoGoods)) {
+			searchState.isSearchSpaceCompletelyExplored = true;
+		}
+	}
+
+	/**
+	 * Forces the {@link RebootableGrounder} to ground all rules corresponding to the given list of
+	 * {@link RuleAtom}s. Then calls {@link DefaultSolver#ingest(Map)} with the {@link NoGood}s obtained this way.
+	 * This method must not be called if reboots are disabled.
+	 * @param ruleAtoms the {@link RuleAtom}s to ground and ingest the corresponding rules for.
+	 */
+	private void ingestNoGoodsFromRulesOfRuleAtoms(List<RuleAtom> ruleAtoms) {
+		if (!rebootEnabled) {
+			throw oops("Reboot is not enabled but nogood ingestion from rule atoms was called");
+		}
+		RebootableGrounder rebootableGrounder = (RebootableGrounder) grounder;
+		Map<Integer, NoGood> newNoGoods = new LinkedHashMap<>();
+		for (RuleAtom ruleAtom : ruleAtoms) {
+			Map<Integer, NoGood> obtained = rebootableGrounder.forceRuleGrounding(ruleAtom);
+			newNoGoods.putAll(obtained);
+		}
+		if (!ingest(newNoGoods)) {
+			searchState.isSearchSpaceCompletelyExplored = true;
+		}
+	}
+
+	private void disableRebootIfNoRepeat() {
+		if (disableRebootRepeat) {
+			rebootEnabled = false;
+		}
+	}
+
 	@Override
 	public int getNumberOfChoices() {
 		return choiceManager.getChoices();
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStore.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStore.java
index ea86c4e44..3aa2a9331 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStore.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveNoGoodStore.java
@@ -139,6 +139,12 @@ public NoGoodCounter getNoGoodCounter() {
 		return counter;
 	}
 
+	@Override
+	public void reset() {
+		clear();
+		counter.reset();
+	}
+	
 	@Override
 	public void cleanupLearnedNoGoods() {
 	}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodCounter.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodCounter.java
index 3ff15e8e8..4fd591744 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodCounter.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodCounter.java
@@ -125,5 +125,10 @@ public String getStatsByType() {
 	public String getStatsByCardinality() {
 		return "unary: " + getNumberOfUnaryNoGoods() + " binary: " + getNumberOfBinaryNoGoods() + " larger: " + getNumberOfNAryNoGoods();
 	}
+
+	public void reset() {
+		countByType = new int[Type.values().length];
+		countByCardinality = new int[3];
+	}
 	
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStore.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStore.java
index ec70069c1..c3e3e7165 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStore.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStore.java
@@ -49,10 +49,15 @@ public interface NoGoodStore {
 	void growForMaxAtomId(int maxAtomId);
 
 	/**
-	 * Tests whether a cleanup of the learned NoGoods database is appropriate and exectutes the cleaning if
+	 * Tests whether a cleanup of the learned NoGoods database is appropriate and executes the cleaning if
 	 * necessary.
 	 */
 	void cleanupLearnedNoGoods();
 
 	NoGoodCounter getNoGoodCounter();
+
+	/**
+	 * Clears all data within the nogood store.
+	 */
+	void reset();
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java
index 8785ac209..80e450ca9 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NoGoodStoreAlphaRoaming.java
@@ -155,10 +155,18 @@ public NoGoodCounter getNoGoodCounter() {
 		return counter;
 	}
 
+	@Override
+	public void reset() {
+		clear();
+		counter.reset();
+	}
+
+
 	@Override
 	public void cleanupLearnedNoGoods() {
 		if (learnedNoGoodDeletion.needToRunNoGoodDeletion()) {
 			learnedNoGoodDeletion.runNoGoodDeletion();
+			LOGGER.info("Nogood deletion performed.");
 		}
 	}
 
@@ -543,7 +551,6 @@ private void logNoGoodAndAssignment(WatchedNoGood noGood, Assignment assignment)
 	}
 
 	private ConflictCause propagateStrongly(int literal, int currentDecisionLevel, boolean restrictToBinaryNoGoods) {
-
 		// Propagate binary watches.
 		ConflictCause conflictCause = binaryWatches[literal].propagateStrongly();
 		if (conflictCause != null || restrictToBinaryNoGoods) {
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/PerformanceLog.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/PerformanceLog.java
index d9153e729..c85d41879 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/PerformanceLog.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/PerformanceLog.java
@@ -1,17 +1,17 @@
 /**
  * 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
@@ -35,7 +35,7 @@ public class PerformanceLog {
 	private final ChoiceManager choiceManager;
 	private final TrailAssignment assignment;
 	private final long msBetweenOutputs;
-	
+
 	private Long timeFirstEntry;
 	private Long timeLastPerformanceLog;
 	private int numberOfChoicesLastPerformanceLog;
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMin.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMin.java
index ff1c65c7f..3fa8515ca 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMin.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMin.java
@@ -278,4 +278,12 @@ private boolean isUnassigned(int atom) {
 	public String toString() {
 		return this.getClass().getSimpleName();
 	}
+
+	@Override
+	public void reset() {
+		activityCounters = new LinkedHashMap<>();
+		signCounters = new LinkedHashMap<>();
+		stackOfNoGoods = new ArrayDeque<>();
+		stepsSinceLastDecay = 0;
+	}
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMinLiteral.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMinLiteral.java
index 8a46227f6..6935709aa 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMinLiteral.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BerkMinLiteral.java
@@ -79,4 +79,9 @@ protected void pushToStack(NoGood noGood) {
 			}
 		}
 	}
+
+	@Override
+	public void reset() {
+		activeLiterals = new LinkedList<>();
+	}
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristic.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristic.java
index 91a7524d1..6e93eb397 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristic.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristic.java
@@ -81,4 +81,10 @@ default void newNoGoods(Collection<NoGood> newNoGoods) {
 
 	default void growForMaxAtomId(int maxAtomId) {
 	}
+
+	/**
+	 * Reset the state of the heuristic to its initial state.
+	 */
+	default void reset() {
+	}
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/ChainedBranchingHeuristics.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/ChainedBranchingHeuristics.java
index 729386635..0e0736e1e 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/ChainedBranchingHeuristics.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/ChainedBranchingHeuristics.java
@@ -122,4 +122,11 @@ public String toString() {
 		return this.getClass().getSimpleName() + chain;
 	}
 
+	@Override
+	public void reset() {
+		for (BranchingHeuristic heuristic : chain) {
+			heuristic.reset();
+		}
+	}
+
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveAtoms.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveAtoms.java
index e73b40417..ecdb9f71e 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveAtoms.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveAtoms.java
@@ -130,7 +130,7 @@ void decayIfTimeHasCome() {
 	public void newNoGoods(Collection<NoGood> newNoGoods) {
 		for (NoGood newNoGood : newNoGoods) {
 			Type type = newNoGood.getType();
-			if (type != Type.LEARNT && type != Type.INTERNAL) {
+			if (type != Type.INTERNAL) {
 				analyzeNewNoGood(newNoGood);
 				initActivity(newNoGood);
 			}
@@ -281,4 +281,16 @@ public void setMOMsStrategy(BinaryNoGoodPropagationEstimationStrategy momsStrate
 		}
 	}
 
+	/**
+	 * Reset the heap to its empty state.
+	 */
+	public void reset() {
+		incrementedActivityScores = new boolean[0];
+		activityScores = new double[0];
+		heap.clear();
+		stepsSinceLastDecay = 0;
+		currentActivityIncrement = 1.0;
+		numberOfNormalizations = 0;
+	}
+
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveChoicePoints.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveChoicePoints.java
index 17b09f1ac..9167efdc4 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveChoicePoints.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfActiveChoicePoints.java
@@ -34,7 +34,6 @@
 import java.util.HashSet;
 import java.util.Set;
 
-import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
 import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf;
 
 /**
@@ -82,9 +81,10 @@ private void recordAtomRelationships(NoGood noGood) {
 			if (body == none && choiceManager.isAtomChoice(atom)) {
 				body = atom;
 			} else {
-				if (choiceManager.isChecksEnabled() && choiceManager.isAtomChoice(atom)) {
-					throw oops("More than one choice point in a nogood: " + body + ", " + atom);
-				}
+				// TODO: reevaluate assumption because of reboots
+//				if (choiceManager.isChecksEnabled() && choiceManager.isAtomChoice(atom)) {
+//					throw oops("More than one choice point in a nogood: " + body + ", " + atom);
+//				}
 				others.add(atom);
 			}
 		}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDS.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDS.java
index 62286638c..fedac8318 100644
--- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDS.java
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDS.java
@@ -253,4 +253,10 @@ public String toString() {
 		return this.getClass().getSimpleName();
 	}
 
+	@Override
+	public void reset() {
+		heapOfActiveAtoms.reset();
+		signBalances = new int[0];
+		bufferedNoGoods.clear();
+	}
 }
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomValuePair.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomValuePair.java
new file mode 100644
index 000000000..ca9692ab4
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomValuePair.java
@@ -0,0 +1,46 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+
+public class AtomValuePair {
+	private final Atom atom;
+	private final boolean truthValue;
+
+	public AtomValuePair(Atom atom, boolean truthValue) {
+		this.atom = atom;
+		this.truthValue = truthValue;
+	}
+
+	public Atom getAtom() {
+		return atom;
+	}
+
+	public boolean isPositive() {
+		return truthValue;
+	}
+}
\ No newline at end of file
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedChoice.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedChoice.java
new file mode 100644
index 000000000..a1e28a0ca
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedChoice.java
@@ -0,0 +1,57 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+
+/**
+ * A choice independent of atom ids provided by an {@link AtomStore}.
+ * It contains an {@link Atom}, a truth value and a backtracked flag.
+ */
+public class AtomizedChoice {
+	private final Atom atom;
+	private final boolean truthValue;
+	private final boolean backtracked;
+
+	public AtomizedChoice(Atom atom, boolean truthValue, boolean backtracked) {
+		this.atom = atom;
+		this.truthValue = truthValue;
+		this.backtracked = backtracked;
+	}
+
+	public Atom getAtom() {
+		return atom;
+	}
+
+	public boolean getTruthValue() {
+		return truthValue;
+	}
+
+	public boolean isBacktracked() {
+		return backtracked;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedNoGoodCollection.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedNoGoodCollection.java
new file mode 100644
index 000000000..4a8ab80a9
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedNoGoodCollection.java
@@ -0,0 +1,85 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+
+import java.util.Collection;
+import java.util.LinkedList;
+import java.util.List;
+
+/**
+ * A collection for nogoods that allows extraction of nogoods also after changes in atom ids. This is done by
+ * converting nogoods to an atomized state based on a specific {@link AtomStore}.
+ */
+public class AtomizedNoGoodCollection {
+	private final AtomStore atomStore;
+	private final List<NoGoodAtomizer> atomizedNoGoods;
+
+	/**
+	 * Initializes the {@link AtomizedNoGoodCollection} with a specific {@link AtomStore} to use for conversions.
+	 *
+	 * @param atomStore the {@link AtomStore} to use.
+	 */
+	public AtomizedNoGoodCollection(AtomStore atomStore) {
+		this.atomStore = atomStore;
+		this.atomizedNoGoods = new LinkedList<>();
+	}
+
+	/**
+	 * Adds a nogood to the collection. The nogood is stored in an atomized way, meaning that it does not depend on
+	 * the atom ids of an {@link AtomStore}.
+	 *
+	 * @param noGood the nogood to add.
+	 */
+	public void add(NoGood noGood) {
+		atomizedNoGoods.add(new NoGoodAtomizer(noGood, atomStore));
+	}
+
+	/**
+	 * see {@link AtomizedNoGoodCollection#add(NoGood)}
+	 *
+	 * @param noGoods the nogoods to add
+	 */
+	public void addAll(Collection<NoGood> noGoods) {
+		noGoods.forEach(this::add);
+	}
+
+	/**
+	 * Gets all nogoods in the collection with atom ids based on the current {@link AtomStore}.
+	 *
+	 * @return all nogoods in the collection converted to contain atom ids based on the current {@link AtomStore}.
+	 * The list is sorted in the order the nogoods were added to the collection.
+	 */
+	public List<NoGood> getNoGoods() {
+		List<NoGood> noGoods = new LinkedList<>();
+		for (NoGoodAtomizer atomizedNoGood : atomizedNoGoods) {
+			noGoods.add(atomizedNoGood.deatomize(atomStore));
+		}
+		return noGoods;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/NoGoodAtomizer.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/NoGoodAtomizer.java
new file mode 100644
index 000000000..a8485fa34
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/NoGoodAtomizer.java
@@ -0,0 +1,83 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.Literals;
+
+/**
+ * A nogood independent of atom ids provided by an {@link AtomStore}.
+ */
+public class NoGoodAtomizer {
+	private final AtomValuePair[] literals;
+	private final Type type;
+
+	/**
+	 * Initializes a {@link NoGoodAtomizer} with the same literals as the given {@link NoGood}.
+	 * Atom ids are provided by the given {@link AtomStore}.
+	 *
+	 * @param noGood    the {@link NoGood} to get the list of literals from.
+	 * @param atomStore the {@link AtomStore} to get atom ids from.
+	 */
+	public NoGoodAtomizer(NoGood noGood, AtomStore atomStore) {
+		this.literals = new AtomValuePair[noGood.size()];
+		this.type = noGood.getType();
+		for (int i = 0; i < noGood.size(); i++) {
+			int literalId = noGood.getLiteral(i);
+			int atomId = Literals.atomOf(literalId);
+			Atom atom = atomStore.get(atomId);
+			boolean truthValue = Literals.isPositive(literalId);
+
+			this.literals[i] = new AtomValuePair(atom, truthValue);
+		}
+	}
+
+	/**
+	 * Creates a new {@link NoGood} with the same literals as this {@link NoGoodAtomizer}.
+	 * Atom ids are provided by the given {@link AtomStore}.
+	 * Atoms are added to the {@link AtomStore} if they are not contained yet.
+	 *
+	 * @param atomStore the {@link AtomStore} to get atom ids from.
+	 * @return the newly created {@link NoGood} with the same literals as this {@link NoGoodAtomizer}.
+	 */
+	public NoGood deatomize(AtomStore atomStore) {
+		int[] literals = new int[this.literals.length];
+		for (int i = 0; i < this.literals.length; i++) {
+			Atom atom = this.literals[i].getAtom();
+			atomStore.putIfAbsent(atom);
+			int atomId = atomStore.get(atom);
+			boolean truthValue = this.literals[i].isPositive();
+
+			literals[i] = Literals.atomToLiteral(atomId, truthValue);
+		}
+
+		return new NoGood(type, literals);
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/RebootManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/RebootManager.java
new file mode 100644
index 000000000..c9d7433f9
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/RebootManager.java
@@ -0,0 +1,109 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.ChoiceAtom;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.EnumerationAtom;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.Literals;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.util.Collection;
+import java.util.LinkedList;
+import java.util.List;
+
+public class RebootManager {
+	private static final Logger LOGGER = LoggerFactory.getLogger(RebootManager.class);
+
+	private final AtomStore atomStore;
+	private final AtomizedNoGoodCollection enumerationNoGoods;
+	private final AtomizedNoGoodCollection learnedNoGoods;
+	private final List<RuleAtom> discoveredRuleAtoms;
+	private int filteredCounter;
+
+	public RebootManager(AtomStore atomStore) {
+		this.atomStore = atomStore;
+		this.enumerationNoGoods = new AtomizedNoGoodCollection(atomStore);
+		this.learnedNoGoods = new AtomizedNoGoodCollection(atomStore);
+		this.discoveredRuleAtoms = new LinkedList<>();
+		this.filteredCounter = 0;
+	}
+
+	public void newEnumerationNoGood(NoGood noGood) {
+		enumerationNoGoods.add(noGood);
+		discoverRuleAtoms(noGood);
+	}
+
+	public void newLearnedNoGood(NoGood noGood) {
+		if (!scanForAtomsToFilter(noGood)) {
+			learnedNoGoods.add(noGood);
+			discoverRuleAtoms(noGood);
+		} else {
+			filteredCounter++;
+		}
+	}
+
+	public void newLearnedNoGoods(Collection<NoGood> noGoods) {
+		noGoods.forEach(this::newLearnedNoGood);
+	}
+
+	public List<NoGood> getEnumerationNoGoods() {
+		return enumerationNoGoods.getNoGoods();
+	}
+
+	public List<NoGood> getLearnedNoGoods() {
+		return learnedNoGoods.getNoGoods();
+	}
+
+	public List<RuleAtom> getDiscoveredRuleAtoms() {
+		LOGGER.debug("Number of rule atoms: " + discoveredRuleAtoms.size());
+		LOGGER.debug("Number of filtered out nogoods: " + filteredCounter);
+		return discoveredRuleAtoms;
+	}
+
+	private void discoverRuleAtoms(NoGood noGood) {
+		noGood.stream().forEach((literalId) -> {
+			Atom atom = atomStore.get(Literals.atomOf(literalId));
+			if (atom instanceof RuleAtom) {
+				discoveredRuleAtoms.add((RuleAtom) atom);
+			}
+		});
+	}
+
+	private boolean scanForAtomsToFilter(NoGood noGood) {
+		for (int literalId : noGood) {
+			Atom atom = atomStore.get(Literals.atomOf(literalId));
+			if (atom instanceof EnumerationAtom || atom instanceof ChoiceAtom) {
+				return true;
+			}
+		}
+		return false;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/AnswerSetRebootStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/AnswerSetRebootStrategy.java
new file mode 100644
index 000000000..0a4f142ba
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/AnswerSetRebootStrategy.java
@@ -0,0 +1,24 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+public class AnswerSetRebootStrategy implements RebootStrategy {
+	private boolean reboot;
+
+	public AnswerSetRebootStrategy() {
+		reboot = false;
+	}
+
+	@Override
+	public void answerSetFound() {
+		reboot = true;
+	}
+
+	@Override
+	public boolean isRebootScheduled() {
+		return reboot;
+	}
+
+	@Override
+	public void rebootPerformed() {
+		reboot = false;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/CompleteAssignmentRebootStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/CompleteAssignmentRebootStrategy.java
new file mode 100644
index 000000000..017288841
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/CompleteAssignmentRebootStrategy.java
@@ -0,0 +1,29 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+public class CompleteAssignmentRebootStrategy implements RebootStrategy {
+	private boolean reboot;
+
+	public CompleteAssignmentRebootStrategy() {
+		reboot = false;
+	}
+
+	@Override
+	public void answerSetFound() {
+		reboot = true;
+	}
+
+	@Override
+	public void backtrackJustified() {
+		reboot = true;
+	}
+
+	@Override
+	public boolean isRebootScheduled() {
+		return reboot;
+	}
+
+	@Override
+	public void rebootPerformed() {
+		reboot = false;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/FixedLearnedRebootStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/FixedLearnedRebootStrategy.java
new file mode 100644
index 000000000..6a0cc8a6a
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/FixedLearnedRebootStrategy.java
@@ -0,0 +1,33 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+
+public class FixedLearnedRebootStrategy implements RebootStrategy {
+	private final int breakpoint;
+	private int learnedCount;
+
+	public FixedLearnedRebootStrategy(int breakpoint) {
+		this.breakpoint = breakpoint;
+		this.learnedCount = 0;
+	}
+
+	@Override
+	public void newEnumerationNoGood(NoGood noGood) {
+		learnedCount++;
+	}
+
+	@Override
+	public void newLearnedNoGood(NoGood noGood) {
+		learnedCount++;
+	}
+
+	@Override
+	public boolean isRebootScheduled() {
+		return learnedCount >= breakpoint;
+	}
+
+	@Override
+	public void rebootPerformed() {
+		learnedCount = 0;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/GeometricLearnedRebootStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/GeometricLearnedRebootStrategy.java
new file mode 100644
index 000000000..c54152c34
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/GeometricLearnedRebootStrategy.java
@@ -0,0 +1,62 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+
+public class GeometricLearnedRebootStrategy implements RebootStrategy {
+	private final double base;
+	private final double scalingFactor;
+
+	private int rebootCount;
+	private int learnedCount;
+
+	public GeometricLearnedRebootStrategy(double base, double scalingFactor) {
+		this.base = base;
+		this.scalingFactor = scalingFactor;
+	}
+
+	@Override
+	public void newEnumerationNoGood(NoGood noGood) {
+		learnedCount++;
+	}
+
+	@Override
+	public void newLearnedNoGood(NoGood noGood) {
+		learnedCount++;
+	}
+
+	@Override
+	public boolean isRebootScheduled() {
+		return learnedCount >= scalingFactor * Math.pow(base, rebootCount);
+	}
+
+	@Override
+	public void rebootPerformed() {
+		rebootCount++;
+		learnedCount = 0;
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/LubyLearnedRebootStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/LubyLearnedRebootStrategy.java
new file mode 100644
index 000000000..3b5b7177c
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/LubyLearnedRebootStrategy.java
@@ -0,0 +1,72 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+
+public class LubyLearnedRebootStrategy implements RebootStrategy {
+	private final double scalingFactor;
+	private int rebootCount;
+	private int learnedCount;
+
+	public LubyLearnedRebootStrategy(double scalingFactor) {
+		this.scalingFactor = scalingFactor;
+	}
+
+	@Override
+	public void newEnumerationNoGood(NoGood noGood) {
+		learnedCount++;
+	}
+
+	@Override
+	public void newLearnedNoGood(NoGood noGood) {
+		learnedCount++;
+	}
+
+	@Override
+	public boolean isRebootScheduled() {
+		return learnedCount >= scalingFactor * luby(rebootCount + 1);
+	}
+
+	@Override
+	public void rebootPerformed() {
+		rebootCount++;
+		learnedCount = 0;
+	}
+
+	private double luby(double i) {
+		for (int k = 1; k < 31; k++) {
+			if (i == (Math.pow(2, k)) - 1) {
+				return Math.pow(2, k - 1);
+			}
+		}
+		for (int k = 1;; k++) {
+			if (Math.pow(2, k - 1) <= i && i < Math.pow(2, k) - 1) {
+				return luby(i - Math.pow(2, k - 1) + 1);
+			}
+		}
+	}
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/RebootStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/RebootStrategy.java
new file mode 100644
index 000000000..9bed67fe5
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/RebootStrategy.java
@@ -0,0 +1,71 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+
+import java.util.Collection;
+
+public interface RebootStrategy {
+	default void nextIteration() {
+	}
+
+	default void decisionMade() {
+	}
+
+	default void conflictEncountered() {
+	}
+
+	default void answerSetFound() {
+	}
+
+	default void backtrackJustified() {
+	}
+
+	default void newEnumerationNoGood(NoGood noGood) {
+	}
+
+	default void newJustificationNoGood(NoGood noGood) {
+	}
+
+	default void newNoGood(NoGood noGood) {
+	}
+
+	default void newNoGoods(Collection<NoGood> newNoGoods) {
+		newNoGoods.forEach(this::newNoGood);
+	}
+
+	default void newLearnedNoGood(NoGood noGood) {
+	}
+
+	default void newLearnedNoGoods(Collection<NoGood> newNoGoods) {
+		newNoGoods.forEach(this::newLearnedNoGood);
+	}
+
+	boolean isRebootScheduled();
+
+	void rebootPerformed();
+}
diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/RebootStrategyFactory.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/RebootStrategyFactory.java
new file mode 100644
index 000000000..140376b35
--- /dev/null
+++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/RebootStrategyFactory.java
@@ -0,0 +1,21 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
+
+public final class RebootStrategyFactory {
+	public static RebootStrategy getRebootStrategy(SystemConfig config) {
+		switch (config.getRebootStrategy()) {
+			case FIXED:
+				return new FixedLearnedRebootStrategy(config.getRebootStrategyInterval());
+			case GEOM:
+				return new GeometricLearnedRebootStrategy(config.getRebootStrategyBase(), config.getRebootStrategyFactor());
+			case LUBY:
+				return new LubyLearnedRebootStrategy(config.getRebootStrategyFactor());
+			case ASSIGN:
+				return new CompleteAssignmentRebootStrategy();
+			case ANSWER:
+				return new AnswerSetRebootStrategy();
+		}
+		throw new IllegalArgumentException("Unknown reboot strategy requested.");
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfig.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfig.java
index 73c318012..c535c8dab 100644
--- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfig.java
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfig.java
@@ -1,6 +1,7 @@
 package at.ac.tuwien.kr.alpha.core.solver;
 
 import at.ac.tuwien.kr.alpha.api.config.Heuristic;
+import at.ac.tuwien.kr.alpha.api.config.RebootStrategyEnum;
 import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
 
 public class RegressionTestConfig {
@@ -13,6 +14,13 @@ public class RegressionTestConfig {
 
 	private final Heuristic branchingHeuristic;
 
+	private final boolean rebootEnabled;
+	private final boolean disableRebootRepeat;
+	private final RebootStrategyEnum rebootStrategy;
+	private final int rebootStrategyInterval;
+	private final double rebootStrategyBase;
+	private final double rebootStrategyFactor;
+
 	private final long seed;
 
 	private final boolean debugChecks;
@@ -26,18 +34,26 @@ public class RegressionTestConfig {
 	private final boolean evaluateStratifiedPart;
 
 	private final boolean encodeAggregatesUsingSortingGrid;
-	
+
 	private final boolean supportNegativeSumElements;
 
 	public RegressionTestConfig(
-			String solverName, String grounderName, String noGoodStoreName,
-			Heuristic branchingHeuristic, long seed,
+			String solverName, String grounderName, String noGoodStoreName, Heuristic branchingHeuristic,
+			boolean rebootEnabled, boolean disableRebootRepeat, RebootStrategyEnum rebootStrategy,
+			int rebootStrategyInterval, double rebootStrategyBase, double rebootStrategyFactor, long seed,
 			boolean debugChecks, String grounderToleranceConstraints, String grounderToleranceRules,
-			boolean disableInstanceRemoval, boolean evaluateStratifiedPart, boolean useSortingGrid, boolean supportNegativeSumElements) {
+			boolean disableInstanceRemoval, boolean evaluateStratifiedPart, boolean useSortingGrid,
+			boolean supportNegativeSumElements) {
 		this.solverName = solverName;
 		this.grounderName = grounderName;
 		this.noGoodStoreName = noGoodStoreName;
 		this.branchingHeuristic = branchingHeuristic;
+		this.rebootEnabled = rebootEnabled;
+		this.disableRebootRepeat = disableRebootRepeat;
+		this.rebootStrategy = rebootStrategy;
+		this.rebootStrategyInterval = rebootStrategyInterval;
+		this.rebootStrategyBase = rebootStrategyBase;
+		this.rebootStrategyFactor = rebootStrategyFactor;
 		this.seed = seed;
 		this.debugChecks = debugChecks;
 		this.grounderToleranceConstraints = grounderToleranceConstraints;
@@ -53,6 +69,9 @@ public SystemConfig toSystemConfig() {
 		retVal.setGrounderName(this.grounderName);
 		retVal.setSolverName(this.solverName);
 		retVal.setNogoodStoreName(this.noGoodStoreName);
+		retVal.setRebootEnabled(this.rebootEnabled);
+		retVal.setRebootStrategyInterval(this.rebootStrategyInterval);
+		retVal.setDisableRebootRepeat(this.disableRebootRepeat);
 		retVal.setSeed(this.seed);
 		retVal.setBranchingHeuristic(this.branchingHeuristic);
 		retVal.setDebugInternalChecks(this.debugChecks);
@@ -81,6 +100,10 @@ public Heuristic getBranchingHeuristic() {
 		return this.branchingHeuristic;
 	}
 
+	public boolean isRebootEnabled() {
+		return rebootEnabled;
+	}
+
 	public long getSeed() {
 		return this.seed;
 	}
@@ -112,14 +135,19 @@ public boolean isEncodeAggregatesUsingSortingGrid() {
 	public boolean isSupportNegativeSumElements() {
 		return this.supportNegativeSumElements;
 	}
-	
+
 	@Override
 	public String toString() {
 		return String.format(
-				"RegressionTestConfig [solverName=%s, grounderName=%s, noGoodStoreName=%s, branchingHeuristic=%s, seed=%s, debugChecks=%s, grounderToleranceConstraints=%s, grounderToleranceRules=%s, disableInstanceRemoval=%s, evaluateStratifiedPart=%s, useSortingGrid=%s, supportNegativeSumElements=%s]",
-				this.solverName, this.grounderName, this.noGoodStoreName, this.branchingHeuristic, this.seed, this.debugChecks,
-				this.grounderToleranceConstraints, this.grounderToleranceRules, this.disableInstanceRemoval, this.evaluateStratifiedPart,
+				"RegressionTestConfig [solverName=%s, grounderName=%s, noGoodStoreName=%s, branchingHeuristic=%s,"
+						+ " rebootEnabled=%b, disableRebootRepeat=%b, rebootStrategy=%s, rebootStrategyInterval=%d,"
+						+ " rebootStrategyBase=%f, rebootStrategyFactor=%f, seed=%s, debugChecks=%s,"
+						+ " grounderToleranceConstraints=%s, grounderToleranceRules=%s, disableInstanceRemoval=%s,"
+						+ " evaluateStratifiedPart=%s, useSortingGrid=%s, supportNegativeSumElements=%s]",
+				this.solverName, this.grounderName, this.noGoodStoreName, this.branchingHeuristic, this.rebootEnabled,
+				this.disableRebootRepeat, this.rebootStrategy, this.rebootStrategyInterval, this.rebootStrategyBase,
+				this.rebootStrategyFactor, this.seed, this.debugChecks, this.grounderToleranceConstraints,
+				this.grounderToleranceRules, this.disableInstanceRemoval, this.evaluateStratifiedPart,
 				this.encodeAggregatesUsingSortingGrid, this.supportNegativeSumElements);
 	}
-
 }
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfigProvider.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfigProvider.java
index 20f139581..82ba7c2bd 100644
--- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfigProvider.java
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/RegressionTestConfigProvider.java
@@ -5,6 +5,7 @@
 import java.util.List;
 import java.util.Random;
 
+import at.ac.tuwien.kr.alpha.api.config.RebootStrategyEnum;
 import org.junit.jupiter.params.provider.Arguments;
 
 import at.ac.tuwien.kr.alpha.api.config.Heuristic;
@@ -15,6 +16,12 @@ public class RegressionTestConfigProvider {
 	private static final String DEFAULT_GROUNDER_NAME = "naive";
 	private static final String DEFAULT_ATOM_STORE = "alpharoaming";
 	private static final String DEFAULT_BRANCHING_HEURISTIC = "VSIDS";
+	private static final boolean DEFAULT_REBOOT_ENABLED = false;
+	private static final boolean DEFAULT_DISABLE_REBOOT_REPEAT = true;
+	private static final RebootStrategyEnum DEFAULT_REBOOT_STRATEGY = RebootStrategyEnum.ANSWER;
+	private static final int DEFAULT_REBOOT_STRATEGY_ITERATIONS = 5;
+	private static final double DEFAULT_REBOOT_STRATEGY_BASE = 5;
+	private static final double DEFAULT_REBOOT_STRATEGY_FACTOR = 2;
 	private static final String DEFAULT_GROUNDER_TOLERANCE = "strict";
 	private static final boolean DEFAULT_DISABLE_INSTANCE_REMOVAL = false;
 	private static final boolean DEFAULT_ENABLE_DEBUG_CHECKS = false;
@@ -24,7 +31,7 @@ public class RegressionTestConfigProvider {
 	 * "RegressionTest" annotation.
 	 * Exact number of combinations depends on the "CI" environment variable that can be used to signal that a test is being run in a CI
 	 * environment.
-	 * 
+	 *
 	 * @return
 	 */
 	private static List<RegressionTestConfig> buildConfigs() {
@@ -32,15 +39,21 @@ private static List<RegressionTestConfig> buildConfigs() {
 		boolean ci = Boolean.valueOf(System.getenv("CI"));
 
 		//@formatter:off
-		String[] solvers = ci ? new String[]{DEFAULT_SOLVER_NAME, "naive" } : new String[]{DEFAULT_SOLVER_NAME };
+		String[] solvers = ci ? new String[]{DEFAULT_SOLVER_NAME, "naive"} : new String[]{DEFAULT_SOLVER_NAME};
 		String grounder = DEFAULT_GROUNDER_NAME;
-		String[] atomStores = ci ? new String[]{DEFAULT_ATOM_STORE, "naive" } : new String[]{DEFAULT_ATOM_STORE };
-		String[] heuristics = ci ? nonDeprecatedHeuristics() : new String[]{"NAIVE", DEFAULT_BRANCHING_HEURISTIC };
-		String[] gtcValues = new String[]{DEFAULT_GROUNDER_TOLERANCE, "permissive" };
+		String[] atomStores = ci ? new String[]{DEFAULT_ATOM_STORE, "naive"} : new String[]{DEFAULT_ATOM_STORE};
+		String[] heuristics = ci ? nonDeprecatedHeuristics() : new String[]{"NAIVE", DEFAULT_BRANCHING_HEURISTIC};
+		boolean[] rebootEnabledValues = new boolean[]{DEFAULT_REBOOT_ENABLED, true};
+		RebootStrategyEnum[] rebootStrategyValues = new RebootStrategyEnum[]{DEFAULT_REBOOT_STRATEGY};
+		int[] rebootStrategyIterationsValues = new int[]{DEFAULT_REBOOT_STRATEGY_ITERATIONS};
+		double[] rebootStrategyBaseValues = new double[]{DEFAULT_REBOOT_STRATEGY_BASE};
+		double[] rebootStrategyFactorValues = new double[]{DEFAULT_REBOOT_STRATEGY_FACTOR};
+		boolean[] disableRebootRepeatValues = new boolean[]{DEFAULT_DISABLE_REBOOT_REPEAT};
+		String[] gtcValues = new String[]{DEFAULT_GROUNDER_TOLERANCE, "permissive"};
 		String gtrValue = DEFAULT_GROUNDER_TOLERANCE;
-		boolean[] disableInstanceRemovalValues = ci ? new boolean[]{DEFAULT_DISABLE_INSTANCE_REMOVAL, true } : new boolean[]{DEFAULT_DISABLE_INSTANCE_REMOVAL };
-		boolean[] evaluateStratifiedValues = new boolean[]{false, true };
-		boolean[] enableDebugChecksValues = new boolean[]{DEFAULT_ENABLE_DEBUG_CHECKS, true };
+		boolean[] disableInstanceRemovalValues = ci ? new boolean[]{DEFAULT_DISABLE_INSTANCE_REMOVAL, true} : new boolean[]{DEFAULT_DISABLE_INSTANCE_REMOVAL};
+		boolean[] evaluateStratifiedValues = new boolean[]{false, true};
+		boolean[] enableDebugChecksValues = new boolean[]{DEFAULT_ENABLE_DEBUG_CHECKS, true};
 		//@formatter:on
 
 		// NOTE:
@@ -56,14 +69,30 @@ private static List<RegressionTestConfig> buildConfigs() {
 		for (String solverName : solvers) {
 			for (String atomStoreName : atomStores) {
 				for (String branchingHeuristicName : heuristics) {
-					for (String grounderTolerance : gtcValues) {
-						for (boolean disableInstanceRemoval : disableInstanceRemovalValues) {
-							for (boolean evaluateStratified : evaluateStratifiedValues) {
-								for (boolean enableDebugChecks : enableDebugChecksValues) {
-									configsToTest.add(new RegressionTestConfig(
-											solverName, grounder, atomStoreName, Heuristic.valueOf(branchingHeuristicName),
-											seed, enableDebugChecks, grounderTolerance, gtrValue, disableInstanceRemoval, evaluateStratified,
-											true, true));
+					for (boolean rebootEnabled : rebootEnabledValues) {
+						for (boolean disableRebootRepeat : disableRebootRepeatValues) {
+							for (RebootStrategyEnum rebootStrategy : rebootStrategyValues) {
+								for (int rebootIterations : rebootStrategyIterationsValues) {
+									for (double rebootStrategyBase : rebootStrategyBaseValues) {
+										for (double rebootStrategyFactor : rebootStrategyFactorValues) {
+											for (String grounderTolerance : gtcValues) {
+												for (boolean disableInstanceRemoval : disableInstanceRemovalValues) {
+													for (boolean evaluateStratified : evaluateStratifiedValues) {
+														for (boolean enableDebugChecks : enableDebugChecksValues) {
+															configsToTest.add(new RegressionTestConfig(
+																	solverName, grounder, atomStoreName,
+																	Heuristic.valueOf(branchingHeuristicName),
+																	rebootEnabled, disableRebootRepeat, rebootStrategy,
+																	rebootIterations, rebootStrategyBase, rebootStrategyFactor,
+																	seed, enableDebugChecks, grounderTolerance, gtrValue,
+																	disableInstanceRemoval, evaluateStratified,
+																	true, true));
+														}
+													}
+												}
+											}
+										}
+									}
 								}
 							}
 						}
@@ -79,25 +108,29 @@ private static List<RegressionTestConfig> buildConfigs() {
 	 * Provides {@link RegressionTestConfig}s specifically for tests concerned with AggregateRewriting.
 	 * All parameters fixed to default values except stratified evaluation, sorting grid encoding for count rewriting
 	 * and negative sum element support.
-	 * 
+	 *
 	 * @return
 	 */
 	private static List<RegressionTestConfig> buildConfigsForAggregateTests() {
 		List<RegressionTestConfig> configsToTest = new ArrayList<>();
 
-		boolean[] evaluateStratifiedValues = new boolean[] {true, false };
-		boolean[] useSortingGridValues = new boolean[] {true, false };
-		boolean[] supportNegativeSumElementsValues = new boolean[] {true, false };
+		boolean[] evaluateStratifiedValues = new boolean[]{true, false};
+		boolean[] useSortingGridValues = new boolean[]{true, false};
+		boolean[] supportNegativeSumElementsValues = new boolean[]{true, false};
 
 		for (boolean evalStratified : evaluateStratifiedValues) {
 			for (boolean useSortingGrid : useSortingGridValues) {
 				for (boolean supportNegativeElements : supportNegativeSumElementsValues) {
 					configsToTest.add(
 							new RegressionTestConfig(
-									DEFAULT_SOLVER_NAME, DEFAULT_GROUNDER_NAME, DEFAULT_ATOM_STORE, Heuristic.valueOf(DEFAULT_BRANCHING_HEURISTIC),
-									0, DEFAULT_ENABLE_DEBUG_CHECKS, DEFAULT_GROUNDER_TOLERANCE, DEFAULT_GROUNDER_TOLERANCE, DEFAULT_DISABLE_INSTANCE_REMOVAL,
-									evalStratified,
-									useSortingGrid, supportNegativeElements));
+									DEFAULT_SOLVER_NAME, DEFAULT_GROUNDER_NAME, DEFAULT_ATOM_STORE,
+									Heuristic.valueOf(DEFAULT_BRANCHING_HEURISTIC),
+									DEFAULT_REBOOT_ENABLED, DEFAULT_DISABLE_REBOOT_REPEAT, DEFAULT_REBOOT_STRATEGY,
+									DEFAULT_REBOOT_STRATEGY_ITERATIONS, DEFAULT_REBOOT_STRATEGY_BASE,
+									DEFAULT_REBOOT_STRATEGY_FACTOR, 0, DEFAULT_ENABLE_DEBUG_CHECKS,
+									DEFAULT_GROUNDER_TOLERANCE, DEFAULT_GROUNDER_TOLERANCE,
+									DEFAULT_DISABLE_INSTANCE_REMOVAL,
+									evalStratified, useSortingGrid, supportNegativeElements));
 				}
 			}
 		}
@@ -128,6 +161,6 @@ private static final String[] nonDeprecatedHeuristics() {
 				nonDeprecatedHeuristicsNames.add(field.getName());
 			}
 		}
-		return nonDeprecatedHeuristicsNames.toArray(new String[] {});
+		return nonDeprecatedHeuristicsNames.toArray(new String[]{});
 	}
 }
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java
index 1afed713b..c102e1e13 100644
--- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverStatisticsTests.java
@@ -26,6 +26,7 @@
 package at.ac.tuwien.kr.alpha.core.solver;
 
 import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.buildSolverForRegressionTest;
+import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.ignoreTestForRebootEnabled;
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assumptions.assumeTrue;
 
@@ -58,6 +59,7 @@ public void checkStatsStringZeroChoices(RegressionTestConfig cfg) {
 
 	@RegressionTest
 	public void checkStatsStringOneChoice(RegressionTestConfig cfg) {
+		ignoreTestForRebootEnabled(cfg); // Do not run this test case with reboot enabled.
 		Solver solver = buildSolverForRegressionTest("a :- not b. b :- not a.", cfg);
 		assumeTrue(solver instanceof StatisticsReportingSolver);
 		collectAnswerSetsAndCheckStats(solver, 2, 1, 1, 1, 1, 0, 0, 0);
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java
index c0bfdd991..10020e1ce 100644
--- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java
@@ -27,11 +27,7 @@
  */
 package at.ac.tuwien.kr.alpha.core.solver;
 
-import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSet;
-import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSets;
-import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSetsWithBase;
-import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.buildSolverForRegressionTest;
-import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.collectRegressionTestAnswerSets;
+import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.*;
 import static java.util.Collections.singleton;
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertTrue;
@@ -806,12 +802,14 @@ public void smallCardinalityAggregate(RegressionTestConfig cfg) {
 
 	@RegressionTest
 	public void dummyGrounder(RegressionTestConfig cfg) {
+		ignoreTestForRebootEnabled(cfg); // Do not run this test case with reboot enabled.
 		AtomStore atomStore = new AtomStoreImpl();
 		assertEquals(DummyGrounder.EXPECTED, buildSolverForRegressionTest(atomStore, new DummyGrounder(atomStore), cfg).collectSet());
 	}
 
 	@RegressionTest
 	public void choiceGrounder(RegressionTestConfig cfg) {
+		ignoreTestForRebootEnabled(cfg); // Do not run this test case with reboot enabled.
 		AtomStore atomStore = new AtomStoreImpl();
 		assertEquals(ChoiceGrounder.EXPECTED, buildSolverForRegressionTest(atomStore, new ChoiceGrounder(atomStore), cfg).collectSet());
 	}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomGeneratorForTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomGeneratorForTests.java
new file mode 100644
index 000000000..cda5097ec
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomGeneratorForTests.java
@@ -0,0 +1,115 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import at.ac.tuwien.kr.alpha.api.programs.Predicate;
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.api.programs.terms.Term;
+import at.ac.tuwien.kr.alpha.commons.Predicates;
+import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
+import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.Literals;
+
+import java.util.List;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+
+/**
+ * Provides utility methods to generate atoms and register them at an {@link AtomStore}.
+ */
+public class AtomGeneratorForTests {
+	/**
+	 * Maps a given list of literals to literal ids based on a given {@link AtomStore}.
+	 *
+	 * @param literals  the list of literals where each literal is represented by a pair of atom and truth value.
+	 * @param atomStore the {@link AtomStore} to use for converting atom ids.
+	 * @return the list of ids for the given literals based on the current {@link AtomStore}.
+	 */
+	public static int[] getLiteralIds(List<AtomValuePair> literals, AtomStore atomStore) {
+		int[] literalIds = new int[literals.size()];
+
+		int position = 0;
+		for (AtomValuePair literal : literals) {
+			literalIds[position] = Literals.atomToLiteral(atomStore.get(literal.getAtom()), literal.isPositive());
+			position++;
+		}
+
+		return literalIds;
+	}
+
+	/**
+	 * Generates a given number of new filler atoms and registers them at the current {@link AtomStore}.
+	 *
+	 * @param count     the number of filler atoms to generate and register.
+	 * @param atomStore the {@link AtomStore} to use for converting atom ids.
+	 */
+	public static void generateAndRegisterFillerAtoms(int count, AtomStore atomStore) {
+		generateAndRegisterFillerAtoms(count, 0, atomStore);
+	}
+
+	/**
+	 * Generates a given number of new filler atoms and registers them at the current {@link AtomStore}.
+	 * Filler atoms are generated under the assumption that a given number of filler atoms were already generated.
+	 *
+	 * @param count     the number of filler atoms to generate and register.
+	 * @param existing  the number of filler atoms already generated before.
+	 * @param atomStore the {@link AtomStore} to use for converting atom ids.
+	 */
+	public static void generateAndRegisterFillerAtoms(int count, int existing, AtomStore atomStore) {
+		for (int i = existing; i < existing + count; i++) {
+			generateAndRegisterAtom(String.format("_FILL%d_", i), 0, atomStore);
+		}
+	}
+
+	/**
+	 * Generates a new {@link Atom} with a given predicate symbol and arity.
+	 * The generated {@link Atom} is then registered at the current {@link AtomStore}.
+	 * Constant terms starting from 1 up to the arity are used.
+	 *
+	 * @param symbol    the predicate symbol of the {@link Atom} to generate.
+	 * @param arity     the arity of the atom to generate.
+	 * @param atomStore the {@link AtomStore} to use for converting atom ids.
+	 * @return the generated {@link Atom}.
+	 */
+	public static Atom generateAndRegisterAtom(String symbol, int arity, AtomStore atomStore) {
+		Predicate predicate = Predicates.getPredicate(symbol, arity);
+
+		Atom atom;
+		if (arity == 0) {
+			atom = Atoms.newBasicAtom(predicate);
+		} else {
+			List<Term> terms = IntStream.iterate(1, x -> x + 1).limit(arity)
+					.mapToObj(Integer::toString)
+					.map(Terms::newConstant)
+					.collect(Collectors.toList());
+			atom = Atoms.newBasicAtom(predicate, terms);
+		}
+
+		atomStore.putIfAbsent(atom);
+		return atom;
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedNoGoodCollectionTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedNoGoodCollectionTest.java
new file mode 100644
index 000000000..f8e06a1a6
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/AtomizedNoGoodCollectionTest.java
@@ -0,0 +1,255 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl;
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.Literals;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+
+/**
+ * Provides test cases for creating nogoods and checking correctness
+ * of the atom id translation performed by a {@link AtomizedNoGoodCollection}.
+ */
+class AtomizedNoGoodCollectionTest {
+	AtomStore atomStore;
+	AtomGeneratorForTests atomGenerator;
+
+	public AtomizedNoGoodCollectionTest() {
+		atomStore = new AtomStoreImpl();
+		atomGenerator = new AtomGeneratorForTests();
+	}
+
+	@BeforeEach
+	public void setUp() {
+		atomStore = new AtomStoreImpl();
+		atomGenerator = new AtomGeneratorForTests();
+	}
+
+
+	/**
+	 * Creates a nogood with a single literal
+	 * and tests conversion correctness after change in the single atom id.
+	 */
+	@Test
+	void testOneSingleLiteralNoGood() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(1, atomStore);
+		List<AtomValuePair> literals = Collections.singletonList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST_", 0, atomStore), true)
+		);
+		int[] literalIds = AtomGeneratorForTests.getLiteralIds(literals, atomStore);
+		NoGood noGood = new NoGood(literalIds);
+
+		AtomizedNoGoodCollection atomizedCollection = new AtomizedNoGoodCollection(atomStore);
+		atomizedCollection.add(noGood);
+
+		atomStore.reset();
+		atomStore.putIfAbsent(literals.get(0).getAtom());
+		extractAndCheckNoGoods(Collections.singletonList(literals), atomizedCollection, atomStore);
+	}
+
+	/**
+	 * Creates two nogoods with a single literal
+	 * and tests conversion correctness after change in an atom id of one of them.
+	 */
+	@Test
+	void testTwoSingleLiteralNoGoodsChangeIdForOne() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		List<AtomValuePair> noGood1 = Collections.singletonList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST1_", 0, atomStore), false)
+		);
+		List<AtomValuePair> noGood2 = Collections.singletonList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST2_", 2, atomStore), true)
+		);
+
+		AtomizedNoGoodCollection atomizedCollection = new AtomizedNoGoodCollection(atomStore);
+		List<List<AtomValuePair>> noGoods = Arrays.asList(noGood1, noGood2);
+		addAtomizedNoGoods(atomizedCollection, noGoods, atomStore);
+
+		atomStore.reset();
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		atomStore.putIfAbsent(noGood1.get(0).getAtom());
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, 2, atomStore);
+		atomStore.putIfAbsent(noGood2.get(0).getAtom());
+		extractAndCheckNoGoods(noGoods, atomizedCollection, atomStore);
+	}
+
+
+	/**
+	 * Creates a nogood with multiple literals
+	 * and tests conversion correctness after change in all atom ids.
+	 */
+	@Test
+	void testOneMultiLiteralNoGoodChangeAllIds() {
+
+	}
+
+	/**
+	 * Creates a nogood with multiple literals
+	 * and tests conversion correctness after change in a single atom id.
+	 */
+	@Test
+	void testOneMultiLiteralNoGoodChangeSingleId() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(1, atomStore);
+		List<AtomValuePair> noGood = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST1_", 0, atomStore), true),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST2_", 2, atomStore), false)
+		);
+
+		AtomizedNoGoodCollection atomizedCollection = new AtomizedNoGoodCollection(atomStore);
+		List<List<AtomValuePair>> noGoods = Collections.singletonList(noGood);
+		addAtomizedNoGoods(atomizedCollection, noGoods, atomStore);
+
+		atomStore.reset();
+		atomStore.putIfAbsent(noGood.get(0).getAtom());
+		atomStore.putIfAbsent(noGood.get(1).getAtom());
+		extractAndCheckNoGoods(noGoods, atomizedCollection, atomStore);
+	}
+
+	/**
+	 * Creates two nogoods with multiple literals
+	 * and tests conversion correctness after change in a single atom id.
+	 */
+	@Test
+	void testTwoMultiLiteralNoGoodsChangeSingleId() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		List<AtomValuePair> noGood1 = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST1_", 0, atomStore), false),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST2_", 0, atomStore), false)
+		);
+		List<AtomValuePair> noGood2 = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST3_", 2, atomStore), true),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST4_", 1, atomStore), false)
+		);
+
+		AtomizedNoGoodCollection atomizedCollection = new AtomizedNoGoodCollection(atomStore);
+		List<List<AtomValuePair>> noGoods = Arrays.asList(noGood1, noGood2);
+		addAtomizedNoGoods(atomizedCollection, noGoods, atomStore);
+
+		atomStore.reset();
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		atomStore.putIfAbsent(noGood1.get(0).getAtom());
+		atomStore.putIfAbsent(noGood1.get(1).getAtom());
+		atomStore.putIfAbsent(noGood2.get(0).getAtom());
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, 2, atomStore);
+		atomStore.putIfAbsent(noGood2.get(1).getAtom());
+		extractAndCheckNoGoods(noGoods, atomizedCollection, atomStore);
+	}
+
+	/**
+	 * Creates two nogoods with multiple literals
+	 * and tests conversion correctness after change in all atom ids.
+	 */
+	@Test
+	void testTwoMultiLiteralNoGoodsChangeAllIds() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		List<AtomValuePair> noGood1 = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST1_", 0, atomStore), false),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST2_", 0, atomStore), true)
+		);
+		List<AtomValuePair> noGood2 = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST3_", 2, atomStore), true),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST4_", 1, atomStore), true)
+		);
+
+		AtomizedNoGoodCollection atomizedCollection = new AtomizedNoGoodCollection(atomStore);
+		List<List<AtomValuePair>> noGoods = Arrays.asList(noGood1, noGood2);
+		addAtomizedNoGoods(atomizedCollection, noGoods, atomStore);
+
+		atomStore.reset();
+		atomStore.putIfAbsent(noGood1.get(0).getAtom());
+		atomStore.putIfAbsent(noGood1.get(1).getAtom());
+		atomStore.putIfAbsent(noGood2.get(0).getAtom());
+		atomStore.putIfAbsent(noGood2.get(1).getAtom());
+		extractAndCheckNoGoods(noGoods, atomizedCollection, atomStore);
+	}
+
+	/**
+	 * Extracts the {@link NoGood}s from a given {@link AtomizedNoGoodCollection} and asserts that the literals
+	 * in these {@link NoGood}s are the same as the literals in the given literal lists.
+	 *
+	 * @param noGoods            the lists of literals where each nogood is represented by a list that contains pairs
+	 *                           of atom and truth value.
+	 * @param atomizedCollection the {@link AtomizedNoGoodCollection} to extract the {@link NoGood}s from.
+	 */
+	private void extractAndCheckNoGoods(List<List<AtomValuePair>> noGoods, AtomizedNoGoodCollection atomizedCollection,
+										AtomStore atomStore) {
+		List<NoGood> noGoodsExtracted = atomizedCollection.getNoGoods();
+		assertEquals(noGoods.size(), noGoodsExtracted.size());
+
+		for (int i = 0; i < noGoods.size(); i++) {
+			List<AtomValuePair> literals = noGoods.get(i);
+			NoGood noGoodExtracted = noGoodsExtracted.get(i);
+			checkNoGood(literals, noGoodExtracted, atomStore);
+		}
+	}
+
+	/**
+	 * Asserts that the literals in the given {@link NoGood} are the same as the given literals.
+	 *
+	 * @param literals the literals to compare to represented as pairs of atom and truth value.
+	 * @param noGood   the given {@link NoGood} to check the literals of.
+	 */
+	private void checkNoGood(List<AtomValuePair> literals, NoGood noGood, AtomStore atomStore) {
+		assertEquals(literals.size(), noGood.size());
+
+		for (int i = 0; i < literals.size(); i++) {
+			AtomValuePair literal = literals.get(i);
+			int literalExtractedId = noGood.getLiteral(i);
+
+			Atom atomExtracted = atomStore.get(Literals.atomOf(literalExtractedId));
+			assertEquals(literal.getAtom(), atomExtracted);
+
+			boolean truthValueExtracted = Literals.isPositive(literalExtractedId);
+			assertEquals(literal.isPositive(), truthValueExtracted);
+		}
+	}
+
+	/**
+	 * Adds the given nogoods to the given {@link AtomizedNoGoodCollection}.
+	 *
+	 * @param atomizedCollection the {@link AtomizedNoGoodCollection} to add to.
+	 * @param noGoods            the nogoods to add to the collection. Each nogood is represented by a list that contains pairs
+	 *                           of atom and truth value.
+	 */
+	private void addAtomizedNoGoods(AtomizedNoGoodCollection atomizedCollection,
+									List<List<AtomValuePair>> noGoods, AtomStore atomStore) {
+		for (List<AtomValuePair> literals : noGoods) {
+			int[] literalIds = AtomGeneratorForTests.getLiteralIds(literals, atomStore);
+			NoGood noGood = new NoGood(literalIds);
+			atomizedCollection.add(noGood);
+		}
+	}
+}
\ No newline at end of file
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/GroundExplosionTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/GroundExplosionTest.java
new file mode 100644
index 000000000..b59dec501
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/GroundExplosionTest.java
@@ -0,0 +1,56 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot;
+
+import at.ac.tuwien.kr.alpha.core.solver.RegressionTest;
+import at.ac.tuwien.kr.alpha.core.solver.RegressionTestConfig;
+
+import java.util.stream.IntStream;
+
+import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSets;
+
+public class GroundExplosionTest {
+	@RegressionTest
+	public void testGroundExplosion_1(RegressionTestConfig cfg) {
+		String domainStr = getDomainString(1);
+		assertRegressionTestAnswerSets(cfg,
+				getProgramString(1),
+				domainStr,
+				"sel(1), p(1,1,1,1,1,1), " + domainStr);
+	}
+
+	@RegressionTest
+	public void testGroundExplosion_5(RegressionTestConfig cfg) {
+		String domainStr = getDomainString(5);
+		assertRegressionTestAnswerSets(cfg,
+				getProgramString(5),
+				domainStr,
+				"sel(1), p(1,1,1,1,1,1), " + domainStr,
+				"sel(2), p(2,2,2,2,2,2), " + domainStr,
+				"sel(3), p(3,3,3,3,3,3), " + domainStr,
+				"sel(4), p(4,4,4,4,4,4), " + domainStr,
+				"sel(5), p(5,5,5,5,5,5), " + domainStr);
+	}
+
+	/**
+	 * Constructs a ground explosion program string with the given domain size.
+	 *
+	 * @param n the size of the encoded domain.
+	 */
+	private String getProgramString(int n) {
+		return "{ sel(X) } :- dom(X)." +
+				":- sel(X), sel(Y), X != Y." +
+				"p(X1,X2,X3,X4,X5,X6) :- sel(X1), sel(X2), sel(X3), sel(X4), sel(X5), sel(X6)." +
+				String.format("dom(1..%d).", n);
+	}
+
+	/**
+	 * Constructs a string of atoms representing a domain of the given size.
+	 *
+	 * @param n the size of the encoded domain.
+	 */
+	private String getDomainString(int n) {
+		return IntStream.range(1, n + 1)
+				.mapToObj(x -> String.format("dom(%d)", x))
+				.reduce((x, y) -> String.format("%s, %s", x, y))
+				.orElse("");
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/NoGoodAtomizerTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/NoGoodAtomizerTest.java
new file mode 100644
index 000000000..ce9418060
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/NoGoodAtomizerTest.java
@@ -0,0 +1,184 @@
+/**
+ * Copyright (c) 2022, the Alpha Team.
+ * All rights reserved.
+ * <p>
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * <p>
+ * 1) Redistributions of source code must retain the above copyright notice, this
+ * list of conditions and the following disclaimer.
+ * <p>
+ * 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.
+ * <p>
+ * 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.core.solver.reboot;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
+import at.ac.tuwien.kr.alpha.core.common.AtomStore;
+import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl;
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import at.ac.tuwien.kr.alpha.core.programs.atoms.Literals;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+
+/**
+ * Provides test cases for creating nogoods and checking correctness
+ * of the atom id translation performed by a {@link NoGoodAtomizer}.
+ */
+class NoGoodAtomizerTest {
+	AtomStore atomStore;
+
+	public NoGoodAtomizerTest() {
+		atomStore = new AtomStoreImpl();
+	}
+
+	@BeforeEach
+	public void setUp() {
+		atomStore = new AtomStoreImpl();
+	}
+
+	/**
+	 * Registers multiple atoms at the {@link AtomStore} and resets the {@link AtomStore}.
+	 * Then registers the same atoms in the same order again and checks whether all of them receive
+	 * the same id as before.
+	 */
+	@Test
+	void testSameAtomIdsAfterAtomStoreReset() {
+		int atomCount = 6;
+
+		List<Atom> atoms = new ArrayList<>();
+		List<Integer> atomIds = new ArrayList<>();
+		for (int i = 0; i < atomCount; i++) {
+			Atom atom = AtomGeneratorForTests.generateAndRegisterAtom(String.format("_TEST%d_", i), 0, atomStore);
+			atoms.add(atom);
+			atomIds.add(atomStore.get(atom));
+		}
+
+		atomStore.reset();
+		for (int i = 0; i < atomCount; i++) {
+			Atom atom = atoms.get(i);
+			atomStore.putIfAbsent(atom);
+			assertEquals(atomIds.get(i), atomStore.get(atom));
+		}
+	}
+
+	/**
+	 * Creates a nogood with a single literal
+	 * and tests conversion correctness after change in atom id.
+	 */
+	@Test
+	void testSingleLiteralNoGood() {
+		List<AtomValuePair> literals = Collections.singletonList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST_", 0, atomStore), false)
+		);
+		int[] literalIds = AtomGeneratorForTests.getLiteralIds(literals, atomStore);
+		NoGoodAtomizer noGoodAtomizer = new NoGoodAtomizer(new NoGood(literalIds), atomStore);
+
+		atomStore.reset();
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(1, atomStore);
+		atomStore.putIfAbsent(literals.get(0).getAtom());
+		extractAndCheckLiterals(literals, noGoodAtomizer);
+	}
+
+	/**
+	 * Creates a nogood with a single literal of arity > 0
+	 * and tests conversion correctness after change in atom id.
+	 */
+	@Test
+	void testSingleTwoTermLiteralNoGood() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(1, atomStore);
+		List<AtomValuePair> literals = Collections.singletonList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST_", 2, atomStore), true)
+		);
+		int[] literalIds = AtomGeneratorForTests.getLiteralIds(literals, atomStore);
+		NoGoodAtomizer noGoodAtomizer = new NoGoodAtomizer(new NoGood(literalIds), atomStore);
+
+		atomStore.reset();
+		atomStore.putIfAbsent(literals.get(0).getAtom());
+		extractAndCheckLiterals(literals, noGoodAtomizer);
+	}
+
+	/**
+	 * Creates a nogood with multiple literals
+	 * and tests conversion correctness after change in a single atom id.
+	 */
+	@Test
+	void testMultiLiteralNoGoodChangeSingleId() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		List<AtomValuePair> literals = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST2_", 0, atomStore), false),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST1_", 0, atomStore), true)
+		);
+		int[] literalIds = AtomGeneratorForTests.getLiteralIds(literals, atomStore);
+		NoGoodAtomizer noGoodAtomizer = new NoGoodAtomizer(new NoGood(literalIds), atomStore);
+
+		atomStore.reset();
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		atomStore.putIfAbsent(literals.get(0).getAtom());
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, 2, atomStore);
+		atomStore.putIfAbsent(literals.get(1).getAtom());
+		extractAndCheckLiterals(literals, noGoodAtomizer);
+	}
+
+	/**
+	 * Creates a nogood with multiple literals
+	 * and tests conversion correctness after change in all atom ids.
+	 */
+	@Test
+	void testMultiLiteralNoGoodChangeAllIds() {
+		AtomGeneratorForTests.generateAndRegisterFillerAtoms(2, atomStore);
+		List<AtomValuePair> literals = Arrays.asList(
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST1_", 0, atomStore), true),
+				new AtomValuePair(AtomGeneratorForTests.generateAndRegisterAtom("_TEST2_", 0, atomStore), false)
+		);
+		int[] literalIds = AtomGeneratorForTests.getLiteralIds(literals, atomStore);
+		NoGoodAtomizer noGoodAtomizer = new NoGoodAtomizer(new NoGood(literalIds), atomStore);
+
+		atomStore.reset();
+		atomStore.putIfAbsent(literals.get(0).getAtom());
+		atomStore.putIfAbsent(literals.get(1).getAtom());
+		extractAndCheckLiterals(literals, noGoodAtomizer);
+	}
+
+	/**
+	 * Extracts the {@link NoGood} from a given {@link NoGoodAtomizer} and asserts that the literals in this
+	 * {@link NoGood} are the same as the given literals.
+	 *
+	 * @param literals       a list of literals where each literal is represented by a pair of atom and truth value.
+	 * @param noGoodAtomizer the {@link NoGoodAtomizer} to extract the {@link NoGood} from.
+	 */
+	private void extractAndCheckLiterals(List<AtomValuePair> literals, NoGoodAtomizer noGoodAtomizer) {
+		NoGood noGood = noGoodAtomizer.deatomize(atomStore);
+		assertEquals(literals.size(), noGood.size());
+
+		for (int i = 0; i < literals.size(); i++) {
+			AtomValuePair literal = literals.get(i);
+			int literalExtractedId = noGood.getLiteral(i);
+
+			Atom atomExtracted = atomStore.get(Literals.atomOf(literalExtractedId));
+			assertEquals(literal.getAtom(), atomExtracted);
+
+			boolean truthValueExtracted = Literals.isPositive(literalExtractedId);
+			assertEquals(literal.isPositive(), truthValueExtracted);
+		}
+	}
+}
\ No newline at end of file
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/AnswerSetRebootStrategyTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/AnswerSetRebootStrategyTest.java
new file mode 100644
index 000000000..1402b762a
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/AnswerSetRebootStrategyTest.java
@@ -0,0 +1,67 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+public class AnswerSetRebootStrategyTest {
+	@Test
+	public void testStrategySchedulesAfterAnswerSet() {
+		RebootStrategy strategy = new AnswerSetRebootStrategy();
+		strategy.answerSetFound();
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyResetsAfterReboot() {
+		RebootStrategy strategy = new AnswerSetRebootStrategy();
+		strategy.answerSetFound();
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleImmediately() {
+		RebootStrategy strategy = new AnswerSetRebootStrategy();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterIteration() {
+		RebootStrategy strategy = new AnswerSetRebootStrategy();
+		strategy.nextIteration();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterUnrelatedEvents() {
+		RebootStrategy strategy = new AnswerSetRebootStrategy();
+
+		strategy.nextIteration();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.decisionMade();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.conflictEncountered();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.backtrackJustified();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newEnumerationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newJustificationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/CompleteAssignmentRebootStrategyTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/CompleteAssignmentRebootStrategyTest.java
new file mode 100644
index 000000000..34a34aa77
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/CompleteAssignmentRebootStrategyTest.java
@@ -0,0 +1,64 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+public class CompleteAssignmentRebootStrategyTest {
+	@Test
+	public void testStrategySchedulesAfterAnswerSet() {
+		RebootStrategy strategy = new CompleteAssignmentRebootStrategy();
+		strategy.answerSetFound();
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterJustification() {
+		RebootStrategy strategy = new CompleteAssignmentRebootStrategy();
+		strategy.backtrackJustified();
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyResetsAfterReboot() {
+		RebootStrategy strategy = new CompleteAssignmentRebootStrategy();
+		strategy.answerSetFound();
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNoScheduleImmediately() {
+		RebootStrategy strategy = new CompleteAssignmentRebootStrategy();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterUnrelatedEvents() {
+		RebootStrategy strategy = new CompleteAssignmentRebootStrategy();
+
+		strategy.nextIteration();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.decisionMade();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.conflictEncountered();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newEnumerationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.newJustificationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/FixedLearnedRebootStrategyTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/FixedLearnedRebootStrategyTest.java
new file mode 100644
index 000000000..d5e6af777
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/FixedLearnedRebootStrategyTest.java
@@ -0,0 +1,117 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import org.junit.jupiter.api.Test;
+
+import java.util.Collection;
+import java.util.List;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+public class FixedLearnedRebootStrategyTest {
+	@Test
+	public void testStrategySchedulesAfterLearnedNogoods() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newLearnedNoGood(new NoGood());
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterEnumerationNogoods() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newEnumerationNoGood(new NoGood());
+		strategy.newEnumerationNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterMixedNogoods() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newLearnedNoGood(new NoGood());
+		strategy.newEnumerationNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterNogoodBundle() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		Collection<NoGood> noGoods = List.of(new NoGood(), new NoGood());
+		strategy.newLearnedNoGoods(noGoods);
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyResetsAfterReboot() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(1);
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleImmediately() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterSmallerBundle() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(3);
+		Collection<NoGood> noGoods = List.of(new NoGood(), new NoGood());
+		strategy.newLearnedNoGoods(noGoods);
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterSingleEnumerationNogood() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newEnumerationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterStaticNogoods() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newNoGood(new NoGood());
+		strategy.newNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterStaticNogoodBundle() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newNoGoods(List.of(new NoGood(), new NoGood()));
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterJustificationNogoods() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(2);
+		strategy.newJustificationNoGood(new NoGood());
+		strategy.newJustificationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterUnrelatedEvents() {
+		RebootStrategy strategy = new FixedLearnedRebootStrategy(1);
+
+		strategy.nextIteration();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.decisionMade();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.conflictEncountered();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.backtrackJustified();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.answerSetFound();
+		assertFalse(strategy.isRebootScheduled());
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/GeometricLearnedRebootStrategyTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/GeometricLearnedRebootStrategyTest.java
new file mode 100644
index 000000000..c04ad257c
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/GeometricLearnedRebootStrategyTest.java
@@ -0,0 +1,133 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import org.junit.jupiter.api.Test;
+
+import java.util.Collection;
+import java.util.List;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+public class GeometricLearnedRebootStrategyTest {
+	@Test
+	public void testStrategySchedulesAfterLearnedNogoods() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newLearnedNoGood(new NoGood());
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterEnumerationNogoods() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newEnumerationNoGood(new NoGood());
+		strategy.newEnumerationNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterMixedNogoods() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newLearnedNoGood(new NoGood());
+		strategy.newEnumerationNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesFirstThreeCorrectly() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 1);
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyResetsAfterReboot() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 1);
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleImmediately() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterSmallerBundle() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 3);
+		Collection<NoGood> noGoods = List.of(new NoGood(), new NoGood());
+		strategy.newLearnedNoGoods(noGoods);
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterSingleEnumerationNogood() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newEnumerationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterStaticNogoods() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newNoGood(new NoGood());
+		strategy.newNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterStaticNogoodBundle() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newNoGoods(List.of(new NoGood(), new NoGood()));
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterJustificationNogoods() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 2);
+		strategy.newJustificationNoGood(new NoGood());
+		strategy.newJustificationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterUnrelatedEvents() {
+		RebootStrategy strategy = new GeometricLearnedRebootStrategy(2, 1);
+
+		strategy.nextIteration();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.decisionMade();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.conflictEncountered();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.backtrackJustified();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.answerSetFound();
+		assertFalse(strategy.isRebootScheduled());
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/LubyLearnedRebootStrategyTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/LubyLearnedRebootStrategyTest.java
new file mode 100644
index 000000000..1eff7c596
--- /dev/null
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/reboot/strategies/LubyLearnedRebootStrategyTest.java
@@ -0,0 +1,131 @@
+package at.ac.tuwien.kr.alpha.core.solver.reboot.strategies;
+
+import at.ac.tuwien.kr.alpha.core.common.NoGood;
+import org.junit.jupiter.api.Test;
+
+import java.util.Collection;
+import java.util.List;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+public class LubyLearnedRebootStrategyTest {
+	@Test
+	public void testStrategySchedulesAfterLearnedNogoods() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newLearnedNoGood(new NoGood());
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterEnumerationNogoods() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newEnumerationNoGood(new NoGood());
+		strategy.newEnumerationNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesAfterMixedNogoods() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newLearnedNoGood(new NoGood());
+		strategy.newEnumerationNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategySchedulesFirstFourCorrectly() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(1);
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyResetsAfterReboot() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(1);
+		strategy.newLearnedNoGood(new NoGood());
+		assertTrue(strategy.isRebootScheduled());
+		strategy.rebootPerformed();
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleImmediately() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(1);
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterSmallerBundle() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(3);
+		Collection<NoGood> noGoods = List.of(new NoGood(), new NoGood());
+		strategy.newLearnedNoGoods(noGoods);
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterSingleEnumerationNogood() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newEnumerationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterStaticNogoods() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newNoGood(new NoGood());
+		strategy.newNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterStaticNogoodBundle() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newNoGoods(List.of(new NoGood(), new NoGood()));
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterJustificationNogoods() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(2);
+		strategy.newJustificationNoGood(new NoGood());
+		strategy.newJustificationNoGood(new NoGood());
+		assertFalse(strategy.isRebootScheduled());
+	}
+
+	@Test
+	public void testStrategyDoesNotScheduleAfterUnrelatedEvents() {
+		RebootStrategy strategy = new LubyLearnedRebootStrategy(1);
+
+		strategy.nextIteration();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.decisionMade();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.conflictEncountered();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.backtrackJustified();
+		assertFalse(strategy.isRebootScheduled());
+
+		strategy.answerSetFound();
+		assertFalse(strategy.isRebootScheduled());
+	}
+}
diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java
index bd0c358c1..2bf50698c 100644
--- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java
+++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java
@@ -54,7 +54,7 @@ public static void fillAtomStore(AtomStore atomStore, int numberOfAtomsToFill) {
 			atomStore.putIfAbsent(Atoms.newBasicAtom(predA, Terms.newConstant(i)));
 		}
 	}
-	
+
 	public static Atom atom(String predicateName, String... termStrings) {
 		Term[] terms = new Term[termStrings.length];
 		for (int i = 0; i < termStrings.length; i++) {
@@ -75,11 +75,11 @@ public static Atom atom(String predicateName, int... termInts) {
 		}
 		return Atoms.newBasicAtom(Predicates.getPredicate(predicateName, terms.length), terms);
 	}
-	
+
 	public static void printNoGoods(AtomStore atomStore, Collection<NoGood> noGoods) {
 		System.out.println(noGoods.stream().map(atomStore::noGoodToString).collect(Collectors.toSet()));
 	}
-	
+
 	public static void assertAnswerSetsEqual(Set<AnswerSet> expected, Set<AnswerSet> actual) {
 		if (expected == null) {
 			if (actual != null) {
@@ -161,15 +161,15 @@ private static Solver buildSolverFromSystemConfig(ASPCore2Program prog, SystemCo
 				: InternalProgram.fromNormalProgram(normalProg);
 		return SolverFactory.getInstance(cfg, atomStore, GrounderFactory.getInstance(cfg.getGrounderName(), preprocessed, atomStore, cfg.isDebugInternalChecks()));
 	}
-	
+
 	public static Solver buildSolverForRegressionTest(ASPCore2Program prog, RegressionTestConfig cfg) {
 		return buildSolverFromSystemConfig(prog, cfg.toSystemConfig());
 	}
-	
+
 	public static Solver buildSolverForRegressionTest(String prog, RegressionTestConfig cfg) {
 		return buildSolverFromSystemConfig(new ProgramParserImpl().parse(prog), cfg.toSystemConfig());
 	}
-	
+
 	public static Solver buildSolverForRegressionTest(AtomStore atomStore, Grounder grounder, RegressionTestConfig cfg) {
 		SystemConfig systemCfg = cfg.toSystemConfig();
 		return SolverFactory.getInstance(systemCfg, atomStore, grounder);
@@ -178,7 +178,7 @@ public static Solver buildSolverForRegressionTest(AtomStore atomStore, Grounder
 	public static Set<AnswerSet> collectRegressionTestAnswerSets(ASPCore2Program prog, RegressionTestConfig cfg) {
 		return buildSolverForRegressionTest(prog, cfg).collectSet();
 	}
-	
+
 	public static Set<AnswerSet> collectRegressionTestAnswerSets(String aspstr, RegressionTestConfig cfg) {
 		ASPCore2Program prog = new ProgramParserImpl().parse(aspstr);
 		return collectRegressionTestAnswerSets(prog, cfg);
@@ -188,32 +188,35 @@ public static void assertRegressionTestAnswerSet(RegressionTestConfig cfg, Strin
 		Set<AnswerSet> actualAnswerSets = collectRegressionTestAnswerSets(program, cfg);
 		TestUtils.assertAnswerSetsEqual(answerSet, actualAnswerSets);
 	}
-	
+
 	public static void assertRegressionTestAnswerSets(RegressionTestConfig cfg, String program, String... answerSets) {
 		Set<AnswerSet> actualAnswerSets = collectRegressionTestAnswerSets(program, cfg);
-		TestUtils.assertAnswerSetsEqual(answerSets, actualAnswerSets);		
+		TestUtils.assertAnswerSetsEqual(answerSets, actualAnswerSets);
 	}
-	
+
 	public static void assertRegressionTestAnswerSetsWithBase(RegressionTestConfig cfg, String program, String base, String... answerSets) {
 		Set<AnswerSet> actualAnswerSets = collectRegressionTestAnswerSets(program, cfg);
-		TestUtils.assertAnswerSetsEqualWithBase(base, answerSets, actualAnswerSets);		
+		TestUtils.assertAnswerSetsEqualWithBase(base, answerSets, actualAnswerSets);
 	}
-	
+
 	public static void runWithTimeout(RegressionTestConfig cfg, long baseTimeout, long timeoutFactor, Executable action) {
 		long timeout = cfg.isDebugChecks() ? timeoutFactor * baseTimeout : baseTimeout;
 		assertTimeoutPreemptively(Duration.ofMillis(timeout), action);
 	}
-	
+
 	public static void ignoreTestForNaiveSolver(RegressionTestConfig cfg) {
 		Assumptions.assumeFalse(cfg.getSolverName().equals("naive"));
 	}
-	
+
 	public static void ignoreTestForNonDefaultDomainIndependentHeuristics(RegressionTestConfig cfg) {
 		Assumptions.assumeTrue(cfg.getBranchingHeuristic() == Heuristic.VSIDS);
 	}
-	
+
 	public static void ignoreTestForSimplifiedSumAggregates(RegressionTestConfig cfg) {
 		Assumptions.assumeTrue(cfg.isSupportNegativeSumElements());
 	}
 
+	public static void ignoreTestForRebootEnabled(RegressionTestConfig cfg) {
+		Assumptions.assumeFalse(cfg.isRebootEnabled());
+	}
 }