Grounder restart

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(", "));
+	}
+}

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;
 	}

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);

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();
 }

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();
+	}
 }

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: ");

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
 	 */