Merge branch 'master' into grounding_strategies

# Conflicts:
#	src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java
#	src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java
#	src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java
#	src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java
#	src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java

.travis.yml

@@ -16,7 +16,7 @@ language: java
 jdk:
  # LTS and in "Premier Support" as of 2019-03 (until 2022-03)
  - openjdk8
- - oraclejdk8
+ # - oraclejdk8 # Removed due to not being supported on Ubuntu xenial
  # LTS and in "Premier Support" as of 2019-03 (until 2023-09)
  - openjdk11
  - oraclejdk11

README.md

@@ -81,6 +81,8 @@ run into trouble feel free to file an issue.
 
 Peer-reviewed publications part of journals, conferences and workshops:
 
+ * [Exploiting Partial Knowledge in Declarative Domain-Specific Heuristics for ASP](https://doi.org/10.4204/EPTCS.306.9) ([supplementary material](https://git-ainf.aau.at/DynaCon/website/tree/master/supplementary_material/2019_ICLP_Domain-Specific_Heuristics))
+ * [Degrees of Laziness in Grounding: Effects of Lazy-Grounding Strategies on ASP Solving](https://doi.org/10.1007/978-3-030-20528-7_22) ([preprint](https://arxiv.org/abs/1903.12510) | [supplementary material](https://git-ainf.aau.at/DynaCon/website/tree/master/supplementary_material/2019_LPNMR_Degrees_of_Laziness))
  * [Exploiting Justifications for Lazy Grounding of Answer Set Programs](https://doi.org/10.24963/ijcai.2018/240)
  * [Lazy Grounding for Dynamic Configuration: Efficient Large-Scale (Re)Configuration of Cyber-Physical Systems with ASP](https://doi.org/10.1007/s13218-018-0536-x)
  * [Blending Lazy-Grounding and CDNL Search for Answer-Set Solving](https://doi.org/10.1007/978-3-319-61660-5_17) ([preprint](http://www.kr.tuwien.ac.at/research/systems/alpha/blending_lazy_grounding.pdf))

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

@@ -27,24 +27,7 @@
  */
 package at.ac.tuwien.kr.alpha;
 
-import java.io.IOException;
-import java.nio.charset.CodingErrorAction;
-import java.nio.file.Files;
-import java.nio.file.Paths;
-import java.util.List;
-import java.util.Map;
-import java.util.Random;
-import java.util.stream.Stream;
-
-import org.antlr.v4.runtime.CharStream;
-import org.antlr.v4.runtime.CharStreams;
-import org.apache.commons.lang3.StringUtils;
-
-import at.ac.tuwien.kr.alpha.common.AnswerSet;
-import at.ac.tuwien.kr.alpha.common.AtomStore;
-import at.ac.tuwien.kr.alpha.common.AtomStoreImpl;
-import at.ac.tuwien.kr.alpha.common.Predicate;
-import at.ac.tuwien.kr.alpha.common.Program;
+import at.ac.tuwien.kr.alpha.common.*;
 import at.ac.tuwien.kr.alpha.common.fixedinterpretations.PredicateInterpretation;
 import at.ac.tuwien.kr.alpha.config.InputConfig;
 import at.ac.tuwien.kr.alpha.config.SystemConfig;
@@ -54,8 +37,17 @@
 import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser;
 import at.ac.tuwien.kr.alpha.solver.Solver;
 import at.ac.tuwien.kr.alpha.solver.SolverFactory;
-import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration;
-import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfigurationBuilder;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CharStreams;
+import org.apache.commons.lang3.StringUtils;
+
+import java.io.IOException;
+import java.nio.charset.CodingErrorAction;
+import java.nio.file.Files;
+import java.nio.file.Paths;
+import java.util.List;
+import java.util.Map;
+import java.util.stream.Stream;
 
 public class Alpha {
 
@@ -110,25 +102,15 @@ public Program readProgramString(String aspString, Map<String, PredicateInterpre
  */
  public Solver prepareSolverFor(Program program, java.util.function.Predicate<Predicate> filter) {
  String grounderName = this.config.getGrounderName();
- String solverName = this.config.getSolverName();
- String nogoodStoreName = this.config.getNogoodStoreName();
- long seed = this.config.getSeed();
  boolean doDebugChecks = this.config.isDebugInternalChecks();
- boolean disableJustificationSearch = this.config.isDisableJustificationSearch();
-
- HeuristicsConfigurationBuilder heuristicsConfigurationBuilder = HeuristicsConfiguration.builder();
- heuristicsConfigurationBuilder.setHeuristic(this.config.getBranchingHeuristic());
- heuristicsConfigurationBuilder.setMomsStrategy(this.config.getMomsStrategy());
 
  GrounderHeuristicsConfiguration grounderHeuristicConfiguration = GrounderHeuristicsConfiguration
  .getInstance(this.config.getGrounderToleranceConstraints(), this.config.getGrounderToleranceRules());
 
  AtomStore atomStore = new AtomStoreImpl();
  Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, grounderHeuristicConfiguration, doDebugChecks);
 
- Solver solver = SolverFactory.getInstance(solverName, nogoodStoreName, atomStore, grounder, new Random(seed), heuristicsConfigurationBuilder.build(),
- doDebugChecks, disableJustificationSearch);
- return solver;
+ return SolverFactory.getInstance(this.config, atomStore, grounder);
  }
 
  public Solver prepareSolverFor(Program program) {

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

@@ -27,12 +27,14 @@
  */
 package at.ac.tuwien.kr.alpha.common;
 
+import at.ac.tuwien.kr.alpha.solver.Antecedent;
 import at.ac.tuwien.kr.alpha.solver.ThriceTruth;
 
 import java.util.Iterator;
 import java.util.Set;
 
-import static at.ac.tuwien.kr.alpha.common.Literals.*;
+import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
+import static at.ac.tuwien.kr.alpha.common.Literals.isNegated;
 
 public interface Assignment {
  Entry get(int atom);
@@ -66,9 +68,9 @@ default ThriceTruth getTruth(int atom) {
  /**
  * Returns the NoGood that implied the atom.
  * @param atom the atom.
- * @return the implying NoGood.
+ * @return the implying Antecedent.
  */
- NoGood getImpliedBy(int atom);
+ Antecedent getImpliedBy(int atom);
 
  /**
  * Determines if the given {@code noGood} is undefined in the current assignment.
@@ -86,11 +88,15 @@ default boolean isUndefined(NoGood noGood) {
  }
 
  /**
- * Returns an iterator over all new assignments. New assignments are only returned once.
- * @return an iterator over all new assignments to TRUE or MBT.
+ * Returns an iterator over all newly assigned atoms. New assignments are only returned once.
+ * @return an iterator over all atoms newly assigned to TRUE or MBT.
  */
  Iterator<Integer> getNewPositiveAssignmentsIterator();
 
+ /**
+ * Returns the new assignments to process.
+ * @return a Pollable that yields the atoms that were newly assigned.
+ */
  Pollable getAssignmentsToProcess();
 
  /**
@@ -111,40 +117,10 @@ interface Entry {
  ThriceTruth getTruth();
  int getAtom();
  int getDecisionLevel();
- NoGood getImpliedBy();
- int getPropagationLevel();
+ Antecedent getImpliedBy();
 
  boolean hasPreviousMBT();
  int getMBTDecisionLevel();
- int getMBTPropagationLevel();
- NoGood getMBTImpliedBy();
-
- default int getPropagationLevelRespectingLowerMBT() {
- return hasPreviousMBT() ? getMBTPropagationLevel() : getPropagationLevel();
- }
-
- default NoGood getImpliedByRespectingLowerMBT() {
- if (hasPreviousMBT()) {
- return getMBTImpliedBy();
- }
- return getImpliedBy();
- }
-
- /**
- * Returns the literal corresponding to this assignment
- * @return atomId if this entry is TRUE/MBT and -atomId if entry is FALSE.
- */
- default int getLiteral() {
- return atomToLiteral(getAtom(), getTruth().toBoolean());
- }
-
- /**
- * Returns the weakly assigned decision level.
- * @return the decision level of a previous MBT if it exists, otherwise the decision level of this entry.
- */
- default int getWeakDecisionLevel() {
- return hasPreviousMBT() ? getMBTDecisionLevel() : getDecisionLevel();
- }
 
  }
 

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

@@ -76,4 +76,8 @@ public static int atomToNegatedLiteral(int atom) {
  public static int positiveLiteral(int literal) {
  return literal & ~0x1;
  }
+
+ public static String literalToString(int literal) {
+ return (isPositive(literal) ? "+" : "-") + atomOf(literal);
+ }
 }

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

@@ -27,6 +27,8 @@
  */
 package at.ac.tuwien.kr.alpha.common;
 
+import at.ac.tuwien.kr.alpha.solver.Antecedent;
+
 import java.util.Arrays;
 import java.util.Iterator;
 import java.util.List;
@@ -137,6 +139,25 @@ public int size() {
  return literals.length;
  }
 
+ @Override
+ public Antecedent asAntecedent() {
+ return new Antecedent() {
+
+ @Override
+ public int[] getReasonLiterals() {
+ return NoGood.this.literals; // Beware: returned array must not be modified!
+ }
+
+ @Override
+ public void bumpActivity() {
+ }
+
+ @Override
+ public void decreaseActivity() {
+ }
+ };
+ }
+
  public NoGood withoutHead() {
  return new NoGood(type, literals.clone());
  }
@@ -262,11 +283,6 @@ public String toString() {
  return sb.toString();
  }
 
- @Override
- public NoGood getNoGood(int impliedAtom) {
- return this;
- }
-
  /**
  * The possible nogood types
  */

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

@@ -1,11 +1,11 @@
 package at.ac.tuwien.kr.alpha.common;
 
-import at.ac.tuwien.kr.alpha.solver.ImplicationReasonProvider;
+import at.ac.tuwien.kr.alpha.solver.Antecedent;
 
 /**
  * Copyright (c) 2018, the Alpha Team.
  */
-public interface NoGoodInterface extends ImplicationReasonProvider {
+public interface NoGoodInterface {
 
  /**
  * Returns the literal at the given index.
@@ -39,4 +39,6 @@ default boolean isUnary() {
  default boolean isBinary() {
  return size() == 2;
  }
+
+ Antecedent asAntecedent();
 }

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

@@ -27,26 +27,20 @@
  */
 package at.ac.tuwien.kr.alpha.config;
 
+import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation;
+import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic;
+import org.apache.commons.cli.*;
+import org.apache.commons.lang3.StringUtils;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
 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 org.apache.commons.cli.CommandLine;
-import org.apache.commons.cli.DefaultParser;
-import org.apache.commons.cli.HelpFormatter;
-import org.apache.commons.cli.Option;
-import org.apache.commons.cli.Options;
-import org.apache.commons.cli.ParseException;
-import org.apache.commons.lang3.StringUtils;
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
-
-import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation;
-import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic;
-
 /**
  * Parses given argument lists (as passed when Alpha is called from command line) into {@link AlphaConfig}s and {@link InputConfig}s.
  *
@@ -95,6 +89,9 @@ public class CommandLineParser {
  private static final Option OPT_MOMS_STRATEGY = Option.builder("ms").longOpt("momsStrategy").hasArg(true).argName("strategy")
  .desc("strategy for mom's heuristic (CountBinaryWatches or BinaryNoGoodPropagation, default: " + SystemConfig.DEFAULT_MOMS_STRATEGY.name() + ")")
  .build();
+ private static final Option OPT_REPLAY_CHOICES = Option.builder("rc").longOpt("replayChoices").hasArg().argName("choices")
+ .desc("comma-separated list of choices to be replayed (each choice is represented by a signed integer whose absolute value designates an atom ID and whose sign designates a truth value)")
+ .build();
  private static final Option OPT_QUIET = Option.builder("q").longOpt("quiet").desc("do not print answer sets (default: " + SystemConfig.DEFAULT_QUIET)
  .build();
  private static final Option OPT_STATS = Option.builder("st").longOpt("stats").desc("print statistics (default: " + SystemConfig.DEFAULT_PRINT_STATS + ")")
@@ -106,6 +103,10 @@ public class CommandLineParser {
  private static final Option OPT_NORMALIZATION_GRID = Option.builder("ng").longOpt("normalizationCountingGrid")
  .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: "
+ + SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION + ")")
+ .build();
  private static final Option OPT_GROUNDER_TOLERANCE_CONSTRAINTS = Option.builder("gtc").longOpt("grounderToleranceConstraints")
  .desc("grounder tolerance for constraints (default: " + SystemConfig.DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS + ")")
  .hasArg().argName("tolerance")
@@ -138,10 +139,12 @@ public class CommandLineParser {
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_DEBUG_INTERNAL_CHECKS);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_BRANCHING_HEURISTIC);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_MOMS_STRATEGY);
+ CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REPLAY_CHOICES);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_QUIET);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_STATS);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_JUSTIFICATION);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NORMALIZATION_GRID);
+ CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_NOGOOD_DELETION);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS);
  CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES);
  }
@@ -181,10 +184,12 @@ public CommandLineParser(String cmdLineSyntax, Consumer<String> abortAction) {
  this.globalOptionHandlers.put(CommandLineParser.OPT_DEBUG_INTERNAL_CHECKS.getOpt(), this::handleInternalChecks);
  this.globalOptionHandlers.put(CommandLineParser.OPT_BRANCHING_HEURISTIC.getOpt(), this::handleBranchingHeuristic);
  this.globalOptionHandlers.put(CommandLineParser.OPT_MOMS_STRATEGY.getOpt(), this::handleMomsStrategy);
+ this.globalOptionHandlers.put(CommandLineParser.OPT_REPLAY_CHOICES.getOpt(), this::handleReplayChoices);
  this.globalOptionHandlers.put(CommandLineParser.OPT_QUIET.getOpt(), this::handleQuiet);
  this.globalOptionHandlers.put(CommandLineParser.OPT_STATS.getOpt(), this::handleStats);
  this.globalOptionHandlers.put(CommandLineParser.OPT_NO_JUSTIFICATION.getOpt(), this::handleNoJustification);
  this.globalOptionHandlers.put(CommandLineParser.OPT_NORMALIZATION_GRID.getOpt(), this::handleNormalizationGrid);
+ this.globalOptionHandlers.put(CommandLineParser.OPT_NO_NOGOOD_DELETION.getOpt(), this::handleNoNoGoodDeletion);
  this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_CONSTRAINTS.getOpt(), this::handleGrounderToleranceConstraints);
  this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES.getOpt(), this::handleGrounderToleranceRules);
 
@@ -333,6 +338,15 @@ private void handleMomsStrategy(Option opt, SystemConfig cfg) throws ParseExcept
  }
  }
 
+ private void handleReplayChoices(Option opt, SystemConfig cfg) throws ParseException {
+ String replayChoices = opt.getValue(SystemConfig.DEFAULT_REPLAY_CHOICES.toString());
+ try {
+ cfg.setReplayChoices(replayChoices);
+ } catch (NumberFormatException e) {
+ throw new ParseException("Cannot parse list of signed integers indicating choices to be replayed: " + replayChoices);
+ }
+ }
+
  private void handleQuiet(Option opt, SystemConfig cfg) {
  cfg.setQuiet(true);
  }
@@ -352,12 +366,16 @@ private void handleNoJustification(Option opt, SystemConfig cfg) {
  private void handleNormalizationGrid(Option opt, SystemConfig cfg) {
  cfg.setUseNormalizationGrid(true);
  }
-
+
+ private void handleNoNoGoodDeletion(Option opt, SystemConfig cfg) {
+ cfg.setDisableNoGoodDeletion(true);
+ }
+
  private void handleGrounderToleranceConstraints(Option opt, SystemConfig cfg) {
  String grounderToleranceConstraints = opt.getValue(SystemConfig.DEFAULT_GROUNDER_TOLERANCE_CONSTRAINTS);
  cfg.setGrounderToleranceConstraints(grounderToleranceConstraints);
  }
- 
+
  private void handleGrounderToleranceRules(Option opt, SystemConfig cfg) {
  String grounderToleranceRules = opt.getValue(SystemConfig.DEFAULT_GROUNDER_TOLERANCE_RULES);
  cfg.setGrounderToleranceRules(grounderToleranceRules);