Phase saving, restarts, and heuristic performance logs

alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/Heuristic.java

@@ -41,7 +41,8 @@ public enum Heuristic {
 	@Deprecated
 	ALPHA_HEAD_MBT,
 	VSIDS,
-	GDD_VSIDS;
+	GDD_VSIDS,
+	VSIDS_PHASE_SAVING;
 
 	/**
 	 * @return a comma-separated list of names of known heuristics

alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/InitialAtomPhase.java

@@ -0,0 +1,24 @@
+package at.ac.tuwien.kr.alpha.api.config;
+
+import java.util.Arrays;
+import java.util.stream.Collectors;
+
+/**
+ * Determines the phase (truth value) initially assigned to all atoms.
+ * The initial phase is only considered for atoms that were never assigned a value during the run of the solver. It may
+ * have huge effects on runtime as the initial phase determines the location in the search space where the search
+ * process starts.
+ *
+ * Copyright (c) 2021, the Alpha Team.
+ */
+public enum InitialAtomPhase {
+	ALLTRUE,		// Initially assign all atoms to true.
+	ALLFALSE,		// Initially assign all atoms to false.
+	RANDOM,			// Initially assign randomly true/false.
+	RULESTRUEATOMSFALSE;	// Initially assign atoms representing rules to true, all others to false.
+
+	public static String listAllowedValues() {
+		return Arrays.stream(InitialAtomPhase.values()).map(InitialAtomPhase::toString)
+			.map(String::toLowerCase).collect(Collectors.joining(", "));
+	}
+}

alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java

@@ -1,5 +1,5 @@
-/**
- * Copyright (c) 2019, the Alpha Team.
+/*
+ * Copyright (c) 2019-2021, the Alpha Team.
  * All rights reserved.
  *
  * Additional changes made by Siemens.
@@ -27,16 +27,16 @@
  */
 package at.ac.tuwien.kr.alpha.api.config;
 
+import at.ac.tuwien.kr.alpha.api.Alpha;
+
 import java.util.Arrays;
 import java.util.Collections;
 import java.util.List;
 import java.util.stream.Collectors;
 
-import at.ac.tuwien.kr.alpha.api.Alpha;
-
 /**
  * Config structure for {@link Alpha} instances.
- * 
+ *
  * Copyright (c) 2021, the Alpha Team.
  */
 public class SystemConfig {
@@ -64,6 +64,8 @@ public class SystemConfig {
 	public static final boolean DEFAULT_GROUNDER_ACCUMULATOR_ENABLED = false;
 	public static final String DEFAULT_ATOM_SEPARATOR = ", ";
 	public static final AggregateRewritingConfig DEFAULT_AGGREGATE_REWRITING_CONFIG = new AggregateRewritingConfig();
+	public static final boolean DEFAULT_ENABLE_RESTARTS = false;
+	public static final InitialAtomPhase DEFAULT_PHASE_INITIALIZER = InitialAtomPhase.RULESTRUEATOMSFALSE;
 
 	private String grounderName = DEFAULT_GROUNDER_NAME;
 	private String solverName = DEFAULT_SOLVER_NAME;
@@ -85,6 +87,8 @@ public class SystemConfig {
 	private boolean grounderAccumulatorEnabled = DEFAULT_GROUNDER_ACCUMULATOR_ENABLED;
 	private String atomSeparator = DEFAULT_ATOM_SEPARATOR;
 	private AggregateRewritingConfig aggregateRewritingConfig = DEFAULT_AGGREGATE_REWRITING_CONFIG;
+	private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS;
+	private InitialAtomPhase phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER;
 
 	public String getGrounderName() {
 		return this.grounderName;
@@ -280,4 +284,23 @@ public void setAggregateRewritingConfig(AggregateRewritingConfig aggregateRewrit
 		this.aggregateRewritingConfig = aggregateRewritingConfig;
 	}
 
+	public boolean areRestartsEnabled() {
+		return areRestartsEnabled;
+	}
+
+	public void setRestartsEnabled(boolean areRestartsEnabled) {
+		this.areRestartsEnabled = areRestartsEnabled;
+	}
+
+	public InitialAtomPhase getPhaseInitializer() {
+		return phaseInitializer;
+	}
+
+	public void setPhaseInitializer(InitialAtomPhase phaseInitializer) {
+		this.phaseInitializer = phaseInitializer;
+	}
+
+	public void setPhaseInitializerName(String phaseInitializerName) {
+		this.phaseInitializer = InitialAtomPhase.valueOf(phaseInitializerName.toUpperCase());
+	}
 }

alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java

@@ -1,4 +1,4 @@
-/**
+/*
  * Copyright (c) 2016-2020, the Alpha Team.
  * All rights reserved.
  *
@@ -27,13 +27,13 @@
  */
 package at.ac.tuwien.kr.alpha.app.config;
 
-import java.io.ByteArrayOutputStream;
-import java.io.FileInputStream;
-import java.io.PrintWriter;
-import java.util.HashMap;
-import java.util.Map;
-import java.util.function.Consumer;
-
+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.InitialAtomPhase;
+import at.ac.tuwien.kr.alpha.api.config.InputConfig;
+import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
 import org.apache.commons.cli.CommandLine;
 import org.apache.commons.cli.DefaultParser;
 import org.apache.commons.cli.HelpFormatter;
@@ -45,12 +45,13 @@
 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;
+import java.io.ByteArrayOutputStream;
+import java.io.FileInputStream;
+import java.io.PrintWriter;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.function.Consumer;
+
 
 /**
  * Parses given argument lists (as passed when Alpha is called from command line) into {@link SystemConfig}s and
@@ -63,13 +64,13 @@ public class CommandLineParser {
 
 	//@formatter:off
 	/*
-	 * Whenever a new command line option is added, perform the following steps: 
-	 * 1. Add it as a constant option below. 
+	 * Whenever a new command line option is added, perform the following steps:
+	 * 1. Add it as a constant option below.
 	 * 2. Add the constant option into the Options "CLI_OPTS" in the static initializer.
-	 * 3. Add a handler method for it and add the respective map entry in initializeGlobalOptionHandlers 
+	 * 3. Add a handler method for it and add the respective map entry in initializeGlobalOptionHandlers
 	 *    or initializeInputOptionHandlers with a method reference to the handler.
 	 */
-	
+
 	// "special", i.e. non-configuration options
 	private static final Option OPT_HELP = Option.builder("h").longOpt("help").hasArg(false).desc("shows this help").build();
 
@@ -130,7 +131,7 @@ public class CommandLineParser {
 			.desc("Disable stratified evaluation")
 			.build();
 	private static final Option OPT_NO_NOGOOD_DELETION = Option.builder("dnd").longOpt("disableNoGoodDeletion")
-			.desc("disable the deletion of (learned, little active) nogoods (default: " 
+			.desc("disable the deletion of (learned, little active) nogoods (default: "
 					+ SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION + ")")
 			.build();
 	private static final Option OPT_GROUNDER_TOLERANCE_CONSTRAINTS = Option.builder("gtc").longOpt("grounderToleranceConstraints")
@@ -142,13 +143,21 @@ public class CommandLineParser {
 			.hasArg().argName("tolerance")
 			.build();
 	private static final Option OPT_GROUNDER_ACCUMULATOR_ENABLED = Option.builder("acc").longOpt("enableAccumulator")
-			.desc("activates the accumulator grounding strategy by disabling removal of instances from grounder memory in certain cases (default: " 
+			.desc("activates the accumulator grounding strategy by disabling removal of instances from grounder memory in certain cases (default: "
 					+ SystemConfig.DEFAULT_GROUNDER_ACCUMULATOR_ENABLED + ")")
 			.build();
 	private static final Option OPT_OUTPUT_ATOM_SEPARATOR = Option.builder("sep").longOpt("atomSeparator").hasArg(true).argName("separator")
 			.desc("a character (sequence) to use as separator for atoms in printed answer sets (default: "
 					+ SystemConfig.DEFAULT_ATOM_SEPARATOR + ")")
 			.build();
+	private static final Option OPT_ENABLE_RESTARTS = Option.builder("rs").longOpt("enableRestarts")
+		.desc("enable the usage of (dynamic and static) restarts (default: "
+			+ SystemConfig.DEFAULT_ENABLE_RESTARTS + ")")
+		.build();
+	private static final Option OPT_INITIAL_PHASE = Option.builder("ph").longOpt("initialPhase").hasArg(true).argName("initializer")
+		.desc("set the initial phase [ " + InitialAtomPhase.listAllowedValues() + " ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + "). " +
+			"Note: only works in conjunction with the " + Heuristic.VSIDS_PHASE_SAVING + " branching heuristic.")
+		.build();
 	//@formatter:on
 
 	private static final Options CLI_OPTS = new Options();
@@ -189,6 +198,8 @@ public class CommandLineParser {
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED);
 		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_OUTPUT_ATOM_SEPARATOR);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_ENABLE_RESTARTS);
+		CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_INITIAL_PHASE);
 	}
 
 	/*
@@ -246,6 +257,8 @@ private void initializeGlobalOptionHandlers() {
 		this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES.getOpt(), this::handleGrounderToleranceRules);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED.getOpt(), this::handleGrounderNoInstanceRemoval);
 		this.globalOptionHandlers.put(CommandLineParser.OPT_OUTPUT_ATOM_SEPARATOR.getOpt(), this::handleAtomSeparator);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_ENABLE_RESTARTS.getOpt(), this::handleEnableRestarts);
+		this.globalOptionHandlers.put(CommandLineParser.OPT_INITIAL_PHASE.getOpt(), this::handleInitialPhase);
 	}
 
 	private void initializeInputOptionHandlers() {
@@ -436,7 +449,7 @@ private void handleNoJustification(Option opt, SystemConfig cfg) {
 	private void handleDisableSortingGrid(Option opt, SystemConfig cfg) {
 		cfg.getAggregateRewritingConfig().setUseSortingGridEncoding(false);
 	}
-	
+
 	private void handleDisableNegativeSumElements(Option opt, SystemConfig cfg) {
 		cfg.getAggregateRewritingConfig().setSupportNegativeValuesInSums(false);
 	}
@@ -470,5 +483,18 @@ private void handleGrounderNoInstanceRemoval(Option opt, SystemConfig cfg) {
 	private void handleAtomSeparator(Option opt, SystemConfig cfg) {
 		cfg.setAtomSeparator(StringEscapeUtils.unescapeJava(opt.getValue(SystemConfig.DEFAULT_ATOM_SEPARATOR)));
 	}
-
+
+	private void handleEnableRestarts(Option opt, SystemConfig cfg) {
+		cfg.setRestartsEnabled(true);
+	}
+
+	private void handleInitialPhase(Option opt, SystemConfig cfg) throws ParseException {
+		String initialPhase = opt.getValue(SystemConfig.DEFAULT_PHASE_INITIALIZER.name());
+		try {
+			cfg.setPhaseInitializerName(initialPhase);
+		} catch (IllegalArgumentException e) {
+			throw new ParseException("Unknown initial phase: " + initialPhase + ". Please try one of the following: "
+					+ InitialAtomPhase.listAllowedValues());
+		}
+	}
 }

alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java

@@ -1,5 +1,5 @@
-/**
- * Copyright (c) 2019, the Alpha Team.
+/*
+ * Copyright (c) 2019-2020, the Alpha Team.
  * All rights reserved.
  *
  * Additional changes made by Siemens.
@@ -27,18 +27,18 @@
  */
 package at.ac.tuwien.kr.alpha.app.config;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
-import static org.junit.jupiter.api.Assertions.assertFalse;
-import static org.junit.jupiter.api.Assertions.assertThrows;
-import static org.junit.jupiter.api.Assertions.assertTrue;
+import at.ac.tuwien.kr.alpha.api.config.AlphaConfig;
+import at.ac.tuwien.kr.alpha.api.config.InitialAtomPhase;
+import org.apache.commons.cli.ParseException;
+import org.junit.jupiter.api.Test;
 
 import java.util.Arrays;
 import java.util.function.Consumer;
 
-import org.apache.commons.cli.ParseException;
-import org.junit.jupiter.api.Test;
-
-import at.ac.tuwien.kr.alpha.api.config.AlphaConfig;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static org.junit.jupiter.api.Assertions.assertTrue;
 
 public class CommandLineParserTest {
 
@@ -181,4 +181,32 @@ public void atomSeparator() throws ParseException {
 		assertEquals("some-string", cfg.getSystemConfig().getAtomSeparator());
 	}
 
+	@Test
+	public void initialPhase_alltrue() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-ph", "allTrue"});
+		assertEquals(InitialAtomPhase.ALLTRUE, alphaConfig.getSystemConfig().getPhaseInitializer());
+	}
+
+	@Test
+	public void initialPhase_allfalse() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-ph", "AllFalse"});
+		assertEquals(InitialAtomPhase.ALLFALSE, alphaConfig.getSystemConfig().getPhaseInitializer());
+	}
+
+	@Test
+	public void initialPhase_random() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-ph", "Random"});
+		assertEquals(InitialAtomPhase.RANDOM, alphaConfig.getSystemConfig().getPhaseInitializer());
+	}
+
+	@Test
+	public void initialPhase_rulesTrueAtomsFalse() throws ParseException {
+		CommandLineParser parser = new CommandLineParser(DEFAULT_COMMAND_LINE, DEFAULT_ABORT_ACTION);
+		AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-ph", "RulesTrueAtomsFalse"});
+		assertEquals(InitialAtomPhase.RULESTRUEATOMSFALSE, alphaConfig.getSystemConfig().getPhaseInitializer());
+	}
+
 }

alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/util/Util.java

@@ -37,6 +37,7 @@
 import java.util.Map;
 import java.util.SortedSet;
 import java.util.StringJoiner;
+import java.util.function.Function;
 import java.util.stream.Collector;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
@@ -62,9 +63,13 @@ public static <E> String join(String prefix, Iterable<E> iterable, String suffix
 	}
 
 	public static <E> String join(String prefix, Iterable<E> iterable, String delimiter, String suffix) {
+		return join(prefix, iterable, E::toString, delimiter, suffix);
+	}
+
+	public static <E> String join(String prefix, Iterable<E> iterable, Function<E, String> toStringMethod, String delimiter, String suffix) {
 		StringJoiner joiner = new StringJoiner(delimiter, prefix, suffix);
 		for (E element : iterable) {
-			joiner.add(element.toString());
+			joiner.add(toStringMethod.apply(element));
 		}
 		return joiner.toString();
 	}

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

@@ -71,6 +71,13 @@ default ThriceTruth getTruth(int atom) {
 	 */
 	Antecedent getImpliedBy(int atom);
 
+	/**
+	 * Returns the last truth value (i.e., phase) assigned to the atom.
+	 * @param atom the atom
+	 * @return the last truth value.
+	 */
+	boolean getLastValue(int atom);
+
 	/**
 	 * Determines if the given {@code noGood} is undefined in the current assignment.
 	 *