diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/Heuristic.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/Heuristic.java index f9cb45982..119d5de9f 100644 --- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/Heuristic.java +++ b/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 diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/InitialAtomPhase.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/InitialAtomPhase.java new file mode 100644 index 000000000..40efaea15 --- /dev/null +++ b/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(", ")); + } +} 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..a489c9e61 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 @@ -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()); + } } 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 4b3ccf1f5..396e10824 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 @@ -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()); + } + } } diff --git a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java b/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java index f77f6527e..cab193404 100644 --- a/alpha-cli-app/src/test/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParserTest.java +++ b/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()); + } + } diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/util/Util.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/util/Util.java index 6e0c7ff8f..87d185b42 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/util/Util.java +++ b/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 String join(String prefix, Iterable iterable, String suffix } public static String join(String prefix, Iterable iterable, String delimiter, String suffix) { + return join(prefix, iterable, E::toString, delimiter, suffix); + } + + public static String join(String prefix, Iterable iterable, Function 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(); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/Assignment.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/Assignment.java index 47ae1790a..fa086d784 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/common/Assignment.java +++ b/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. * 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 19b012b41..a16d4566d 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 @@ -28,18 +28,25 @@ package at.ac.tuwien.kr.alpha.core.grounder; import at.ac.tuwien.kr.alpha.commons.util.IntIdGenerator; +import at.ac.tuwien.kr.alpha.commons.util.Util; import at.ac.tuwien.kr.alpha.core.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.NoGood; - import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Pair; -import java.util.*; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; import static at.ac.tuwien.kr.alpha.core.atoms.ChoiceAtom.off; import static at.ac.tuwien.kr.alpha.core.atoms.ChoiceAtom.on; -import static at.ac.tuwien.kr.alpha.core.atoms.Literals.*; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.negateLiteral; import static java.util.Collections.emptyList; public class ChoiceRecorder { @@ -117,14 +124,9 @@ public void addHeadToBody(int headId, int bodyId) { @Override public String toString() { - StringBuilder sb = new StringBuilder("[enablers: "); - for (Map.Entry enablers : newChoiceAtoms.getLeft().entrySet()) { - sb.append(enablers.getKey()).append("/").append(enablers.getValue()).append(", "); - } - sb.append(" disablers: "); - for (Map.Entry disablers : newChoiceAtoms.getRight().entrySet()) { - sb.append(disablers.getKey()).append("/").append(disablers.getValue()); - } - return sb.append("]").toString(); + StringBuilder sb = new StringBuilder(); + sb.append(Util.join("[enablers: ", newChoiceAtoms.getLeft().entrySet(), (entry) -> entry.getKey() + "/" + entry.getValue(), ", ", "")); + sb.append(Util.join(" disablers: ", newChoiceAtoms.getRight().entrySet(), (entry) -> entry.getKey() + "/" + entry.getValue(), ", ", "]")); + return sb.toString(); } } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java index 2c697f955..d0cddeb12 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java @@ -37,6 +37,7 @@ import at.ac.tuwien.kr.alpha.core.common.Assignment; import at.ac.tuwien.kr.alpha.core.common.IntIterator; import at.ac.tuwien.kr.alpha.core.common.NoGood; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; public interface Grounder { /** @@ -80,4 +81,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(); } 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 1e498d50d..bf32b07f8 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 @@ -76,11 +76,12 @@ import at.ac.tuwien.kr.alpha.core.grounder.structure.AnalyzeUnjustified; import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; /** * A semi-naive grounder. * - * Copyright (c) 2016-2020, the Alpha Team. + * Copyright (c) 2016-2021, the Alpha Team. */ public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGrounder { private static final Logger LOGGER = LoggerFactory.getLogger(NaiveGrounder.class); @@ -96,6 +97,7 @@ public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGr private final Map> factsFromProgram; private final Map> rulesUsingPredicateWorkingMemory = new HashMap<>(); private final Map knownNonGroundRules; + private final AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation(); private ArrayList fixedRules = new ArrayList<>(); private LinkedHashSet removeAfterObtainingNewNoGoods = new LinkedHashSet<>(); @@ -135,7 +137,7 @@ private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeur final Set uniqueGroundRulePerGroundHead = getRulesWithUniqueHead(); choiceRecorder = new ChoiceRecorder(atomStore); - noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, this.program, uniqueGroundRulePerGroundHead); + noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, this.program, uniqueGroundRulePerGroundHead, atomChoiceRelation); this.debugInternalChecks = debugInternalChecks; @@ -147,6 +149,11 @@ private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeur this.ruleInstantiator = new LiteralInstantiator(this.instantiationStrategy); } + @Override + public AtomChoiceRelation getAtomChoiceRelation() { + return atomChoiceRelation; + } + private void initializeFactsAndRules() { // Initialize all facts. for (Atom fact : program.getFacts()) { @@ -221,7 +228,7 @@ private Set getRulesWithUniqueHead() { /** * Registers a starting literal of a NonGroundRule at its corresponding working memory. - * + * * @param nonGroundRule the rule in which the literal occurs. */ private void registerLiteralAtWorkingMemory(Literal literal, CompiledRule nonGroundRule) { @@ -291,7 +298,7 @@ public AnswerSet assignmentToAnswerSet(Iterable trueAtoms) { /** * Prepares facts of the input program for joining and derives all NoGoods representing ground rules. May only be called once. - * + * * @return */ protected HashMap bootstrap() { @@ -497,9 +504,9 @@ private BindingResult pushBackAndBindNextAtomInRule(RuleGroundingOrder grounding * Computes ground substitutions for a literal based on a {@link RuleGroundingOrderImpl} and a {@link BasicSubstitution}. * * Computes ground substitutions for the literal at position orderPosition of groundingOrder - * Actual substitutions are computed by this grounder's {@link LiteralInstantiator}. + * Actual substitutions are computed by this grounder's {@link LiteralInstantiator}. * - * @param groundingOrder a {@link RuleGroundingOrderImpl} representing the body literals of a rule in the + * @param groundingOrder a {@link RuleGroundingOrderImpl} representing the body literals of a rule in the * sequence in which the should be bound during grounding. * @param orderPosition the current position within groundingOrder, indicates which literal should be bound * @param originalTolerance the original tolerance of the used grounding heuristic 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 3d97e7fa6..2f679ce0f 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 @@ -52,6 +52,7 @@ import at.ac.tuwien.kr.alpha.core.common.NoGood; import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; import at.ac.tuwien.kr.alpha.core.rules.CompiledRule; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; /** * Class to generate ground NoGoods out of non-ground rules and grounding substitutions. @@ -63,13 +64,15 @@ public class NoGoodGenerator { private final Map> factsFromProgram; private final CompiledProgram programAnalysis; private final Set uniqueGroundRulePerGroundHead; + private final AtomChoiceRelation atomChoiceRelation; - NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map> factsFromProgram, CompiledProgram programAnalysis, Set uniqueGroundRulePerGroundHead) { + NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map> factsFromProgram, CompiledProgram programAnalysis, Set uniqueGroundRulePerGroundHead, AtomChoiceRelation atomChoiceRelation) { this.atomStore = atomStore; this.choiceRecorder = recorder; this.factsFromProgram = factsFromProgram; this.programAnalysis = programAnalysis; this.uniqueGroundRulePerGroundHead = uniqueGroundRulePerGroundHead; + this.atomChoiceRelation = atomChoiceRelation; } /** @@ -135,6 +138,13 @@ List generateNoGoodsFromGroundSubstitution(final CompiledRule nonGroundR // If the body of the rule contains negation, add choices. if (!negLiterals.isEmpty()) { result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals, negLiterals, bodyRepresentingLiteral)); + + // Record atom-choiceAtom relationships for rules that are choice points. + atomChoiceRelation.growForMaxAtomId(atomStore.getMaxAtomId()); + atomChoiceRelation.addRelation(headId, atomOf(bodyRepresentingLiteral)); + for (Integer negLiteral : negLiterals) { + atomChoiceRelation.addRelation(atomOf(negLiteral), atomOf(bodyRepresentingLiteral)); + } } return result; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AtomChoiceRelation.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AtomChoiceRelation.java new file mode 100644 index 000000000..d5b8e7a63 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AtomChoiceRelation.java @@ -0,0 +1,50 @@ +package at.ac.tuwien.kr.alpha.core.grounder.structure; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.List; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; + +/** + * Stores and provides relationships between ordinary atoms and those that represent choice points. + * More specifically: relations between atoms and choice points (=body-representing atoms) influencing their truth + * values. Moreover, each body-representing atom is in relation with itself. + * + * Copyright (c) 2019, the Alpha Team. + */ +public class AtomChoiceRelation { + @SuppressWarnings("unchecked") + private ArrayList[] atomToChoiceAtoms = new ArrayList[0]; + + public void addRelation(int atom, int bodyRepresentingAtom) { + if (atomToChoiceAtoms[atom] == null) { + atomToChoiceAtoms[atom] = new ArrayList<>(); + } + atomToChoiceAtoms[atom].add(bodyRepresentingAtom); + + // Ensure that each bodyRepresentingAtom is in relation with itself. + if (atomToChoiceAtoms[bodyRepresentingAtom] == null) { + atomToChoiceAtoms[bodyRepresentingAtom] = new ArrayList<>(); + atomToChoiceAtoms[bodyRepresentingAtom].add(bodyRepresentingAtom); + } + } + + public List getRelatedChoiceAtoms(int atom) { + if (atomToChoiceAtoms[atom] == null) { + return Collections.emptyList(); + } + return Collections.unmodifiableList(atomToChoiceAtoms[atom]); + } + + public void growForMaxAtomId(int maxAtomId) { + if (maxAtomId >= atomToChoiceAtoms.length) { + int newCapacity = arrayGrowthSize(atomToChoiceAtoms.length); + if (newCapacity < maxAtomId + 1) { + newCapacity = maxAtomId + 1; + } + atomToChoiceAtoms = Arrays.copyOf(atomToChoiceAtoms, newCapacity); + } + } +} 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..5cf8de224 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 @@ -221,8 +221,10 @@ void recomputeActive() { changed = true; LOGGER.debug("Deactivating choice point for atom {}", this.atom); } - if (changed && activityListener != null) { - activityListener.callbackOnChanged(atom, isActive); + if (changed + //&& isActive // FIXME: not sure if this should be in, apparently bugs VSIDS. + && activityListener != null) { + activityListener.callbackOnChange(atom); } } @@ -232,8 +234,8 @@ public String toString() { } } - public static interface ActivityListener { - void callbackOnChanged(int atom, boolean active); + public interface ActivityListener { + void callbackOnChange(int atom); } } 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 b6d952e23..88e95f284 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 @@ -84,6 +84,7 @@ public class DefaultSolver extends AbstractSolver implements StatisticsReporting private final ChoiceManager choiceManager; private final WritableAssignment assignment; private final GroundConflictNoGoodLearner learner; + private final MixedRestartStrategy restartStrategy; private final BranchingHeuristic branchingHeuristic; private int mbtAtFixpoint; @@ -111,10 +112,16 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.choiceManager = new ChoiceManager(assignment, store); this.choiceManager.setChecksEnabled(config.isDebugInternalChecks()); this.learner = new GroundConflictNoGoodLearner(assignment, atomStore); + LearnedNoGoodDeletion learnedNoGoodDeletion = this.store instanceof NoGoodStoreAlphaRoaming ? ((NoGoodStoreAlphaRoaming)store).getLearnedNoGoodDeletion() : null; + if (config.areRestartsEnabled() && this.store instanceof NoGoodStoreAlphaRoaming) { + this.restartStrategy = new MixedRestartStrategy(learnedNoGoodDeletion); + } else { + this.restartStrategy = null; + } this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration); this.disableJustifications = config.isDisableJustificationSearch(); this.disableNoGoodDeletion = config.isDisableNoGoodDeletion(); - this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000); + this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, restartStrategy, learnedNoGoodDeletion, branchingHeuristic, 1000); } private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) { @@ -144,6 +151,10 @@ protected boolean tryAdvance(Consumer action) { return false; } ConflictCause conflictCause = propagate(); + deleteLearnedNoGoodsIfPossible(conflictCause); + if (executeRestart(conflictCause)) { + continue; + } if (conflictCause != null) { LOGGER.debug("Conflict encountered, analyzing conflict."); learnFromConflict(conflictCause); @@ -171,6 +182,24 @@ private void initializeSearch() { searchState.hasBeenInitialized = true; } + private void deleteLearnedNoGoodsIfPossible(ConflictCause conflictCause) { + // Run learned NoGood deletion strategy if no conflict occured. + if (conflictCause == null && !disableNoGoodDeletion) { + store.cleanupLearnedNoGoods(); + } + } + + private boolean executeRestart(ConflictCause conflictCause) { + if (conflictCause == null && restartStrategy != null && restartStrategy.shouldRestart()) { + // Restart if necessary. + LOGGER.trace("Restarting search."); + choiceManager.backjump(0); + restartStrategy.onRestart(); + return true; + } + return false; + } + private void prepareForSubsequentAnswerSet() { // We already found one Answer-Set and are requested to find another one. searchState.afterAllAtomsAssigned = false; @@ -229,10 +258,6 @@ private ConflictCause propagate() { LOGGER.trace("Doing propagation step."); ConflictCause conflictCause = store.propagate(); LOGGER.trace("Assignment after propagation is: {}", assignment); - if (!disableNoGoodDeletion && conflictCause == null) { - // Run learned-NoGood deletion-strategy. - store.cleanupLearnedNoGoods(); - } return conflictCause; } @@ -288,6 +313,9 @@ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) { } branchingHeuristic.analyzedConflict(analysisResult); + if (restartStrategy != null) { + restartStrategy.newConflictWithLbd(analysisResult.lbd); + } if (analysisResult.learnedNoGood == null) { throw oops("Did not learn new NoGood from conflict."); @@ -465,6 +493,7 @@ private boolean ingest(Map obtained) { store.growForMaxAtomId(maxAtomId); choiceManager.growForMaxAtomId(maxAtomId); branchingHeuristic.growForMaxAtomId(maxAtomId); + choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies()); branchingHeuristic.newNoGoods(obtained.values()); LinkedList> noGoodsToAdd = new LinkedList<>(obtained.entrySet()); @@ -511,7 +540,6 @@ private boolean fixContradiction(Map.Entry noGoodEntry, Conflic } private boolean choose() { - choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies()); choiceManager.updateAssignments(); // Hint: for custom heuristics, evaluate them here and pick a value if the heuristics suggests one. diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/LearnedNoGoodDeletion.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/LearnedNoGoodDeletion.java index f77211baa..50345f865 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/LearnedNoGoodDeletion.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/LearnedNoGoodDeletion.java @@ -26,6 +26,7 @@ class LearnedNoGoodDeletion { private final NoGoodStoreAlphaRoaming store; private final Assignment assignment; private int conflictCounter; + private int totalConflictsCounter; private int cleanupCounter; private int numberOfDeletedNoGoods; @@ -37,6 +38,7 @@ class LearnedNoGoodDeletion { void reset() { learnedNoGoods.clear(); conflictCounter = 0; + totalConflictsCounter = 0; cleanupCounter = 0; numberOfDeletedNoGoods = 0; } @@ -63,6 +65,7 @@ boolean needToRunNoGoodDeletion() { } void runNoGoodDeletion() { + totalConflictsCounter += conflictCounter; conflictCounter = 0; cleanupCounter++; // Reset the sequence after enough growth cycles. @@ -114,4 +117,8 @@ private boolean isLocked(WatchedNoGood noGood, Assignment assignment) { public int getNumberOfDeletedNoGoods() { return numberOfDeletedNoGoods; } + + int getNumTotalConflicts() { + return totalConflictsCounter + conflictCounter; + } } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/MixedRestartStrategy.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/MixedRestartStrategy.java new file mode 100644 index 000000000..058888fdc --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/MixedRestartStrategy.java @@ -0,0 +1,81 @@ +package at.ac.tuwien.kr.alpha.core.solver; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; +import static at.ac.tuwien.kr.alpha.core.solver.NoGoodStore.LBD_NO_VALUE; + +/** + * A restart strategy that mixes dynamic restarts and Luby sequence-based restarts. + * + * Copyright (c) 2019, the Alpha Team. + */ +public class MixedRestartStrategy { + private final LearnedNoGoodDeletion learnedNoGoodDeletion; + + // Variables for dynamic restarts. + private long fast; + private long slow; + private long currentConflictsLimit; + private int numTotalRestarts; + + // Variables for Luby-based restarts. + private int un = 1; + private int vn = 1; + private static final int LUBY_FACTOR = 32; + private int lubyLimit = LUBY_FACTOR; + + + MixedRestartStrategy(LearnedNoGoodDeletion learnedNoGoodDeletion) { + this.learnedNoGoodDeletion = learnedNoGoodDeletion; + reset(); + } + + private void reset() { + fast = 0; + slow = 0; + currentConflictsLimit = 50; + numTotalRestarts = 0; + un = 1; + vn = 1; + } + + boolean shouldRestart() { + long numTotalConflicts = learnedNoGoodDeletion.getNumTotalConflicts(); + return (numTotalConflicts > currentConflictsLimit && fast / 125 > slow / 100) + || numTotalConflicts > lubyLimit; + } + + void onRestart() { + currentConflictsLimit = learnedNoGoodDeletion.getNumTotalConflicts() + 50; + nextLuby(); + numTotalRestarts++; + } + + void newConflictWithLbd(int lbd) { + /// Below is a fast 64-bit fixed point implementation of the following: + // slow += (lbd - slow)/(double)(1<<14); + // fast += (lbd - fast)/(double)(1<<5); + // See Armin Biere's POS'15 slides. + if (lbd == LBD_NO_VALUE) { + throw oops("Conflict has no LBD value."); + } + fast -= fast >> 5; + fast += (long) lbd << (32 - 5); + slow -= slow >> 14; + slow += (long) lbd << (32 - 14); + } + + int getTotalRestarts() { + return numTotalRestarts; + } + + private void nextLuby() { + // Compute Luby-sequence [Knuth'12]-style. + if ((un & -un) == vn) { + un++; + vn = 1; + } else { + vn <<= 1; + } + lubyLimit = vn * LUBY_FACTOR + learnedNoGoodDeletion.getNumTotalConflicts(); + } +} 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..9720eb389 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 @@ -25,28 +25,42 @@ */ package at.ac.tuwien.kr.alpha.core.solver; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.BranchingHeuristic; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.ChainedBranchingHeuristics; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.VSIDSWithPhaseSaving; import org.slf4j.Logger; /** - * Collects performance data (mainly number of decisions per second) and outputs them on demand. + * Collects performance data and outputs them on demand. + * + * Copyright (c) 2019, the Alpha Team. */ public class PerformanceLog { private final ChoiceManager choiceManager; private final TrailAssignment assignment; + private final MixedRestartStrategy restartStrategy; + private final LearnedNoGoodDeletion learnedNoGoodDeletion; + private final BranchingHeuristic branchingHeuristic; private final long msBetweenOutputs; private Long timeFirstEntry; private Long timeLastPerformanceLog; private int numberOfChoicesLastPerformanceLog; + private int numberOfRestartsLastPerformanceLog; + private int numberOfConflictsLastPerformanceLog; + private int numberOfDeletedNoGoodsLastPerformanceLog; /** * @param msBetweenOutputs minimum number of milliseconds that have to pass between writing of performance logs. */ - public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, long msBetweenOutputs) { + public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, MixedRestartStrategy restartStrategy, LearnedNoGoodDeletion learnedNoGoodDeletion, BranchingHeuristic branchingHeuristic, long msBetweenOutputs) { super(); this.choiceManager = choiceManager; this.assignment = assignment; + this.restartStrategy = restartStrategy; + this.learnedNoGoodDeletion = learnedNoGoodDeletion; + this.branchingHeuristic = branchingHeuristic; this.msBetweenOutputs = msBetweenOutputs; } @@ -61,14 +75,51 @@ public void initialize() { */ public void writeIfTimeForLogging(Logger logger) { long currentTime = System.currentTimeMillis(); + if (currentTime < timeLastPerformanceLog + msBetweenOutputs) { + return; + } int currentNumberOfChoices = choiceManager.getChoices(); - if (currentTime >= timeLastPerformanceLog + msBetweenOutputs) { - logger.info("Decisions in {}s: {}", (currentTime - timeLastPerformanceLog) / 1000.0f, currentNumberOfChoices - numberOfChoicesLastPerformanceLog); - timeLastPerformanceLog = currentTime; - numberOfChoicesLastPerformanceLog = currentNumberOfChoices; - float overallTime = (currentTime - timeFirstEntry) / 1000.0f; - float decisionsPerSec = currentNumberOfChoices / overallTime; - logger.info("Overall performance: {} decisions in {}s or {} decisions per sec. Overall replayed assignments: {}.", currentNumberOfChoices, overallTime, decisionsPerSec, assignment.replayCounter); + float timeSinceLastLog = (currentTime - timeLastPerformanceLog) / 1000.0f; + logger.info("Decisions in {}s: {}", timeSinceLastLog, currentNumberOfChoices - numberOfChoicesLastPerformanceLog); + timeLastPerformanceLog = currentTime; + numberOfChoicesLastPerformanceLog = currentNumberOfChoices; + float overallTime = (currentTime - timeFirstEntry) / 1000.0f; + float decisionsPerSec = currentNumberOfChoices / overallTime; + logger.info("Overall performance: {} decisions in {}s or {} decisions per sec. Overall replayed assignments: {}.", currentNumberOfChoices, overallTime, decisionsPerSec, assignment.replayCounter); + if (restartStrategy != null) { + int totalRestarts = restartStrategy.getTotalRestarts(); + int currentNumberOfRestarts = totalRestarts - numberOfRestartsLastPerformanceLog; + logStatsPerTime(logger, "Restarts", timeSinceLastLog, overallTime, totalRestarts, currentNumberOfRestarts); + numberOfRestartsLastPerformanceLog = totalRestarts; + } + if (branchingHeuristic != null && branchingHeuristic instanceof ChainedBranchingHeuristics) { + BranchingHeuristic firstHeuristic = ((ChainedBranchingHeuristics) branchingHeuristic).getFirstElement(); + if (firstHeuristic instanceof VSIDSWithPhaseSaving) { + VSIDSWithPhaseSaving vsidsWithPhaseSaving = (VSIDSWithPhaseSaving) firstHeuristic; + long numThrownAway = vsidsWithPhaseSaving.getNumThrownAway(); + long numNoChoicePoint = vsidsWithPhaseSaving.getNumNoChoicePoint(); + long numNotActiveChoicePoint = vsidsWithPhaseSaving.getNumNotActiveChoicePoint(); + double activityDecrease = vsidsWithPhaseSaving.getActivityDecrease(); + logger.info("Heuristic threw away {} preferred choices ({} no choice, {} not active choice points) averaging {} thrown away per choice done.", numThrownAway, numNoChoicePoint, numNotActiveChoicePoint, (float) numThrownAway / currentNumberOfChoices); + logger.info("HeapOfActiveAtoms had {} choices added due to increased activity.", vsidsWithPhaseSaving.getNumAddedToHeapByActivity()); + logger.info("Atom activity decreased overall by {} or {} per choice on average", activityDecrease, activityDecrease / currentNumberOfChoices); + } + } + if (learnedNoGoodDeletion != null) { + int totalConflicts = learnedNoGoodDeletion.getNumTotalConflicts(); + int currentNumConflicts = totalConflicts - numberOfConflictsLastPerformanceLog; + int totalDeletedNogoods = learnedNoGoodDeletion.getNumberOfDeletedNoGoods(); + int currenDeletedNoGoods = totalDeletedNogoods - numberOfDeletedNoGoodsLastPerformanceLog; + logStatsPerTime(logger, "Conflicts", timeSinceLastLog, overallTime, totalConflicts, currentNumConflicts); + logStatsPerTime(logger, "Deleted NoGoods", timeSinceLastLog, overallTime, totalDeletedNogoods, currenDeletedNoGoods); + numberOfConflictsLastPerformanceLog = totalConflicts; + numberOfDeletedNoGoodsLastPerformanceLog = totalDeletedNogoods; } } + + private void logStatsPerTime(Logger logger, String statName, float timeSinceLastLog, float overallTime, int total, int differenceSinceLast) { + logger.info(statName + " in {}s: {}", timeSinceLastLog, differenceSinceLast); + logger.info("Overall performance: {} " + statName + " in {}s or {} " + statName + " per sec", total, overallTime, total / overallTime); + + } } \ No newline at end of file diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java index e6af12d0a..6e96074a2 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java @@ -1,5 +1,5 @@ -/** - * Copyright (c) 2016-2017, the Alpha Team. +/* + * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * * Additional changes made by Siemens. @@ -33,6 +33,7 @@ import at.ac.tuwien.kr.alpha.core.grounder.Grounder; import at.ac.tuwien.kr.alpha.core.solver.heuristics.HeuristicsConfiguration; import at.ac.tuwien.kr.alpha.core.solver.heuristics.HeuristicsConfigurationBuilder; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.PhaseInitializerFactory; import java.util.Random; @@ -44,7 +45,9 @@ public static Solver getInstance(SystemConfig config, AtomStore atomStore, Groun final Random random = new Random(config.getSeed()); final boolean debugInternalChecks = config.isDebugInternalChecks(); final HeuristicsConfiguration heuristicsConfiguration = buildHeuristicsConfiguration(config); - final WritableAssignment assignment = new TrailAssignment(atomStore, debugInternalChecks); + final PhaseInitializerFactory.PhaseInitializer phaseInitializer = + PhaseInitializerFactory.getInstance(config.getPhaseInitializer(), random, atomStore); + final WritableAssignment assignment = new TrailAssignment(atomStore, phaseInitializer, debugInternalChecks); NoGoodStore store; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java index 9194925d8..2b0834951 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java @@ -27,6 +27,21 @@ */ package at.ac.tuwien.kr.alpha.core.solver; +import at.ac.tuwien.kr.alpha.api.config.SystemConfig; +import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.core.common.Assignment; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; +import at.ac.tuwien.kr.alpha.core.common.IntIterator; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.PhaseInitializerFactory; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; @@ -37,20 +52,6 @@ import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.HashSet; -import java.util.List; -import java.util.Set; - -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; -import at.ac.tuwien.kr.alpha.core.common.Assignment; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.IntIterator; - /** * An implementation of Assignment using a trail (of literals) and arrays as underlying structures for storing * assignments. @@ -79,6 +80,7 @@ public void decreaseActivity() { private final AtomStore atomStore; private ChoiceManager choiceManagerCallback; + private final PhaseInitializerFactory.PhaseInitializer phaseInitializer; /** * Contains for each known atom a value whose two least @@ -91,6 +93,8 @@ public void decreaseActivity() { private int[] strongDecisionLevels; private Antecedent[] impliedBy; private boolean[] callbackUponChange; + private boolean[] phase; + private boolean[] hasPhaseSet; private ArrayList outOfOrderLiterals = new ArrayList<>(); private int highestDecisionLevelContainingOutOfOrderLiterals; private int[] trail = new int[0]; @@ -104,20 +108,23 @@ public void decreaseActivity() { private boolean checksEnabled; long replayCounter; - public TrailAssignment(AtomStore atomStore, boolean checksEnabled) { + public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitializer phaseInitializer, boolean checksEnabled) { + this.phaseInitializer = phaseInitializer; this.checksEnabled = checksEnabled; this.atomStore = atomStore; this.values = new int[0]; this.strongDecisionLevels = new int[0]; this.impliedBy = new Antecedent[0]; this.callbackUponChange = new boolean[0]; + this.phase = new boolean[0]; + this.hasPhaseSet = new boolean[0]; this.trailIndicesOfDecisionLevels.add(0); nextPositionInTrail = 0; newAssignmentsIterator = 0; } public TrailAssignment(AtomStore atomStore) { - this(atomStore, false); + this(atomStore, PhaseInitializerFactory.getInstance(SystemConfig.DEFAULT_PHASE_INITIALIZER, null, atomStore), false); } @Override @@ -127,6 +134,8 @@ public void clear() { Arrays.fill(strongDecisionLevels, -1); Arrays.fill(impliedBy, null); Arrays.fill(callbackUponChange, false); + Arrays.fill(phase, false); + Arrays.fill(hasPhaseSet, false); outOfOrderLiterals = new ArrayList<>(); highestDecisionLevelContainingOutOfOrderLiterals = 0; Arrays.fill(trail, 0); @@ -360,6 +369,8 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent im trail[trailSize++] = atomToLiteral(atom, value.toBoolean()); values[atom] = (getDecisionLevel() << 2) | translateTruth(value); this.impliedBy[atom] = impliedBy; + this.phase[atom] = value.toBoolean(); + this.hasPhaseSet[atom] = true; // Adjust MBT counter. if (value == MBT) { mbtCount++; @@ -463,6 +474,14 @@ public Antecedent getImpliedBy(int atom) { return antecedent; } + @Override + public boolean getLastValue(int atom) { + if (hasPhaseSet[atom]) { + return phase[atom]; + } + return phaseInitializer.getNextInitialPhase(atom); + } + @Override public Set getTrueAssignments() { Set result = new HashSet<>(); @@ -558,6 +577,8 @@ public void growForMaxAtomId() { strongDecisionLevels = Arrays.copyOf(strongDecisionLevels, newCapacity); Arrays.fill(strongDecisionLevels, oldLength, strongDecisionLevels.length, -1); impliedBy = Arrays.copyOf(impliedBy, newCapacity); + phase = Arrays.copyOf(phase, newCapacity); + hasPhaseSet = Arrays.copyOf(hasPhaseSet, newCapacity); callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity); trail = Arrays.copyOf(trail, newCapacity * 2); // Trail has at most 2 assignments (MBT+TRUE) for each atom. } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AbstractVSIDS.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AbstractVSIDS.java new file mode 100644 index 000000000..c6bba298c --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AbstractVSIDS.java @@ -0,0 +1,101 @@ +package at.ac.tuwien.kr.alpha.core.solver.heuristics; + +import at.ac.tuwien.kr.alpha.api.config.BinaryNoGoodPropagationEstimationStrategy; +import at.ac.tuwien.kr.alpha.core.common.Assignment; +import at.ac.tuwien.kr.alpha.core.common.NoGood; +import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.activity.BodyActivityProvider; +import at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner; + +import java.util.ArrayList; +import java.util.Collection; + +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; + +/** + * Combines fields and methods common to several VSIDS variants. + * + * Copyright (c) 2021, the Alpha Team. + */ +public abstract class AbstractVSIDS implements ActivityBasedBranchingHeuristic { + protected static final int DEFAULT_DECAY_PERIOD = 1; + /** + * The default factor by which VSID's activity increment will be multiplied when the decay period has expired. + * The value is taken from clasp's tweety configuration which clasp uses by default. + */ + protected static final double DEFAULT_DECAY_FACTOR = 1 / 0.92; + protected final Assignment assignment; + protected final ChoiceManager choiceManager; + protected final HeapOfActiveAtoms heapOfActiveAtoms; + protected final Collection bufferedNoGoods = new ArrayList<>(); + + public AbstractVSIDS(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { + this.assignment = assignment; + this.choiceManager = choiceManager; + this.heapOfActiveAtoms = heapOfActiveAtoms; + this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy); + } + + public void growForMaxAtomId(int maxAtomId) { + heapOfActiveAtoms.growForMaxAtomId(maxAtomId); + } + + @Override + public void violatedNoGood(NoGood violatedNoGood) { + } + + @Override + public void newNoGood(NoGood newNoGood) { + bufferedNoGoods.add(newNoGood); + } + + @Override + public void newNoGoods(Collection newNoGoods) { + bufferedNoGoods.addAll(newNoGoods); + } + + protected void ingestBufferedNoGoods() { + heapOfActiveAtoms.newNoGoods(bufferedNoGoods); + bufferedNoGoods.clear(); + } + + /** + * {@link VSIDS} manages a stack of nogoods in the fashion of {@link BerkMin} + * and starts by looking at the most active atom a in the nogood currently at the top of the stack. + * If a is an active choice point (i.e. representing the body of an applicable rule), it is immediately chosen; + * else the most active choice point dependent on a is. + * If there is no such atom, we continue further down the stack. + * When choosing between dependent atoms, a {@link BodyActivityProvider} is employed to define the activity of a choice point. + */ + @Override + public int chooseLiteral() { + int atom = chooseAtom(); + if (atom == DEFAULT_CHOICE_ATOM) { + return DEFAULT_CHOICE_LITERAL; + } + boolean sign = chooseSign(atom); + return atomToLiteral(atom, sign); + } + + @Override + public void analyzedConflict(GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult) { + ingestBufferedNoGoods(); // The analysisResult may contain new atoms whose activity must be initialized. + for (int resolutionAtom : analysisResult.resolutionAtoms) { + incrementActivityResolutionAtom(resolutionAtom); + } + if (analysisResult.learnedNoGood != null) { + for (int literal : analysisResult.learnedNoGood) { + incrementActivityLearnedNoGood(literal); + } + } + heapOfActiveAtoms.decayIfTimeHasCome(); + } + + protected abstract void incrementActivityLearnedNoGood(int literal); + + protected abstract void incrementActivityResolutionAtom(int resolutionAtom); + + protected abstract int chooseAtom(); + + protected abstract boolean chooseSign(int atom); +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java index b14bc9d1e..cdd0362e0 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java @@ -36,6 +36,8 @@ import java.util.Set; import java.util.stream.Stream; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; + /** * A variant of {@link DependencyDrivenHeuristic} that prefers to choose atoms representing bodies of rules whose heads * are assigned {@link at.ac.tuwien.kr.alpha.core.solver.ThriceTruth#MBT}. @@ -60,7 +62,7 @@ public int chooseLiteral() { .max(Comparator.comparingDouble(bodyActivity::get)); if (mostActiveBody.isPresent()) { rememberedAtom = mostActiveBody.get(); - return rememberedAtom; + return atomToLiteral(rememberedAtom); } return super.chooseLiteral(); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristicFactory.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristicFactory.java index 29f995071..bfb24fcea 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristicFactory.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/BranchingHeuristicFactory.java @@ -29,6 +29,7 @@ import java.util.Random; import at.ac.tuwien.kr.alpha.core.grounder.Grounder; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.core.solver.WritableAssignment; import at.ac.tuwien.kr.alpha.core.solver.heuristics.activity.BodyActivityProviderFactory.BodyActivityType; @@ -86,6 +87,9 @@ private static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfigurati return new VSIDS(assignment, choiceManager, heuristicsConfiguration.getMomsStrategy()); case GDD_VSIDS: return new DependencyDrivenVSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); + case VSIDS_PHASE_SAVING: + AtomChoiceRelation atomChoiceRelation = grounder.getAtomChoiceRelation(); + return new VSIDSWithPhaseSaving(assignment, choiceManager, atomChoiceRelation, heuristicsConfiguration.getMomsStrategy()); } throw new IllegalArgumentException("Unknown branching heuristic requested."); } 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..4f2caf96f 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 @@ -98,6 +98,10 @@ public void add(BranchingHeuristic element) { } } + public BranchingHeuristic getFirstElement() { + return chain.get(0); + } + public BranchingHeuristic getLastElement() { return chain.get(chain.size() - 1); } 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 94421084f..7f0afcbfa 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 @@ -36,6 +36,7 @@ import org.slf4j.LoggerFactory; import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; import java.util.Arrays; import java.util.Collection; @@ -45,32 +46,36 @@ /** * Manages a heap of atoms that are assigned an activity, such that the most active atom * resides at the top of the heap. - * In contrast to standard heuristics like VSIDS, activities are not periodically decayed but - * the increment added when increasing activities is constantly increased itself, which has the + * Activities are not periodically decayed but an increasing increment is added for each updated activity, which has the * same effect. * + * The heap contains only (once-active) choice atoms, i.e., the heap may contain choice points that are currently + * inactive but once were active. + * */ public class HeapOfActiveAtoms { protected static final Logger LOGGER = LoggerFactory.getLogger(HeapOfActiveAtoms.class); private static final double NORMALIZATION_THRESHOLD = 1E100; private static final double INCREMENT_TO_AVOID_DENORMALS = Double.MIN_VALUE * NORMALIZATION_THRESHOLD; - private static final double SCORE_EPSILON = 1E-100; + static final double SCORE_EPSILON = 1E-100; - private boolean[] incrementedActivityScores = new boolean[0]; - protected double[] activityScores = new double[0]; - protected final PriorityQueue heap = new PriorityQueue<>(new AtomActivityComparator().reversed()); + boolean[] incrementedActivityScores = new boolean[0]; + private boolean[] occursInHeap = new boolean[0]; // Stores whether an atom is currently in the heap (or a left-over duplicate). + double[] activityScores = new double[0]; + final PriorityQueue heap = new PriorityQueue<>(new AtomActivityComparator().reversed()); protected ChoiceManager choiceManager; private int decayPeriod; private double decayFactor; private int stepsSinceLastDecay; private double currentActivityIncrement = 1.0; - private int numberOfNormalizations; + int numberOfNormalizations; + private long numAddedToHeapByActivity; - private final MOMs moms; + final MOMs moms; - public HeapOfActiveAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager) { + HeapOfActiveAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager) { this.decayPeriod = decayPeriod; this.decayFactor = decayFactor; this.choiceManager = choiceManager; @@ -104,6 +109,10 @@ public double getDecayFactor() { return decayFactor; } + double getCurrentActivityIncrement() { + return currentActivityIncrement; + } + /** * @see #getDecayFactor() */ @@ -146,7 +155,7 @@ protected void analyzeNewNoGood(NoGood newNoGood) { /** * Computes and stores initial activity values for the atoms occurring in the given nogood. */ - protected void initActivity(NoGood newNoGood) { + private void initActivity(NoGood newNoGood) { if (moms != null) { initActivityMOMs(newNoGood); } else { @@ -161,7 +170,7 @@ protected void initActivity(NoGood newNoGood) { * 1.01 is added to avoid computing the logarithm of a number between 0 and 1 (input scores have to be greater or equal to 0!) * @param newNoGood a new nogood, the atoms occurring in which will be initialized */ - private void initActivityMOMs(NoGood newNoGood) { + protected void initActivityMOMs(NoGood newNoGood) { LOGGER.debug("Initializing activity scores with MOMs"); for (int literal : newNoGood) { int atom = atomOf(literal); @@ -183,6 +192,19 @@ private void initActivityMOMs(NoGood newNoGood) { void growToCapacity(int newCapacity) { activityScores = Arrays.copyOf(activityScores, newCapacity); incrementedActivityScores = Arrays.copyOf(incrementedActivityScores, newCapacity); + occursInHeap = Arrays.copyOf(occursInHeap, newCapacity); + } + + void growForMaxAtomId(int maxAtomId) { + // Grow arrays only if needed. + if (activityScores.length > maxAtomId) { + return; + } + int newCapacity = arrayGrowthSize(activityScores.length); + if (newCapacity < maxAtomId + 1) { + newCapacity = maxAtomId + 1; + } + growToCapacity(newCapacity); } private void initActivityNaive(NoGood newNoGood) { @@ -196,8 +218,18 @@ private void initActivityNaive(NoGood newNoGood) { /** * Returns the atom with the highest activity score and removes it from the heap. */ - public Integer getMostActiveAtom() { - return heap.poll(); + Integer getMostActiveAtom() { + Integer mostActiveAtom; + // Here we lazily remove atoms from the heap that were once added and had their activity increased + // (which creates a duplicate entry in the heap). + // Remove the topmost atom from the heap until non-duplicate one is obtained. + do { + mostActiveAtom = heap.poll(); + } while (mostActiveAtom != null && !occursInHeap[mostActiveAtom]); + if (mostActiveAtom != null) { + occursInHeap[mostActiveAtom] = false; + } + return mostActiveAtom; } /** @@ -206,7 +238,7 @@ public Integer getMostActiveAtom() { * by adding to it the current activity increment times the increment factor. * If the new value exceeds a certain threshold, all activity scores are normalized. */ - public void incrementActivity(int atom) { + void incrementActivity(int atom) { incrementActivity(atom, currentActivityIncrement); } @@ -217,7 +249,7 @@ protected void incrementActivity(int atom, double increment) { incrementedActivityScores[atom] = true; } - private void setActivity(int atom, double newActivity) { + void setActivity(int atom, double newActivity) { activityScores[atom] = newActivity; if (LOGGER.isTraceEnabled()) { LOGGER.trace("Activity of atom {} set to {}", atom, newActivity); @@ -227,7 +259,10 @@ private void setActivity(int atom, double newActivity) { normalizeActivityScores(); } - heap.add(atom); // ignores the fact that atom may already be in the heap for performance reasons (may be revised in future) + if (occursInHeap[atom]) { + numAddedToHeapByActivity++; + heap.add(atom); // For performance reason ignores that the atom may already be in the heap. + } } /** @@ -244,13 +279,17 @@ private void normalizeActivityScores() { } } - private double normalizeNewActivityScore(double newActivity) { + double normalizeNewActivityScore(double newActivity) { for (int i = 0; i < numberOfNormalizations; i++) { newActivity = (newActivity + INCREMENT_TO_AVOID_DENORMALS) / NORMALIZATION_THRESHOLD; } return newActivity; } + long getNumAddedToHeapByActivity() { + return numAddedToHeapByActivity; + } + private class AtomActivityComparator implements Comparator { @Override @@ -263,19 +302,15 @@ public int compare(Integer a1, Integer a2) { private class ChoicePointActivityListener implements ChoiceInfluenceManager.ActivityListener { @Override - public void callbackOnChanged(int atom, boolean active) { - if (active && choiceManager.isActiveChoiceAtom(atom)) { - if (atom < activityScores.length) { - /* if atom has no activity score, probably the atom is still being buffered - by DependencyDrivenVSIDSHeuristic and will get an initial activity - when the buffer is ingested */ - heap.add(atom); - } + public void callbackOnChange(int atom) { + if (!occursInHeap[atom]) { + occursInHeap[atom] = true; + heap.add(atom); } } } - public void setMOMsStrategy(BinaryNoGoodPropagationEstimationStrategy momsStrategy) { + void setMOMsStrategy(BinaryNoGoodPropagationEstimationStrategy momsStrategy) { if (moms != null) { moms.setStrategy(momsStrategy); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfRelatedChoiceAtoms.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfRelatedChoiceAtoms.java new file mode 100644 index 000000000..48675b412 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/HeapOfRelatedChoiceAtoms.java @@ -0,0 +1,42 @@ +package at.ac.tuwien.kr.alpha.core.solver.heuristics; + +import at.ac.tuwien.kr.alpha.core.common.NoGood; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; +import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; + +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; + +/** + * A heap of active choice points that uses {@link AtomChoiceRelation} for initializing activities of related choice points. + * + * Copyright (c) 2019, the Alpha Team. + */ +public class HeapOfRelatedChoiceAtoms extends HeapOfActiveAtoms { + private final AtomChoiceRelation atomChoiceRelation; + + HeapOfRelatedChoiceAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation) { + super(decayPeriod, decayFactor, choiceManager); + this.atomChoiceRelation = atomChoiceRelation; + } + + @Override + protected void initActivityMOMs(NoGood newNoGood) { + LOGGER.debug("Initializing activity scores with MOMs"); + for (int literal : newNoGood) { + for (Integer relatedChoiceAtom : atomChoiceRelation.getRelatedChoiceAtoms(atomOf(literal))) { + if (!incrementedActivityScores[relatedChoiceAtom]) { // update initial value as long as not incremented yet by VSIDS + double score = moms.getScore(relatedChoiceAtom); + if (score > 0.0) { + double newActivity = 1 - 1 / (Math.log(score + 1.01)); + if (newActivity - activityScores[relatedChoiceAtom] > SCORE_EPSILON) { // avoid computation overhead if score does not increase + if (numberOfNormalizations > 0) { + newActivity = normalizeNewActivityScore(newActivity); + } + setActivity(relatedChoiceAtom, newActivity); + } + } + } + } + } + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/PhaseInitializerFactory.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/PhaseInitializerFactory.java new file mode 100644 index 000000000..4398c3026 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/PhaseInitializerFactory.java @@ -0,0 +1,99 @@ +/* + * Copyright (c) 2019-2020, the Alpha Team. + * All rights reserved. + * + * Additional changes made by Siemens. + * + * 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 + * 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.heuristics; + +import at.ac.tuwien.kr.alpha.api.config.InitialAtomPhase; +import at.ac.tuwien.kr.alpha.core.atoms.RuleAtom; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; + +import java.util.Random; + +/** + * Factory returning atom phase initializers, which determine the initial phase given to atoms that were previously + * unassigned. + * + * Copyright (c) 2019, the Alpha Team. + */ +public abstract class PhaseInitializerFactory { + + public abstract static class PhaseInitializer { + public abstract boolean getNextInitialPhase(int atom); + } + + public static PhaseInitializer getInstance(InitialAtomPhase initialPhase, Random random, AtomStore atomStore) { + switch (initialPhase) { + case ALLTRUE: + return getPhaseInitializerAllTrue(); + case ALLFALSE: + return getPhaseInitializerAllFalse(); + case RANDOM: + return getPhaseInitializerRandom(random); + case RULESTRUEATOMSFALSE: + return getPhaseInitializerRulesTrueRestFalse(atomStore); + default: + throw new IllegalArgumentException("Unknown phase initializer requested:" + initialPhase); + } + } + + private static PhaseInitializer getPhaseInitializerAllTrue() { + return new PhaseInitializer() { + @Override + public boolean getNextInitialPhase(int atom) { + return true; + } + }; + } + + private static PhaseInitializer getPhaseInitializerAllFalse() { + return new PhaseInitializer() { + @Override + public boolean getNextInitialPhase(int atom) { + return false; + } + }; + } + + private static PhaseInitializer getPhaseInitializerRandom(Random random) { + return new PhaseInitializer() { + private final Random rand = random; + @Override + public boolean getNextInitialPhase(int atom) { + return rand.nextBoolean(); + } + }; + } + + private static PhaseInitializer getPhaseInitializerRulesTrueRestFalse(AtomStore atomStore) { + return new PhaseInitializer() { + @Override + public boolean getNextInitialPhase(int atom) { + return atomStore.get(atom) instanceof RuleAtom; // Return true for RuleAtoms, otherwise false. + } + }; + } +} 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 bb29d6e14..423c1af36 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 @@ -25,27 +25,18 @@ */ package at.ac.tuwien.kr.alpha.core.solver.heuristics; -import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; -import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; -import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; -import static at.ac.tuwien.kr.alpha.core.atoms.Literals.isPositive; - -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collection; - -import org.apache.commons.collections4.MultiValuedMap; -import org.apache.commons.collections4.multimap.HashSetValuedHashMap; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - import at.ac.tuwien.kr.alpha.api.config.BinaryNoGoodPropagationEstimationStrategy; import at.ac.tuwien.kr.alpha.core.common.Assignment; -import at.ac.tuwien.kr.alpha.core.common.NoGood; import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; -import at.ac.tuwien.kr.alpha.core.solver.heuristics.activity.BodyActivityProvider; -import at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.Arrays; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.isPositive; /** * This implementation is inspired by the VSIDS implementation in clasp. @@ -61,39 +52,15 @@ * Chaff: engineering an efficient SAT solver. * In: Proceedings of the 38th Design Automation Conference. IEEE, pp. 530–535. */ -public class VSIDS implements ActivityBasedBranchingHeuristic { +public class VSIDS extends AbstractVSIDS { protected static final Logger LOGGER = LoggerFactory.getLogger(VSIDS.class); - public static final int DEFAULT_DECAY_PERIOD = 1; - - /** - * The default factor by which VSID's activity increment will be multiplied when the decay period has expired. - * The value is taken from clasp's tweety configuration which clasp uses by default. - */ - public static final double DEFAULT_DECAY_FACTOR = 1 / 0.92; - - protected final Assignment assignment; - protected final ChoiceManager choiceManager; - - protected final HeapOfActiveAtoms heapOfActiveAtoms; protected int[] signBalances = new int[0]; - - private final Collection bufferedNoGoods = new ArrayList<>(); - private int nChoicesTrue; private int nChoicesFalse; - private int nChoicesRand; - - /** - * Maps rule heads to atoms representing corresponding bodies. - */ - protected final MultiValuedMap headToBodies = new HashSetValuedHashMap<>(); protected VSIDS(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { - this.assignment = assignment; - this.choiceManager = choiceManager; - this.heapOfActiveAtoms = heapOfActiveAtoms; - this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy); + super(assignment, choiceManager, heapOfActiveAtoms, momsStrategy); } public VSIDS(Assignment assignment, ChoiceManager choiceManager, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { @@ -105,57 +72,17 @@ public VSIDS(Assignment assignment, ChoiceManager choiceManager, BinaryNoGoodPro } @Override - public void violatedNoGood(NoGood violatedNoGood) { - } - - @Override - public void analyzedConflict(ConflictAnalysisResult analysisResult) { - ingestBufferedNoGoods(); //analysisResult may contain new atoms whose activity must be initialized - for (int resolutionAtom : analysisResult.resolutionAtoms) { - heapOfActiveAtoms.incrementActivity(resolutionAtom); - } - if (analysisResult.learnedNoGood != null) { - for (int literal : analysisResult.learnedNoGood) { - incrementSignCounter(literal); - heapOfActiveAtoms.incrementActivity(atomOf(literal)); - } - } - heapOfActiveAtoms.decayIfTimeHasCome(); - } - - @Override - public void newNoGood(NoGood newNoGood) { - this.bufferedNoGoods.add(newNoGood); + protected void incrementActivityResolutionAtom(int resolutionAtom) { + heapOfActiveAtoms.incrementActivity(resolutionAtom); } @Override - public void newNoGoods(Collection newNoGoods) { - this.bufferedNoGoods.addAll(newNoGoods); + protected void incrementActivityLearnedNoGood(int literal) { + incrementSignCounter(literal); + heapOfActiveAtoms.incrementActivity(atomOf(literal)); } - private void ingestBufferedNoGoods() { - heapOfActiveAtoms.newNoGoods(bufferedNoGoods); - bufferedNoGoods.clear(); - } - - /** - * {@link VSIDS} manages a stack of nogoods in the fashion of {@link BerkMin} - * and starts by looking at the most active atom a in the nogood currently at the top of the stack. - * If a is an active choice point (i.e. representing the body of an applicable rule), it is immediately chosen; - * else the most active choice point dependent on a is. - * If there is no such atom, we continue further down the stack. - * When choosing between dependent atoms, a {@link BodyActivityProvider} is employed to define the activity of a choice point. - */ @Override - public int chooseLiteral() { - int atom = chooseAtom(); - if (atom == DEFAULT_CHOICE_ATOM) { - return DEFAULT_CHOICE_LITERAL; - } - boolean sign = chooseSign(atom); - return atomToLiteral(atom, sign); - } - protected int chooseAtom() { ingestBufferedNoGoods(); Integer mostActiveAtom; @@ -181,6 +108,7 @@ protected int chooseAtom() { * the chosen atom * @return the truth value to assign to the given atom */ + @Override protected boolean chooseSign(int atom) { atom = getAtomForChooseSign(atom); @@ -189,8 +117,8 @@ protected boolean chooseSign(int atom) { } int signBalance = getSignBalance(atom); - if (LOGGER.isDebugEnabled() && (nChoicesFalse + nChoicesTrue + nChoicesRand) % 100 == 0) { - LOGGER.debug("chooseSign stats: f={}, t={}, r={}", nChoicesFalse, nChoicesTrue, nChoicesRand); + if (LOGGER.isDebugEnabled() && (nChoicesFalse + nChoicesTrue) % 100 == 0) { + LOGGER.debug("chooseSign stats: f={}, t={}", nChoicesFalse, nChoicesTrue); LOGGER.debug("chooseSign stats: signBalance={}", signBalance); } @@ -212,7 +140,7 @@ protected int getAtomForChooseSign(int atom) { return atom; } - protected void incrementSignCounter(int literal) { + private void incrementSignCounter(int literal) { int atom = atomOf(literal); boolean sign = isPositive(literal); growForMaxAtomId(atom); @@ -225,13 +153,13 @@ public void growForMaxAtomId(int maxAtomId) { if (signBalances.length > maxAtomId) { return; } + super.growForMaxAtomId(maxAtomId); // Grow to default size, except if bigger array is required due to maxAtomId. int newCapacity = arrayGrowthSize(signBalances.length); if (newCapacity < maxAtomId + 1) { newCapacity = maxAtomId + 1; } signBalances = Arrays.copyOf(signBalances, newCapacity); - heapOfActiveAtoms.growToCapacity(newCapacity); } @Override diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDSWithPhaseSaving.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDSWithPhaseSaving.java new file mode 100644 index 000000000..40c9b97f6 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/heuristics/VSIDSWithPhaseSaving.java @@ -0,0 +1,145 @@ +package at.ac.tuwien.kr.alpha.core.solver.heuristics; + +import at.ac.tuwien.kr.alpha.api.config.BinaryNoGoodPropagationEstimationStrategy; +import at.ac.tuwien.kr.alpha.core.common.Assignment; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; +import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager; +import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; + +/** + * This implementation is similar to {@link VSIDS} but uses the saved phase for the truth of the chosen atom. + * + * Copyright (c) 2019-2021, the Alpha Team. + */ +public class VSIDSWithPhaseSaving extends AbstractVSIDS { + protected static final Logger LOGGER = LoggerFactory.getLogger(VSIDSWithPhaseSaving.class); + + private final AtomChoiceRelation atomChoiceRelation; + private double activityDecrease; + private long numThrownAway; + private long numNoChoicePoint; + private long numNotActiveChoicePoint; + + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { + super(assignment, choiceManager, heapOfActiveAtoms, momsStrategy); + this.atomChoiceRelation = atomChoiceRelation; + } + + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { + this(assignment, choiceManager, atomChoiceRelation, new HeapOfRelatedChoiceAtoms(decayPeriod, decayFactor, choiceManager, atomChoiceRelation), momsStrategy); + } + + VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { + this(assignment, choiceManager, atomChoiceRelation, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR, momsStrategy); + } + + @Override + protected void incrementActivityResolutionAtom(int resolutionAtom) { + incrementActivityOfRelatedChoiceAtoms(resolutionAtom); + } + + @Override + protected void incrementActivityLearnedNoGood(int literal) { + incrementActivityOfRelatedChoiceAtoms(atomOf(literal)); + } + + private void incrementActivityOfRelatedChoiceAtoms(int toAtom) { + if (atomChoiceRelation == null) { + heapOfActiveAtoms.incrementActivity(toAtom); + throw new RuntimeException("Condition met: atomChoiceRelation is null."); + } + for (Integer relatedChoiceAtom : atomChoiceRelation.getRelatedChoiceAtoms(toAtom)) { + if (!choiceManager.isAtomChoice(relatedChoiceAtom)) { + throw oops("Related atom is no choice."); + } + heapOfActiveAtoms.incrementActivity(relatedChoiceAtom); + } + } + + public double getActivityDecrease() { + return activityDecrease; + } + + public long getNumThrownAway() { + return numThrownAway; + } + + public long getNumNoChoicePoint() { + return numNoChoicePoint; + } + + public long getNumNotActiveChoicePoint() { + return numNotActiveChoicePoint; + } + + public long getNumAddedToHeapByActivity() { + return heapOfActiveAtoms.getNumAddedToHeapByActivity(); + } + + @Override + protected int chooseAtom() { + ingestBufferedNoGoods(); + Integer mostActiveAtom; + double maxActivity = 0.0f; + while ((mostActiveAtom = heapOfActiveAtoms.getMostActiveAtom()) != null) { + double activity = heapOfActiveAtoms.getActivity(atomToLiteral(mostActiveAtom)); + if (activity > maxActivity) { + maxActivity = activity; + } + if (choiceManager.isActiveChoiceAtom(mostActiveAtom)) { + if (maxActivity > activity) { + double lostActivityNormalized = (maxActivity - activity) / heapOfActiveAtoms.getCurrentActivityIncrement(); + activityDecrease += lostActivityNormalized; + } + return mostActiveAtom; + } + if (choiceManager.isAtomChoice(mostActiveAtom)) { + numNotActiveChoicePoint++; + } else { + numNoChoicePoint++; + } + numThrownAway++; + } + return DEFAULT_CHOICE_ATOM; + } + + /** + * Chooses a sign (truth value) to assign to the given atom; + * uses the last value (saved phase) to determine its truth value. + * + * @param atom + * the chosen atom + * @return the truth value to assign to the given atom + */ + @Override + protected boolean chooseSign(int atom) { + if (assignment.getTruth(atom) == ThriceTruth.MBT) { + return true; + } + return assignment.getLastValue(atom); + } + + public void growForMaxAtomId(int maxAtomId) { + super.growForMaxAtomId(maxAtomId); + if (atomChoiceRelation != null) { + atomChoiceRelation.growForMaxAtomId(maxAtomId); + } + } + + @Override + public double getActivity(int literal) { + return heapOfActiveAtoms.getActivity(literal); + } + + @Override + public String toString() { + return this.getClass().getSimpleName(); + } + +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java index 66374d312..d98c46380 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java @@ -66,6 +66,7 @@ import at.ac.tuwien.kr.alpha.core.rules.BasicRule; import at.ac.tuwien.kr.alpha.core.rules.InternalRule; import at.ac.tuwien.kr.alpha.core.rules.NormalRuleImpl; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; /** * Represents a small ASP program with choices {@code { aa :- not bb. bb :- not aa. }}. @@ -124,6 +125,7 @@ public class ChoiceGrounder implements Grounder { private static Atom atomEnBR2 = ChoiceAtom.on(2); private static Atom atomDisBR1 = ChoiceAtom.off(3); private static Atom atomDisBR2 = ChoiceAtom.off(4); + private static AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation(); private final AtomStore atomStore; private boolean returnedAllNogoods; @@ -137,6 +139,11 @@ public ChoiceGrounder(AtomStore atomStore, java.util.function.Predicate solverDerivedNoGoods = new HashMap<>(); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java index 669e6037f..ce1b24bff 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java @@ -65,6 +65,7 @@ import at.ac.tuwien.kr.alpha.core.rules.BasicRule; import at.ac.tuwien.kr.alpha.core.rules.InternalRule; import at.ac.tuwien.kr.alpha.core.rules.NormalRuleImpl; +import at.ac.tuwien.kr.alpha.core.grounder.structure.AtomChoiceRelation; /** * Represents a small ASP program {@code { c :- a, b. a. b. }}. @@ -96,6 +97,7 @@ public class DummyGrounder implements Grounder { private static BasicAtom atomCC = Atoms.newBasicAtom(Predicates.getPredicate("c", 0)); private static BasicRule ruleABC = new BasicRule(Heads.newNormalHead(atomCC), Arrays.asList(atomAA.toLiteral(), atomBB.toLiteral())); private static Atom rule1 = new RuleAtom(InternalRule.fromNormalRule(NormalRuleImpl.fromBasicRule(ruleABC)), new BasicSubstitution()); + private static AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation(); private Set returnedNogoods = new HashSet<>(); public DummyGrounder(AtomStore atomStore) { @@ -126,6 +128,11 @@ public int register(NoGood noGood) { return solverDerivedNoGoods.get(noGood); } + @Override + public AtomChoiceRelation getAtomChoiceRelation() { + return atomChoiceRelation; + } + @Override public AnswerSet assignmentToAnswerSet(Iterable trueAtoms) { // Note: This grounder only deals with 0-ary predicates, i.e., every atom is a predicate and there is