Phase saving, restarts, and heuristic performance logs

src/main/java/at/ac/tuwien/kr/alpha/AnswerSetToXlsxWriter.java

@@ -1,5 +1,14 @@
 package at.ac.tuwien.kr.alpha;
 
+import at.ac.tuwien.kr.alpha.api.mapper.AnswerSetToObjectMapper;
+import at.ac.tuwien.kr.alpha.api.mapper.impl.AnswerSetToWorkbookMapper;
+import at.ac.tuwien.kr.alpha.common.AnswerSet;
+import org.apache.poi.ss.usermodel.Cell;
+import org.apache.poi.ss.usermodel.Row;
+import org.apache.poi.ss.usermodel.Sheet;
+import org.apache.poi.ss.usermodel.Workbook;
+import org.apache.poi.xssf.usermodel.XSSFWorkbook;
+
 import java.io.IOException;
 import java.io.OutputStream;
 import java.nio.file.Files;
@@ -8,16 +17,6 @@
 import java.nio.file.StandardOpenOption;
 import java.util.function.BiConsumer;
 
-import org.apache.poi.ss.usermodel.Cell;
-import org.apache.poi.ss.usermodel.Row;
-import org.apache.poi.ss.usermodel.Sheet;
-import org.apache.poi.ss.usermodel.Workbook;
-import org.apache.poi.xssf.usermodel.XSSFWorkbook;
-
-import at.ac.tuwien.kr.alpha.api.mapper.AnswerSetToObjectMapper;
-import at.ac.tuwien.kr.alpha.api.mapper.impl.AnswerSetToWorkbookMapper;
-import at.ac.tuwien.kr.alpha.common.AnswerSet;
-
 public class AnswerSetToXlsxWriter implements BiConsumer<Integer, AnswerSet> {
 
  private String targetBasePath;

src/main/java/at/ac/tuwien/kr/alpha/Main.java

@@ -27,19 +27,6 @@
  */
 package at.ac.tuwien.kr.alpha;
 
-import java.io.FileNotFoundException;
-import java.io.IOException;
-import java.nio.file.Paths;
-import java.util.concurrent.atomic.AtomicInteger;
-import java.util.function.BiConsumer;
-import java.util.stream.Collectors;
-import java.util.stream.Stream;
-
-import org.antlr.v4.runtime.RecognitionException;
-import org.apache.commons.cli.ParseException;
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
-
 import at.ac.tuwien.kr.alpha.api.Alpha;
 import at.ac.tuwien.kr.alpha.common.AnswerSet;
 import at.ac.tuwien.kr.alpha.common.Program;
@@ -48,6 +35,18 @@
 import at.ac.tuwien.kr.alpha.config.InputConfig;
 import at.ac.tuwien.kr.alpha.solver.Solver;
 import at.ac.tuwien.kr.alpha.solver.SolverMaintainingStatistics;
+import org.antlr.v4.runtime.RecognitionException;
+import org.apache.commons.cli.ParseException;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import java.nio.file.Paths;
+import java.util.concurrent.atomic.AtomicInteger;
+import java.util.function.BiConsumer;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 /**
  * Main entry point for Alpha.

src/main/java/at/ac/tuwien/kr/alpha/api/mapper/impl/AnswerSetToWorkbookMapper.java

@@ -25,8 +25,11 @@
  */
 package at.ac.tuwien.kr.alpha.api.mapper.impl;
 
-import java.util.List;
-
+import at.ac.tuwien.kr.alpha.api.mapper.AnswerSetToObjectMapper;
+import at.ac.tuwien.kr.alpha.common.AnswerSet;
+import at.ac.tuwien.kr.alpha.common.Predicate;
+import at.ac.tuwien.kr.alpha.common.atoms.Atom;
+import at.ac.tuwien.kr.alpha.common.terms.Term;
 import org.apache.poi.ss.usermodel.Cell;
 import org.apache.poi.ss.usermodel.CellStyle;
 import org.apache.poi.ss.usermodel.FillPatternType;
@@ -39,11 +42,7 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import at.ac.tuwien.kr.alpha.api.mapper.AnswerSetToObjectMapper;
-import at.ac.tuwien.kr.alpha.common.AnswerSet;
-import at.ac.tuwien.kr.alpha.common.Predicate;
-import at.ac.tuwien.kr.alpha.common.atoms.Atom;
-import at.ac.tuwien.kr.alpha.common.terms.Term;
+import java.util.List;
 
 /**
  * Implementation of {@link AnswerSetToObjectMapper} that generates an office open xml workbook ("excel file") from a given answer set.

src/main/java/at/ac/tuwien/kr/alpha/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.
  *

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

@@ -35,8 +35,15 @@
 import java.util.stream.IntStream;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
-import static at.ac.tuwien.kr.alpha.common.Literals.*;
-import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.*;
+import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
+import static at.ac.tuwien.kr.alpha.common.Literals.isNegated;
+import static at.ac.tuwien.kr.alpha.common.Literals.isPositive;
+import static at.ac.tuwien.kr.alpha.common.Literals.negateLiteral;
+import static at.ac.tuwien.kr.alpha.common.Literals.positiveLiteral;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.INTERNAL;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.LEARNT;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.STATIC;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.SUPPORT;
 
 public class NoGood implements NoGoodInterface, Comparable<NoGood> {
  public static final int HEAD = 0;

src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ComparisonLiteral.java

@@ -34,7 +34,11 @@
 import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
 import at.ac.tuwien.kr.alpha.grounder.Substitution;
 
-import java.util.*;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Set;
 
 import static at.ac.tuwien.kr.alpha.common.terms.ArithmeticTerm.evaluateGroundTerm;
 

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

@@ -112,7 +112,7 @@ public class CommandLineParser {
  .desc("use counting grid normalization instead of sorting circuit for #count (default: " + SystemConfig.DEFAULT_USE_NORMALIZATION_GRID + ")")
  .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")
@@ -127,6 +127,13 @@ public class CommandLineParser {
  .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_ENABLE_RESTARTS = Option.builder("rs").longOpt("enableRestarts")
+ .desc("enable the usage of (dynamic and static) restarts (default: "
+ + SystemConfig.DEFAULT_ENABLE_RESTARTS + ")")
+ .build();
+ private static final Option OPT_INITIAL_PHASE = Option.builder("ph").longOpt("initialPhase").hasArg(true).argName("initializer")
+ .desc("set the initial phase [ alltrue | allfalse | random ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + ")")
+ .build();
  //@formatter:on
 
  private static final Options CLI_OPTS = new Options();
@@ -162,6 +169,8 @@ public class CommandLineParser {
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED);
+ CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_ENABLE_RESTARTS);
+ CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_INITIAL_PHASE);
  }
 
  /*
@@ -208,6 +217,8 @@ public CommandLineParser(String cmdLineSyntax, Consumer<String> abortAction) {
  this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS.getOpt(), this::handleGrounderToleranceConstraints);
  this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES.getOpt(), this::handleGrounderToleranceRules);
  this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED.getOpt(), this::handleGrounderNoInstanceRemoval);
+ this.globalOptionHandlers.put(CommandLineParser.OPT_ENABLE_RESTARTS.getOpt(), this::handleEnableRestarts);
+ this.globalOptionHandlers.put(CommandLineParser.OPT_INITIAL_PHASE.getOpt(), this::handleInitialPhase);
 
  this.inputOptionHandlers.put(CommandLineParser.OPT_NUM_ANSWER_SETS.getOpt(), this::handleNumAnswerSets);
  this.inputOptionHandlers.put(CommandLineParser.OPT_INPUT.getOpt(), this::handleInput);
@@ -410,4 +421,11 @@ private void handleGrounderNoInstanceRemoval(Option opt, SystemConfig cfg) {
  cfg.setGrounderAccumulatorEnabled(true);
  }
 
+ private void handleEnableRestarts(Option opt, SystemConfig cfg) {
+ cfg.setRestartsEnabled(true);
+ }
+
+ private void handleInitialPhase(Option opt, SystemConfig cfg) {
+ cfg.setPhaseInitializer(opt.getValue(SystemConfig.DEFAULT_PHASE_INITIALIZER));
+ }
 }

src/main/java/at/ac/tuwien/kr/alpha/config/InputConfig.java

@@ -1,14 +1,15 @@
 package at.ac.tuwien.kr.alpha.config;
 
+import at.ac.tuwien.kr.alpha.common.Predicate;
+import at.ac.tuwien.kr.alpha.common.fixedinterpretations.PredicateInterpretation;
+
 import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
 
 import at.ac.tuwien.kr.alpha.api.externals.Externals;
-import at.ac.tuwien.kr.alpha.common.Predicate;
-import at.ac.tuwien.kr.alpha.common.fixedinterpretations.PredicateInterpretation;
 
 public class InputConfig {
 

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

@@ -60,6 +60,8 @@ public class SystemConfig {
  public static final String DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS = GrounderHeuristicsConfiguration.STRICT_STRING;
  public static final String DEFAULT_GROUNDER_TOLERANCE_RULES = GrounderHeuristicsConfiguration.STRICT_STRING;
  public static final boolean DEFAULT_GROUNDER_ACCUMULATOR_ENABLED = false;
+ public static final boolean DEFAULT_ENABLE_RESTARTS = false;
+ public static final String DEFAULT_PHASE_INITIALIZER = "random";
 
  private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME;
  private String solverName = SystemConfig.DEFAULT_SOLVER_NAME;
@@ -79,6 +81,8 @@ public class SystemConfig {
  private String grounderToleranceConstraints = DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS;
  private String grounderToleranceRules = DEFAULT_GROUNDER_TOLERANCE_RULES;
  private boolean grounderAccumulatorEnabled = DEFAULT_GROUNDER_ACCUMULATOR_ENABLED;
+ private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS;
+ private String phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER;
 
  public String getGrounderName() {
  return this.grounderName;
@@ -235,4 +239,20 @@ public boolean isGrounderAccumulatorEnabled() {
  public void setGrounderAccumulatorEnabled(boolean grounderAccumulatorEnabled) {
  this.grounderAccumulatorEnabled = grounderAccumulatorEnabled;
  }
+ public boolean areRestartsEnabled() {
+ return areRestartsEnabled;
+ }
+
+ public void setRestartsEnabled(boolean areRestartsEnabled) {
+ this.areRestartsEnabled = areRestartsEnabled;
+ }
+
+ public String getPhaseInitializerName() {
+ return phaseInitializer;
+ }
+
+ public void setPhaseInitializer(String phaseInitializer) {
+ this.phaseInitializer = phaseInitializer;
+ }
+
 }

src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java

@@ -121,7 +121,7 @@ public String toString() {
  }
  sb.append(" disablers: ");
  for (Map.Entry<Integer, Integer> disablers : newChoiceAtoms.getRight().entrySet()) {
- sb.append(disablers.getKey()).append("/").append(disablers.getValue());
+ sb.append(disablers.getKey()).append("/").append(disablers.getValue()).append(", ");
  }
  return sb.append("]").toString();
  }

src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java

@@ -32,6 +32,7 @@
 import at.ac.tuwien.kr.alpha.common.IntIterator;
 import at.ac.tuwien.kr.alpha.common.NoGood;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import org.apache.commons.lang3.tuple.Pair;
 
 import java.util.Map;
@@ -79,4 +80,11 @@ public interface Grounder {
  * @return
  */
  int register(NoGood noGood);
+
+
+ /**
+ * Returns the relation between atoms and choices in form of an {@link AtomChoiceRelation} object.
+ * @return the {@link AtomChoiceRelation} of the grounded program parts.
+ */
+ AtomChoiceRelation getAtomChoiceRelation();
 }

src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java

@@ -51,6 +51,7 @@
 import at.ac.tuwien.kr.alpha.grounder.bridges.Bridge;
 import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration;
 import at.ac.tuwien.kr.alpha.grounder.structure.AnalyzeUnjustified;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis;
 import at.ac.tuwien.kr.alpha.grounder.transformation.CardinalityNormalization;
 import at.ac.tuwien.kr.alpha.grounder.transformation.ChoiceHeadToNormal;
@@ -103,6 +104,7 @@ public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGr
  private final Map<IndexedInstanceStorage, ArrayList<FirstBindingAtom>> rulesUsingPredicateWorkingMemory = new HashMap<>();
  private final Map<NonGroundRule, HashSet<Substitution>> knownGroundingSubstitutions = new HashMap<>();
  private final Map<Integer, NonGroundRule> knownNonGroundRules = new HashMap<>();
+ private final AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation();
 
  private ArrayList<NonGroundRule> fixedRules = new ArrayList<>();
  private LinkedHashSet<Atom> removeAfterObtainingNewNoGoods = new LinkedHashSet<>();
@@ -137,11 +139,15 @@ private NaiveGrounder(Program program, AtomStore atomStore, GrounderHeuristicsCo
 
  final Set<NonGroundRule> uniqueGroundRulePerGroundHead = getRulesWithUniqueHead();
  choiceRecorder = new ChoiceRecorder(atomStore);
- noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, programAnalysis, uniqueGroundRulePerGroundHead);
-
+ noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, programAnalysis, uniqueGroundRulePerGroundHead, atomChoiceRelation);
  this.debugInternalChecks = debugInternalChecks;
  }
 
+ @Override
+ public AtomChoiceRelation getAtomChoiceRelation() {
+ return atomChoiceRelation;
+ }
+
  private void initializeFactsAndRules(Program program) {
  // initialize all facts
  for (Atom fact : program.getFacts()) {

src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java

@@ -34,6 +34,7 @@
 import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral;
 import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom;
 import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis;
 
 import java.util.*;
@@ -52,13 +53,15 @@ public class NoGoodGenerator {
  private final Map<Predicate, LinkedHashSet<Instance>> factsFromProgram;
  private final ProgramAnalysis programAnalysis;
  private final Set<NonGroundRule> uniqueGroundRulePerGroundHead;
+ private final AtomChoiceRelation atomChoiceRelation;
 
- NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map<Predicate, LinkedHashSet<Instance>> factsFromProgram, ProgramAnalysis programAnalysis, Set<NonGroundRule> uniqueGroundRulePerGroundHead) {
+ NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map<Predicate, LinkedHashSet<Instance>> factsFromProgram, ProgramAnalysis programAnalysis, Set<NonGroundRule> uniqueGroundRulePerGroundHead, AtomChoiceRelation atomChoiceRelation) {
  this.atomStore = atomStore;
  this.choiceRecorder = recorder;
  this.factsFromProgram = factsFromProgram;
  this.programAnalysis = programAnalysis;
  this.uniqueGroundRulePerGroundHead = uniqueGroundRulePerGroundHead;
+ this.atomChoiceRelation = atomChoiceRelation;
  }
 
  /**
@@ -126,6 +129,15 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround
  result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals, negLiterals, bodyRepresentingLiteral));
  }
 
+ // Record atom-choiceAtom relationships for rules that are choice points.
+ if (!negLiterals.isEmpty()) {
+ atomChoiceRelation.growForMaxAtomId(atomStore.getMaxAtomId());
+ atomChoiceRelation.addRelation(headId, atomOf(bodyRepresentingLiteral));
+ for (Integer negLiteral : negLiterals) {
+ atomChoiceRelation.addRelation(atomOf(negLiteral), atomOf(bodyRepresentingLiteral));
+ }
+ }
+
  return result;
  }
 

src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java

@@ -3,6 +3,7 @@
 import at.ac.tuwien.kr.alpha.common.Assignment;
 import at.ac.tuwien.kr.alpha.common.atoms.Atom;
 import at.ac.tuwien.kr.alpha.common.atoms.Literal;
+import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation;
 
 import java.util.Set;
 
@@ -32,4 +33,10 @@ public interface ProgramAnalyzingGrounder extends Grounder {
  * @return the corresponding NonGroundRule.
  */
  NonGroundRule getNonGroundRule(Integer ruleId);
+
+ /**
+ * Provides relationship information between atoms and choice points influencing their truth values.
+ * @return the {@link AtomChoiceRelation}.
+ */
+ AtomChoiceRelation getAtomChoiceRelation();
 }

src/main/java/at/ac/tuwien/kr/alpha/grounder/RuleGroundingOrders.java

@@ -31,7 +31,15 @@
 import at.ac.tuwien.kr.alpha.common.atoms.Literal;
 import at.ac.tuwien.kr.alpha.common.terms.VariableTerm;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedHashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Set;
 
 /**
  * Provides the grounder with information on the order to ground the literals in the body of a rule.