From 8b69a7ad6484bdff6686bfe607ca0eb5603ac8d8 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 30 Sep 2019 00:50:32 +0200 Subject: [PATCH 01/27] Add phase saving. - Assignment provides getLastValue (i.e. phase). - VSIDSWithPhaseSaving is VSIDS but uses saved phase from Assignment. - BranchingHeuristicFactory knows new VSIDSWithPhaseSaving heuristics. - HeapOfActiveAtoms polished, growForMaxAtomId added. - TrailAssignment saves the phase (last truth value) of variables. --- .../ac/tuwien/kr/alpha/common/Assignment.java | 7 + .../tuwien/kr/alpha/solver/DefaultSolver.java | 2 +- .../kr/alpha/solver/TrailAssignment.java | 12 +- .../heuristics/BranchingHeuristicFactory.java | 5 +- .../solver/heuristics/HeapOfActiveAtoms.java | 28 ++- .../heuristics/VSIDSWithPhaseSaving.java | 168 ++++++++++++++++++ 6 files changed, 212 insertions(+), 10 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java index 638696fce..04fdc8288 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java @@ -71,6 +71,13 @@ default ThriceTruth getTruth(int atom) { */ Antecedent getImpliedBy(int atom); + /** + * Returns the last truth value (i.e., phase) assigned to the atom. + * @param atom the atom + * @return the last truth value. + */ + boolean getLastValue(int atom); + /** * Determines if the given {@code noGood} is undefined in the current assignment. * diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java index 2ee2b11d4..91074801d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java @@ -281,7 +281,7 @@ private boolean justifyMbtAndBacktrack() { } ProgramAnalyzingGrounder analyzingGrounder = (ProgramAnalyzingGrounder) grounder; // Justify one MBT assigned atom. - Integer atomToJustify = assignment.getBasicAtomAssignedMBT(); + int atomToJustify = assignment.getBasicAtomAssignedMBT(); if (LOGGER.isDebugEnabled()) { LOGGER.debug("Searching for justification of {} / {}", atomToJustify, atomStore.atomToString(atomToJustify)); LOGGER.debug("Assignment is (TRUE part only): {}", translate(assignment.getTrueAssignments())); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java index 9c4640d01..d76166a7e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java @@ -49,7 +49,7 @@ */ public class TrailAssignment implements WritableAssignment, Checkable { private static final Logger LOGGER = LoggerFactory.getLogger(TrailAssignment.class); - public static final Antecedent CLOSING_INDICATOR_ANTECEDENT = new Antecedent() { + static final Antecedent CLOSING_INDICATOR_ANTECEDENT = new Antecedent() { int[] literals = new int[0]; @Override @@ -81,6 +81,7 @@ public void decreaseActivity() { private int[] strongDecisionLevels; private Antecedent[] impliedBy; private boolean[] callbackUponChange; + private boolean[] phase; private ArrayList outOfOrderLiterals = new ArrayList<>(); private int highestDecisionLevelContainingOutOfOrderLiterals; private ArrayList trail = new ArrayList<>(); @@ -101,6 +102,7 @@ public TrailAssignment(AtomStore atomStore, boolean checksEnabled) { this.strongDecisionLevels = new int[0]; this.impliedBy = new Antecedent[0]; this.callbackUponChange = new boolean[0]; + this.phase = new boolean[0]; this.trailIndicesOfDecisionLevels.add(0); nextPositionInTrail = 0; newAssignmentsIterator = 0; @@ -119,6 +121,7 @@ public void clear() { Arrays.fill(strongDecisionLevels, -1); Arrays.fill(impliedBy, null); Arrays.fill(callbackUponChange, false); + Arrays.fill(phase, false); outOfOrderLiterals = new ArrayList<>(); highestDecisionLevelContainingOutOfOrderLiterals = 0; trail = new ArrayList<>(); @@ -353,6 +356,7 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent im trail.add(atomToLiteral(atom, value.toBoolean())); values[atom] = (getDecisionLevel() << 2) | translateTruth(value); this.impliedBy[atom] = impliedBy; + this.phase[atom] = value.toBoolean(); // Adjust MBT counter. if (value == MBT) { mbtCount++; @@ -445,6 +449,11 @@ public Antecedent getImpliedBy(int atom) { return impliedBy[atom]; } + @Override + public boolean getLastValue(int atom) { + return phase[atom]; + } + @Override public Set getTrueAssignments() { Set result = new HashSet<>(); @@ -533,6 +542,7 @@ 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); callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java index b54cfdd53..740e016fd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java @@ -56,7 +56,8 @@ public enum Heuristic { ALPHA_ACTIVE_RULE, ALPHA_HEAD_MBT, VSIDS, - GDD_VSIDS; + GDD_VSIDS, + VSIDS_PHASE_SAVING; /** * @return a comma-separated list of names of known heuristics @@ -117,6 +118,8 @@ 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: + return new VSIDSWithPhaseSaving(assignment, choiceManager, heuristicsConfiguration.getMomsStrategy()); } throw new IllegalArgumentException("Unknown branching heuristic requested."); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java index 5ff32fc06..56db8f727 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java @@ -38,6 +38,7 @@ import java.util.Comparator; import java.util.PriorityQueue; +import static at.ac.tuwien.kr.alpha.Util.arrayGrowthSize; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; /** @@ -56,8 +57,8 @@ public class HeapOfActiveAtoms { private 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()); + private double[] activityScores = new double[0]; + final PriorityQueue heap = new PriorityQueue<>(new AtomActivityComparator().reversed()); protected ChoiceManager choiceManager; private int decayPeriod; @@ -68,7 +69,7 @@ public class HeapOfActiveAtoms { private 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; @@ -144,7 +145,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 { @@ -183,6 +184,19 @@ void growToCapacity(int newCapacity) { incrementedActivityScores = Arrays.copyOf(incrementedActivityScores, 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; + } + activityScores = Arrays.copyOf(activityScores, newCapacity); + incrementedActivityScores = Arrays.copyOf(incrementedActivityScores, newCapacity); + } + private void initActivityNaive(NoGood newNoGood) { LOGGER.debug("Initializing activity scores naively"); for (Integer literal : newNoGood) { @@ -194,7 +208,7 @@ private void initActivityNaive(NoGood newNoGood) { /** * Returns the atom with the highest activity score and removes it from the heap. */ - public Integer getMostActiveAtom() { + Integer getMostActiveAtom() { return heap.poll(); } @@ -204,7 +218,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); } @@ -271,7 +285,7 @@ public void callbackOnChanged(int atom, boolean active) { } } - public void setMOMsStrategy(BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + void setMOMsStrategy(BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { if (moms != null) { moms.setStrategy(momsStrategy); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java new file mode 100644 index 000000000..80512659d --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -0,0 +1,168 @@ +/** + * Copyright (c) 2018-2019 Siemens AG + * All rights reserved. + * + * 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.solver.heuristics; + +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; +import at.ac.tuwien.kr.alpha.solver.ChoiceManager; +import at.ac.tuwien.kr.alpha.solver.ThriceTruth; +import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Collection; + +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; + +/** + * This implementation is like {@link VSIDS} but uses the saved phase for the truth of the chosen atom. + * + * Copyright (c) 2019, the Alpha Team. + */ +public class VSIDSWithPhaseSaving implements ActivityBasedBranchingHeuristic { + protected static final Logger LOGGER = LoggerFactory.getLogger(VSIDSWithPhaseSaving.class); + + private 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. + */ + private static final double DEFAULT_DECAY_FACTOR = 1 / 0.92; + + protected final Assignment assignment; + protected final ChoiceManager choiceManager; + + private final HeapOfActiveAtoms heapOfActiveAtoms; + + private final Collection bufferedNoGoods = new ArrayList<>(); + + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + this.assignment = assignment; + this.choiceManager = choiceManager; + this.heapOfActiveAtoms = heapOfActiveAtoms; + this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy); + } + + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + this(assignment, choiceManager, new HeapOfActiveAtoms(decayPeriod, decayFactor, choiceManager), momsStrategy); + } + + VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + this(assignment, choiceManager, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR, momsStrategy); + } + + @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) { + heapOfActiveAtoms.incrementActivity(atomOf(literal)); + } + } + heapOfActiveAtoms.decayIfTimeHasCome(); + } + + @Override + public void newNoGood(NoGood newNoGood) { + this.bufferedNoGoods.add(newNoGood); + } + + @Override + public void newNoGoods(Collection newNoGoods) { + this.bufferedNoGoods.addAll(newNoGoods); + } + + private void ingestBufferedNoGoods() { + heapOfActiveAtoms.newNoGoods(bufferedNoGoods); + bufferedNoGoods.clear(); + } + + /** + * {@link VSIDSWithPhaseSaving} works like {@link VSIDS} for selecting an atom but uses the saved phase to + * determine the truth value to choose. + */ + @Override + public int chooseLiteral() { + int atom = chooseAtom(); + if (atom == DEFAULT_CHOICE_ATOM) { + return DEFAULT_CHOICE_LITERAL; + } + boolean sign = chooseSign(atom); + return atomToLiteral(atom, sign); + } + + private int chooseAtom() { + ingestBufferedNoGoods(); + Integer mostActiveAtom; + while ((mostActiveAtom = heapOfActiveAtoms.getMostActiveAtom()) != null) { + if (choiceManager.isActiveChoiceAtom(mostActiveAtom)) { + return mostActiveAtom; + } + } + 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 + */ + private boolean chooseSign(int atom) { + if (assignment.getTruth(atom) == ThriceTruth.MBT) { + return true; + } + return assignment.getLastValue(atom); + } + + public void growForMaxAtomId(int maxAtomId) { + heapOfActiveAtoms.growForMaxAtomId(maxAtomId); + } + + @Override + public double getActivity(int literal) { + return heapOfActiveAtoms.getActivity(literal); + } + + @Override + public String toString() { + return this.getClass().getSimpleName(); + } + +} From 2904653d9931e486f4b17b70ebe337fc428f5d52 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sat, 5 Oct 2019 04:06:15 +0200 Subject: [PATCH 02/27] Adding restarts (default disabled). - CommandLineParser and SystemConfig have option to enable restarts. - DefaultSolver runs restarts if enabled. - Add MixedRestartStrategy combining Luby and dynamic (EMA) restarts. - Enhanced performance logs for conflicts and restarts --- .../kr/alpha/config/CommandLineParser.java | 9 +++ .../tuwien/kr/alpha/config/SystemConfig.java | 10 +++ .../tuwien/kr/alpha/solver/DefaultSolver.java | 26 +++++- .../alpha/solver/LearnedNoGoodDeletion.java | 7 ++ .../kr/alpha/solver/MixedRestartStrategy.java | 81 +++++++++++++++++++ .../kr/alpha/solver/PerformanceLog.java | 58 +++++++++---- 6 files changed, 173 insertions(+), 18 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java index 6efa8e4b4..26e1e786d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java @@ -107,6 +107,10 @@ public class CommandLineParser { .desc("disable the deletion of (learned, little active) nogoods (default: " + SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION + ")") .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 Options CLI_OPTS = new Options(); @@ -137,6 +141,7 @@ public class CommandLineParser { 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_ENABLE_RESTARTS); } /* @@ -180,6 +185,7 @@ public CommandLineParser(String cmdLineSyntax, Consumer abortAction) { 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_ENABLE_RESTARTS.getOpt(), this::handleEnableRestarts); this.inputOptionHandlers.put(CommandLineParser.OPT_NUM_ANSWER_SETS.getOpt(), this::handleNumAnswerSets); this.inputOptionHandlers.put(CommandLineParser.OPT_INPUT.getOpt(), this::handleInput); @@ -359,4 +365,7 @@ private void handleNoNoGoodDeletion(Option opt, SystemConfig cfg) { cfg.setDisableNoGoodDeletion(true); } + private void handleEnableRestarts(Option opt, SystemConfig cfg) { + cfg.setRestartsEnabled(true); + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java index 6ffeeb8cf..c8c3c9b08 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java @@ -56,6 +56,7 @@ public class SystemConfig { public static final boolean DEFAULT_SORT_ANSWER_SETS = false; public static final List DEFAULT_REPLAY_CHOICES = Collections.emptyList(); public static final boolean DEFAULT_DISABLE_NOGOOD_DELETION = false; + public static final boolean DEFAULT_ENABLE_RESTARTS = false; private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME; private String solverName = SystemConfig.DEFAULT_SOLVER_NAME; @@ -72,6 +73,7 @@ public class SystemConfig { private boolean sortAnswerSets = SystemConfig.DEFAULT_SORT_ANSWER_SETS; private List replayChoices = SystemConfig.DEFAULT_REPLAY_CHOICES; private boolean disableNoGoodDeletion = SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION; + private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS; public String getGrounderName() { return this.grounderName; @@ -205,4 +207,12 @@ public void setDisableNoGoodDeletion(boolean disableNoGoodDeletion) { this.disableNoGoodDeletion = disableNoGoodDeletion; } + public boolean areRestartsEnabled() { + return areRestartsEnabled; + } + + public void setRestartsEnabled(boolean areRestartsEnabled) { + this.areRestartsEnabled = areRestartsEnabled; + } + } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java index 91074801d..4bd785f47 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java @@ -67,6 +67,7 @@ public class DefaultSolver extends AbstractSolver implements SolverMaintainingSt private final WritableAssignment assignment; private final GroundConflictNoGoodLearner learner; + private final MixedRestartStrategy restartStrategy; private final BranchingHeuristic branchingHeuristic; @@ -86,10 +87,16 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.store = store; this.choiceManager = new ChoiceManager(assignment, store); 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, 1000); } private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) { @@ -148,9 +155,17 @@ protected boolean tryAdvance(Consumer action) { ConflictCause conflictCause = store.propagate(); didChange |= store.didPropagate(); LOGGER.trace("Assignment after propagation is: {}", assignment); - if (!disableNoGoodDeletion && conflictCause == null) { - // Run learned NoGood deletion strategy. - store.cleanupLearnedNoGoods(); + if (conflictCause == null) { + if (!disableNoGoodDeletion) { + // Run learned NoGood deletion strategy. + store.cleanupLearnedNoGoods(); + } + if (restartStrategy != null && restartStrategy.shouldRestart()) { + // Restart if necessary. + LOGGER.trace("Restarting search."); + choiceManager.backjump(0); + restartStrategy.onRestart(); + } } if (conflictCause != null) { // Learn from conflict. @@ -244,6 +259,9 @@ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) { } branchingHeuristic.analyzedConflict(analysisResult); + if (restartStrategy != null) { + restartStrategy.newConflictWithLbd(analysisResult.lbd); + } if (analysisResult.learnedNoGood != null) { choiceManager.backjump(analysisResult.backjumpLevel); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java index a17264654..d4fa14d4c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java @@ -25,6 +25,7 @@ class LearnedNoGoodDeletion { private final NoGoodStoreAlphaRoaming store; private final Assignment assignment; private int conflictCounter; + private int totalConflictsCounter; private int cleanupCounter; private int numberOfDeletedNoGoods; @@ -36,6 +37,7 @@ class LearnedNoGoodDeletion { void reset() { learnedNoGoods.clear(); conflictCounter = 0; + totalConflictsCounter = 0; cleanupCounter = 0; numberOfDeletedNoGoods = 0; } @@ -62,6 +64,7 @@ boolean needToRunNoGoodDeletion() { } void runNoGoodDeletion() { + totalConflictsCounter += conflictCounter; conflictCounter = 0; cleanupCounter++; // Reset the sequence after enough growth cycles. @@ -113,4 +116,8 @@ private boolean isLocked(WatchedNoGood noGood, Assignment assignment) { public int getNumberOfDeletedNoGoods() { return numberOfDeletedNoGoods; } + + int getNumTotalConflicts() { + return totalConflictsCounter + conflictCounter; + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java new file mode 100644 index 000000000..5e8a552ce --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java @@ -0,0 +1,81 @@ +package at.ac.tuwien.kr.alpha.solver; + +import static at.ac.tuwien.kr.alpha.Util.oops; +import static at.ac.tuwien.kr.alpha.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 += lbd << (32 - 5); + slow -= slow >> 14; + slow += 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; + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java index 9c4d74601..2e43dd50e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java @@ -28,25 +28,31 @@ 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 ChoiceManager choiceManager; - private TrailAssignment assignment; + private final ChoiceManager choiceManager; + private final TrailAssignment assignment; + private final MixedRestartStrategy restartStrategy; + private final LearnedNoGoodDeletion learnedNoGoodDeletion; private long msBetweenOutputs; private Long timeFirstEntry; private Long timeLastPerformanceLog; private int numberOfChoicesLastPerformanceLog; + private int numberOfRestartsLastPerformanceLog; + private int numberOfConflictsLastPerformanceLog; + private int numberOfDeletedNoGoodsLastPerformanceLog; - /** - * @param msBetweenOutputs - */ - public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, long msBetweenOutputs) { + public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, MixedRestartStrategy restartStrategy, LearnedNoGoodDeletion learnedNoGoodDeletion, long msBetweenOutputs) { super(); this.choiceManager = choiceManager; this.assignment = assignment; + this.restartStrategy = restartStrategy; + this.learnedNoGoodDeletion = learnedNoGoodDeletion; this.msBetweenOutputs = msBetweenOutputs; } @@ -60,14 +66,38 @@ public void initialize() { */ public void infoIfTimeForOutput(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 (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 From af19a1494d35d5706f2759426af480ac522ea680 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 7 Oct 2019 14:02:28 +0200 Subject: [PATCH 03/27] Enhance performance logs to show quality of heuristic decisions. - ChainedBranchingHeuristics gives access to first-run heuristics. - HeapOfActiveAtoms reports activity increment for normalization. - VSIDSWithPhaseSaving logs * the overall, normalized decrease in activity of the seelected atoms, * the number of most-active choices thrown away because they were not active choice points at the time. - PerformanceLog prints heuristics information if DefaultSolver is runnning with VSIDSWithPhaseSaving --- .../tuwien/kr/alpha/solver/DefaultSolver.java | 2 +- .../kr/alpha/solver/PerformanceLog.java | 17 +++++++++++++- .../ChainedBranchingHeuristics.java | 4 ++++ .../solver/heuristics/HeapOfActiveAtoms.java | 4 ++++ .../heuristics/VSIDSWithPhaseSaving.java | 23 +++++++++++++++++-- 5 files changed, 46 insertions(+), 4 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java index 4bd785f47..a47ceea44 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java @@ -96,7 +96,7 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration); this.disableJustifications = config.isDisableJustificationSearch(); this.disableNoGoodDeletion = config.isDisableNoGoodDeletion(); - this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, restartStrategy, learnedNoGoodDeletion, 1000); + this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, restartStrategy, learnedNoGoodDeletion, branchingHeuristic, 1000); } private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java index 2e43dd50e..28b9b14fe 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java @@ -25,6 +25,9 @@ */ package at.ac.tuwien.kr.alpha.solver; +import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristic; +import at.ac.tuwien.kr.alpha.solver.heuristics.ChainedBranchingHeuristics; +import at.ac.tuwien.kr.alpha.solver.heuristics.VSIDSWithPhaseSaving; import org.slf4j.Logger; /** @@ -38,6 +41,7 @@ public class PerformanceLog { private final TrailAssignment assignment; private final MixedRestartStrategy restartStrategy; private final LearnedNoGoodDeletion learnedNoGoodDeletion; + private final BranchingHeuristic branchingHeuristic; private long msBetweenOutputs; private Long timeFirstEntry; @@ -47,12 +51,13 @@ public class PerformanceLog { private int numberOfConflictsLastPerformanceLog; private int numberOfDeletedNoGoodsLastPerformanceLog; - public PerformanceLog(ChoiceManager choiceManager, TrailAssignment assignment, MixedRestartStrategy restartStrategy, LearnedNoGoodDeletion learnedNoGoodDeletion, 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; } @@ -83,6 +88,16 @@ public void infoIfTimeForOutput(Logger logger) { 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(); + double activityDecrease = vsidsWithPhaseSaving.getActivityDecrease(); + logger.info("Heuristic threw away {} preferred choices.", numThrownAway); + 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; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java index b8cfb0919..9a121f348 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java @@ -106,6 +106,10 @@ public static ChainedBranchingHeuristics chainOf(BranchingHeuristic... branching return new ChainedBranchingHeuristics(branchingHeuristics); } + public BranchingHeuristic getFirstElement() { + return chain.get(0); + } + /** * Returns a mapping from individual heuristics to number of decisions made by them. */ diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java index 56db8f727..acadd6920 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java @@ -103,6 +103,10 @@ public double getDecayFactor() { return decayFactor; } + double getCurrentActivityIncrement() { + return currentActivityIncrement; + } + /** * @see #getDecayFactor() */ diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index 80512659d..dddcd5f3d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -58,11 +58,12 @@ public class VSIDSWithPhaseSaving implements ActivityBasedBranchingHeuristic { protected final Assignment assignment; protected final ChoiceManager choiceManager; - private final HeapOfActiveAtoms heapOfActiveAtoms; - private final Collection bufferedNoGoods = new ArrayList<>(); + private double activityDecrease; + private long numThrownAway; + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { this.assignment = assignment; this.choiceManager = choiceManager; @@ -111,6 +112,14 @@ private void ingestBufferedNoGoods() { bufferedNoGoods.clear(); } + public double getActivityDecrease() { + return activityDecrease; + } + + public long getNumThrownAway() { + return numThrownAway; + } + /** * {@link VSIDSWithPhaseSaving} works like {@link VSIDS} for selecting an atom but uses the saved phase to * determine the truth value to choose. @@ -128,10 +137,20 @@ public int chooseLiteral() { private 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 lostActitivyNormalized = (maxActivity - activity) / heapOfActiveAtoms.getCurrentActivityIncrement(); + activityDecrease += lostActitivyNormalized; + } return mostActiveAtom; } + numThrownAway++; } return DEFAULT_CHOICE_ATOM; } From c3ac9780830005225625f509af61a77b771d3e99 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 23 Oct 2019 04:33:52 +0200 Subject: [PATCH 04/27] Add options for initial phase settings; add atom dependency to VSIDS with phase saving. - CommandLineParser and SystemConfig accept initial phase settings. - AtomChoiceRelation stores relation between ordinary atoms and the choice points that influence them. - NaiveGrounder and ProgramAnalyzingGrounder provide AtomChoiceRelation. - NoGoodGenerator fills AtomChoiceRelation. - BranchingHeuristicFactory sets AtomChoiceRelation for VSIDSWithPhaseSaving. - PhaseInitializerFactory provides different initial phase settings. - VSIDSWithPhaseSaving uses AtomChoiceRelation for activity increments. - SolverFactory sets chosen phase initializer. - TrailAssignment considers initial phase value, if phase was not set. - Tests set a phase initializer if needed. --- .../kr/alpha/config/CommandLineParser.java | 9 +++ .../tuwien/kr/alpha/config/SystemConfig.java | 10 ++++ .../kr/alpha/grounder/NaiveGrounder.java | 8 ++- .../kr/alpha/grounder/NoGoodGenerator.java | 14 ++++- .../grounder/ProgramAnalyzingGrounder.java | 7 +++ .../structure/AtomChoiceRelation.java | 31 ++++++++++ .../tuwien/kr/alpha/solver/DefaultSolver.java | 1 + .../tuwien/kr/alpha/solver/SolverFactory.java | 5 +- .../kr/alpha/solver/TrailAssignment.java | 19 +++++-- .../heuristics/BranchingHeuristicFactory.java | 5 +- .../heuristics/PhaseInitializerFactory.java | 57 +++++++++++++++++++ .../heuristics/VSIDSWithPhaseSaving.java | 34 ++++++++--- .../kr/alpha/grounder/NaiveGrounderTest.java | 7 ++- .../structure/AnalyzeUnjustifiedTest.java | 9 +-- .../kr/alpha/solver/ChoiceManagerTests.java | 3 +- .../solver/LearnedNoGoodDeletionTest.java | 3 +- .../kr/alpha/solver/NaiveNoGoodStoreTest.java | 3 +- .../solver/NoGoodStoreAlphaRoamingTest.java | 3 +- .../kr/alpha/solver/TrailAssignmentTest.java | 3 +- .../AlphaHeuristicTestAssumptions.java | 2 +- .../alpha/solver/heuristics/BerkMinTest.java | 2 +- .../BranchingHeuristicFactoryTest.java | 2 +- .../heuristics/HeapOfActiveAtomsTest.java | 2 +- .../heuristics/ReplayHeuristicTest.java | 2 +- .../kr/alpha/solver/heuristics/VSIDSTest.java | 2 +- .../GroundConflictNoGoodLearnerTest.java | 3 +- 26 files changed, 212 insertions(+), 34 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java index 26e1e786d..a5541916c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java @@ -111,6 +111,9 @@ public class CommandLineParser { .desc("enable the usage of (dynamic and static) restarts (default: " + SystemConfig.DEFAULT_ENABLE_RESTARTS + ")") .build(); + private static final Option OPT_INITIAL_PHASE = Option.builder("ph").longOpt("initialPhase").hasArg(true).argName("initializer") + .desc("set the initial phase [ alltrue | allfalse | random ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + ")") + .build(); private static final Options CLI_OPTS = new Options(); @@ -142,6 +145,7 @@ public class CommandLineParser { CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NORMALIZATION_GRID); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_NOGOOD_DELETION); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_ENABLE_RESTARTS); + CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_INITIAL_PHASE); } /* @@ -186,6 +190,7 @@ public CommandLineParser(String cmdLineSyntax, Consumer abortAction) { 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_ENABLE_RESTARTS.getOpt(), this::handleEnableRestarts); + this.globalOptionHandlers.put(CommandLineParser.OPT_INITIAL_PHASE.getOpt(), this::handleInitialPhase); this.inputOptionHandlers.put(CommandLineParser.OPT_NUM_ANSWER_SETS.getOpt(), this::handleNumAnswerSets); this.inputOptionHandlers.put(CommandLineParser.OPT_INPUT.getOpt(), this::handleInput); @@ -368,4 +373,8 @@ private void handleNoNoGoodDeletion(Option opt, SystemConfig cfg) { private void handleEnableRestarts(Option opt, SystemConfig cfg) { cfg.setRestartsEnabled(true); } + + private void handleInitialPhase(Option opt, SystemConfig cfg) { + cfg.setPhaseInitializer(opt.getValue(SystemConfig.DEFAULT_PHASE_INITIALIZER)); + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java index c8c3c9b08..5fceeddb3 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java @@ -57,6 +57,7 @@ public class SystemConfig { public static final List DEFAULT_REPLAY_CHOICES = Collections.emptyList(); public static final boolean DEFAULT_DISABLE_NOGOOD_DELETION = false; public static final boolean DEFAULT_ENABLE_RESTARTS = false; + public static final String DEFAULT_PHASE_INITIALIZER = "random"; private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME; private String solverName = SystemConfig.DEFAULT_SOLVER_NAME; @@ -74,6 +75,7 @@ public class SystemConfig { private List replayChoices = SystemConfig.DEFAULT_REPLAY_CHOICES; private boolean disableNoGoodDeletion = SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION; private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS; + private String phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER; public String getGrounderName() { return this.grounderName; @@ -215,4 +217,12 @@ public void setRestartsEnabled(boolean areRestartsEnabled) { this.areRestartsEnabled = areRestartsEnabled; } + public String getPhaseInitializerName() { + return phaseInitializer; + } + + public void setPhaseInitializer(String phaseInitializer) { + this.phaseInitializer = phaseInitializer; + } + } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java index 387f86a4e..768403d92 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java @@ -39,6 +39,7 @@ import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.grounder.bridges.Bridge; import at.ac.tuwien.kr.alpha.grounder.structure.AnalyzeUnjustified; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis; import at.ac.tuwien.kr.alpha.grounder.transformation.*; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; @@ -72,6 +73,7 @@ public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGr private final Map> rulesUsingPredicateWorkingMemory = new HashMap<>(); private final Map> knownGroundingSubstitutions = new HashMap<>(); private final Map knownNonGroundRules = new HashMap<>(); + private final AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation(); private ArrayList fixedRules = new ArrayList<>(); private LinkedHashSet removeAfterObtainingNewNoGoods = new LinkedHashSet<>(); @@ -108,11 +110,15 @@ public NaiveGrounder(Program program, AtomStore atomStore, boolean debugInternal final Set uniqueGroundRulePerGroundHead = getRulesWithUniqueHead(); choiceRecorder = new ChoiceRecorder(atomStore); - noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, programAnalysis, uniqueGroundRulePerGroundHead); + noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, programAnalysis, uniqueGroundRulePerGroundHead, atomChoiceRelation); this.debugInternalChecks = debugInternalChecks; } + public AtomChoiceRelation getAtomChoiceRelation() { + return atomChoiceRelation; + } + private void initializeFactsAndRules(Program program) { // initialize all facts for (Atom fact : program.getFacts()) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java index 72500f499..7a1e015ff 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java @@ -34,6 +34,7 @@ import at.ac.tuwien.kr.alpha.common.atoms.FixedInterpretationLiteral; import at.ac.tuwien.kr.alpha.grounder.atoms.EnumerationAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.grounder.structure.ProgramAnalysis; import java.util.*; @@ -52,13 +53,15 @@ public class NoGoodGenerator { private final Map> factsFromProgram; private final ProgramAnalysis programAnalysis; private final Set uniqueGroundRulePerGroundHead; + private final AtomChoiceRelation atomChoiceRelation; - NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map> factsFromProgram, ProgramAnalysis programAnalysis, Set uniqueGroundRulePerGroundHead) { + NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map> factsFromProgram, ProgramAnalysis programAnalysis, Set uniqueGroundRulePerGroundHead, AtomChoiceRelation atomChoiceRelation) { this.atomStore = atomStore; this.choiceRecorder = recorder; this.factsFromProgram = factsFromProgram; this.programAnalysis = programAnalysis; this.uniqueGroundRulePerGroundHead = uniqueGroundRulePerGroundHead; + this.atomChoiceRelation = atomChoiceRelation; } /** @@ -126,6 +129,15 @@ List generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround result.addAll(choiceRecorder.generateChoiceNoGoods(posLiterals, negLiterals, bodyRepresentingLiteral)); } + // Record atom-choiceAtom relationships for rules that are choice points. + if (!negLiterals.isEmpty()) { + atomChoiceRelation.growForMaxAtomId(atomStore.getMaxAtomId()); + atomChoiceRelation.addRelation(headId, atomOf(bodyRepresentingLiteral)); + for (Integer negLiteral : negLiterals) { + atomChoiceRelation.addRelation(atomOf(negLiteral), atomOf(bodyRepresentingLiteral)); + } + } + return result; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java index 21295d1e7..57ba291e1 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java @@ -3,6 +3,7 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import java.util.Set; @@ -32,4 +33,10 @@ public interface ProgramAnalyzingGrounder extends Grounder { * @return the corresponding NonGroundRule. */ NonGroundRule getNonGroundRule(Integer ruleId); + + /** + * Provides relationship information between atoms and choice points influencing their truth values. + * @return the {@link AtomChoiceRelation}. + */ + AtomChoiceRelation getAtomChoiceRelation(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java new file mode 100644 index 000000000..8db7941e2 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java @@ -0,0 +1,31 @@ +package at.ac.tuwien.kr.alpha.grounder.structure; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** + * Stores and provides relationships between ordinary atoms and those that represent choice points. + * + * Copyright (c) 2019, the Alpha Team. + */ +public class AtomChoiceRelation { + private final ArrayList> atomToChoiceAtoms = new ArrayList<>(); + + public void addRelation(int atom, int bodyRepresentingAtom) { + while (atom > atomToChoiceAtoms.size() - 1) { + atomToChoiceAtoms.add(new ArrayList<>()); + } + atomToChoiceAtoms.get(atom).add(bodyRepresentingAtom); + } + + public List getRelatedChoiceAtoms(int atom) { + return Collections.unmodifiableList(atomToChoiceAtoms.get(atom)); + } + + public void growForMaxAtomId(int maxAtomId) { + while (maxAtomId > atomToChoiceAtoms.size() - 1) { + atomToChoiceAtoms.add(new ArrayList<>()); + } + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java index a47ceea44..9b0d3980c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java @@ -165,6 +165,7 @@ protected boolean tryAdvance(Consumer action) { LOGGER.trace("Restarting search."); choiceManager.backjump(0); restartStrategy.onRestart(); + continue; } } if (conflictCause != null) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java index 36bbe668d..755ad8012 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java @@ -32,6 +32,7 @@ import at.ac.tuwien.kr.alpha.grounder.Grounder; import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration; import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfigurationBuilder; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import java.util.Random; @@ -42,7 +43,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.getPhaseInitializerName(), random); + final WritableAssignment assignment = new TrailAssignment(atomStore, phaseInitializer, debugInternalChecks); NoGoodStore store; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java index d76166a7e..da49f4f21 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java @@ -30,6 +30,7 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -69,6 +70,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 @@ -82,6 +84,7 @@ public void decreaseActivity() { private Antecedent[] impliedBy; private boolean[] callbackUponChange; private boolean[] phase; + private boolean[] hasPhaseSet; private ArrayList outOfOrderLiterals = new ArrayList<>(); private int highestDecisionLevelContainingOutOfOrderLiterals; private ArrayList trail = new ArrayList<>(); @@ -95,7 +98,8 @@ public void decreaseActivity() { private boolean checksEnabled; int 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]; @@ -103,6 +107,7 @@ public TrailAssignment(AtomStore atomStore, boolean checksEnabled) { 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; @@ -110,8 +115,8 @@ public TrailAssignment(AtomStore atomStore, boolean checksEnabled) { assignmentsForChoicePosition = 0; } - public TrailAssignment(AtomStore atomStore) { - this(atomStore, false); + public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitializer phaseInitializer) { + this(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue(), false); } @Override @@ -122,6 +127,7 @@ public void clear() { Arrays.fill(impliedBy, null); Arrays.fill(callbackUponChange, false); Arrays.fill(phase, false); + Arrays.fill(hasPhaseSet, false); outOfOrderLiterals = new ArrayList<>(); highestDecisionLevelContainingOutOfOrderLiterals = 0; trail = new ArrayList<>(); @@ -357,6 +363,7 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent im 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++; @@ -451,7 +458,10 @@ public Antecedent getImpliedBy(int atom) { @Override public boolean getLastValue(int atom) { - return phase[atom]; + if (hasPhaseSet[atom]) { + return phase[atom]; + } + return phaseInitializer.getNextInitialPhase(); } @Override @@ -543,6 +553,7 @@ public void growForMaxAtomId() { 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); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java index 740e016fd..6d56a9ed9 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java @@ -26,6 +26,8 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; import at.ac.tuwien.kr.alpha.grounder.Grounder; +import at.ac.tuwien.kr.alpha.grounder.ProgramAnalyzingGrounder; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.WritableAssignment; import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProviderFactory.BodyActivityType; @@ -119,7 +121,8 @@ private static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfigurati case GDD_VSIDS: return new DependencyDrivenVSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); case VSIDS_PHASE_SAVING: - return new VSIDSWithPhaseSaving(assignment, choiceManager, heuristicsConfiguration.getMomsStrategy()); + AtomChoiceRelation atomChoiceRelation = grounder instanceof ProgramAnalyzingGrounder ? ((ProgramAnalyzingGrounder) grounder).getAtomChoiceRelation() : null; + return new VSIDSWithPhaseSaving(assignment, choiceManager, atomChoiceRelation, heuristicsConfiguration.getMomsStrategy()); } throw new IllegalArgumentException("Unknown branching heuristic requested."); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java new file mode 100644 index 000000000..095f1435f --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java @@ -0,0 +1,57 @@ +package at.ac.tuwien.kr.alpha.solver.heuristics; + +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(); + } + + public static PhaseInitializer getInstance(String phaseInitializerName, Random random) { + switch (phaseInitializerName.toLowerCase()) { + case "alltrue": + return getPhaseInitializerAllTrue(); + case "allfalse": + return getPhaseInitializerAllFalse(); + case "random": + return getPhaseInitializerRandom(random); + default: + throw new IllegalArgumentException("Unknown phase initializer requested:" + phaseInitializerName); + } + } + + public static PhaseInitializer getPhaseInitializerAllTrue() { + return new PhaseInitializer() { + @Override + public boolean getNextInitialPhase() { + return true; + } + }; + } + + private static PhaseInitializer getPhaseInitializerAllFalse() { + return new PhaseInitializer() { + @Override + public boolean getNextInitialPhase() { + return false; + } + }; + } + + private static PhaseInitializer getPhaseInitializerRandom(Random random) { + return new PhaseInitializer() { + private final Random rand = random; + @Override + public boolean getNextInitialPhase() { + return rand.nextBoolean(); + } + }; + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index dddcd5f3d..7de6b294b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -27,6 +27,7 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; @@ -37,6 +38,7 @@ import java.util.ArrayList; import java.util.Collection; +import static at.ac.tuwien.kr.alpha.Util.oops; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; @@ -58,25 +60,27 @@ public class VSIDSWithPhaseSaving implements ActivityBasedBranchingHeuristic { protected final Assignment assignment; protected final ChoiceManager choiceManager; + private final AtomChoiceRelation atomChoiceRelation; private final HeapOfActiveAtoms heapOfActiveAtoms; private final Collection bufferedNoGoods = new ArrayList<>(); private double activityDecrease; private long numThrownAway; - private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { this.assignment = assignment; this.choiceManager = choiceManager; + this.atomChoiceRelation = atomChoiceRelation; this.heapOfActiveAtoms = heapOfActiveAtoms; this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy); } - private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { - this(assignment, choiceManager, new HeapOfActiveAtoms(decayPeriod, decayFactor, choiceManager), momsStrategy); + private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + this(assignment, choiceManager, atomChoiceRelation, new HeapOfActiveAtoms(decayPeriod, decayFactor, choiceManager), momsStrategy); } - VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { - this(assignment, choiceManager, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR, momsStrategy); + VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + this(assignment, choiceManager, atomChoiceRelation, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR, momsStrategy); } @Override @@ -87,16 +91,29 @@ public void violatedNoGood(NoGood violatedNoGood) { public void analyzedConflict(ConflictAnalysisResult analysisResult) { ingestBufferedNoGoods(); //analysisResult may contain new atoms whose activity must be initialized for (int resolutionAtom : analysisResult.resolutionAtoms) { - heapOfActiveAtoms.incrementActivity(resolutionAtom); + incrementActivityOfRelatedChoiceAtoms(resolutionAtom); } if (analysisResult.learnedNoGood != null) { for (int literal : analysisResult.learnedNoGood) { - heapOfActiveAtoms.incrementActivity(atomOf(literal)); + incrementActivityOfRelatedChoiceAtoms(atomOf(literal)); } } heapOfActiveAtoms.decayIfTimeHasCome(); } + private void incrementActivityOfRelatedChoiceAtoms(int toAtom) { + if (atomChoiceRelation == null) { + heapOfActiveAtoms.incrementActivity(toAtom); + return; + } + for (Integer relatedChoiceAtom : atomChoiceRelation.getRelatedChoiceAtoms(toAtom)) { + if (!choiceManager.isAtomChoice(relatedChoiceAtom)) { + throw oops("Related atom is no choice."); + } + heapOfActiveAtoms.incrementActivity(relatedChoiceAtom); + } + } + @Override public void newNoGood(NoGood newNoGood) { this.bufferedNoGoods.add(newNoGood); @@ -172,6 +189,9 @@ private boolean chooseSign(int atom) { public void growForMaxAtomId(int maxAtomId) { heapOfActiveAtoms.growForMaxAtomId(maxAtomId); + if (atomChoiceRelation != null) { + atomChoiceRelation.growForMaxAtomId(maxAtomId); + } } @Override diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java index aadf8c8f0..117d55d92 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java @@ -29,6 +29,7 @@ import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Test; import java.util.Arrays; @@ -57,7 +58,7 @@ public void groundRuleAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); + Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue())); int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false); int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0)))); assertExistsNoGoodContaining(noGoods.values(), litCNeg); @@ -77,7 +78,7 @@ public void groundRuleWithLongerBodyAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); + Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue())); int litANeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("a", 0))), false); int litBNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))), false); int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false); @@ -100,7 +101,7 @@ public void groundConstraintAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); + Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue())); int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0)))); assertTrue(noGoods.containsValue(NoGood.fromConstraint(Arrays.asList(litB), Collections.emptyList()))); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java index efe8b1baf..7a23ef780 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java @@ -39,6 +39,7 @@ import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Test; import java.util.Arrays; @@ -67,7 +68,7 @@ public void justifySimpleRules() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); + TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); int rId = atomStore.get(new BasicAtom(Predicate.getInstance("r", 0))); int nrId = atomStore.get(new BasicAtom(Predicate.getInstance("nr", 0))); assignment.growForMaxAtomId(); @@ -92,7 +93,7 @@ public void justifyLargerRules() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); + TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); Atom p1 = parser.parse("p(1).").getFacts().get(0); Atom r2 = parser.parse("r(2).").getFacts().get(0); Atom s12 = parser.parse("s(1,2).").getFacts().get(0); @@ -129,7 +130,7 @@ public void justifyMultipleReasons() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); + TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); Atom qa = parser.parse("q(a).").getFacts().get(0); Atom qb = parser.parse("q(b).").getFacts().get(0); Atom qc = parser.parse("q(c).").getFacts().get(0); @@ -185,7 +186,7 @@ public void justifyNegatedFactsRemovedFromReasons() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore); + TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); int rId = atomStore.get(new BasicAtom(Predicate.getInstance("r", 0))); int nrId = atomStore.get(new BasicAtom(Predicate.getInstance("nr", 0))); assignment.growForMaxAtomId(); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java index 682ddb425..49e06f571 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java @@ -33,6 +33,7 @@ import at.ac.tuwien.kr.alpha.grounder.NaiveGrounder; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Test; @@ -53,7 +54,7 @@ public void setUp() throws IOException { Program parsedProgram = new ProgramParser().parse(testProgram); this.atomStore = new AtomStoreImpl(); this.grounder = new NaiveGrounder(parsedProgram, atomStore, true); - WritableAssignment assignment = new TrailAssignment(atomStore); + WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment); this.choiceManager = new ChoiceManager(assignment, store); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java index 1d9f4cbc5..2ec460f14 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.common.AtomStoreTest; import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Test; @@ -47,7 +48,7 @@ public class LearnedNoGoodDeletionTest { public LearnedNoGoodDeletionTest() { AtomStore atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 200); - WritableAssignment assignment = new TrailAssignment(atomStore); + WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); assignment.growForMaxAtomId(); store = new NoGoodStoreAlphaRoaming(assignment); learnedNoGoodDeletion = store.getLearnedNoGoodDeletion(); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java index 33a069469..5bc9477ca 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java @@ -1,6 +1,7 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Ignore; import org.junit.Test; @@ -22,7 +23,7 @@ public class NaiveNoGoodStoreTest { public NaiveNoGoodStoreTest() { atomStore = new AtomStoreImpl(); - assignment = new TrailAssignment(atomStore); + assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); store = new NaiveNoGoodStore(assignment); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java index 0f6d73acf..20f18ce43 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java @@ -1,6 +1,7 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Ignore; import org.junit.Test; @@ -24,7 +25,7 @@ public class NoGoodStoreAlphaRoamingTest { public NoGoodStoreAlphaRoamingTest() { atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 200); - assignment = new TrailAssignment(atomStore); + assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); assignment.growForMaxAtomId(); store = new NoGoodStoreAlphaRoaming(assignment); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java index 119e3a0db..f90c7bc05 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.common.AtomStoreTest; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Test; @@ -51,7 +52,7 @@ public class TrailAssignmentTest { public TrailAssignmentTest() { AtomStore atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 20); - assignment = new TrailAssignment(atomStore); + assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); } @Before diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java index ab891ae23..4c325280e 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java @@ -73,7 +73,7 @@ public void setUp() throws IOException { Program parsedProgram = new ProgramParser().parse(testProgram); this.atomStore = new AtomStoreImpl(); this.grounder = new NaiveGrounder(parsedProgram, atomStore, true); - this.assignment = new TrailAssignment(atomStore); + this.assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); this.choiceManager = new TestableChoiceManager(assignment, new NaiveNoGoodStore(assignment)); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java index 29227058f..5d660946e 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java @@ -62,7 +62,7 @@ public class BerkMinTest { public void setUp() { AtomStore atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 2); - WritableAssignment assignment = new TrailAssignment(atomStore); + WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); assignment.growForMaxAtomId(); this.berkmin = new BerkMin( assignment, diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java index 519f14169..8254e889d 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java @@ -48,7 +48,7 @@ public class BranchingHeuristicFactoryTest { @Before public void setUp() { AtomStore atomStore = new AtomStoreImpl(); - WritableAssignment assignment = new TrailAssignment(atomStore); + WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks); this.choiceManager = new ChoiceManager(assignment, store); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java index a73882ed5..a8955bd78 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java @@ -55,7 +55,7 @@ public class HeapOfActiveAtomsTest { @Before public void setUp() { atomStore = new AtomStoreImpl(); - assignment = new TrailAssignment(atomStore); + assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); noGoodStore = new NoGoodStoreAlphaRoaming(assignment); ChoiceManager choiceManager = new PseudoChoiceManager(assignment, noGoodStore); this.vsids = new VSIDS(assignment, choiceManager, MOMs.DEFAULT_STRATEGY); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java index 81ec7bbd1..d6b8796a5 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java @@ -48,7 +48,7 @@ public class ReplayHeuristicTest { @Before public void setUp() { AtomStore atomStore = new AtomStoreImpl(); - WritableAssignment assignment = new TrailAssignment(atomStore); + WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks); this.choiceManager = new PseudoChoiceManager(assignment, store); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java index e4f4f714f..71f10e96c 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java @@ -68,7 +68,7 @@ public class VSIDSTest { public void setUp() { atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 4); - assignment = new TrailAssignment(atomStore); + assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); assignment.growForMaxAtomId(); noGoodStore = new NoGoodStoreAlphaRoaming(assignment); this.vsids = new VSIDS( diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java index 238894bbd..9ec7ecfdf 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java @@ -5,6 +5,7 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreTest; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.*; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Ignore; import org.junit.Test; @@ -24,7 +25,7 @@ public class GroundConflictNoGoodLearnerTest { public GroundConflictNoGoodLearnerTest() { atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 20); - this.assignment = new TrailAssignment(atomStore); + this.assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); this.assignment.growForMaxAtomId(); this.store = new NoGoodStoreAlphaRoaming(assignment); this.store.growForMaxAtomId(20); From 78b7e89d383a9435e85ad512d8ff647387114822 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Thu, 7 Nov 2019 03:32:53 +0100 Subject: [PATCH 05/27] Add HeapOfRelatedChoiceAtoms recording only choice points, improve logs. - In HeapOfActiveAtoms several members/methods package-private now to allow overriding. - Add HeapOfRelatedChoiceAtoms using AtomChoiceRelation to only record and initialize choice points. - Moved ChoiceManager update in DefaultSolver to correctly know which atoms are choice points. - Improved logging in VSIDSWithPhaseSaving and PerformanceLog. --- .../kr/alpha/grounder/ChoiceRecorder.java | 2 +- .../tuwien/kr/alpha/solver/DefaultSolver.java | 2 +- .../kr/alpha/solver/PerformanceLog.java | 4 +- .../solver/heuristics/HeapOfActiveAtoms.java | 16 +++---- .../heuristics/HeapOfRelatedChoiceAtoms.java | 42 +++++++++++++++++++ .../heuristics/VSIDSWithPhaseSaving.java | 17 +++++++- 6 files changed, 71 insertions(+), 12 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java index c807e0bae..d4b223a60 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java @@ -121,7 +121,7 @@ public String toString() { } sb.append(" disablers: "); for (Map.Entry disablers : newChoiceAtoms.getRight().entrySet()) { - sb.append(disablers.getKey()).append("/").append(disablers.getValue()); + sb.append(disablers.getKey()).append("/").append(disablers.getValue()).append(", "); } return sb.append("]").toString(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java index 9b0d3980c..c59a8d16e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/DefaultSolver.java @@ -468,6 +468,7 @@ private boolean ingest(Map obtained) { int maxAtomId = atomStore.getMaxAtomId(); store.growForMaxAtomId(maxAtomId); branchingHeuristic.growForMaxAtomId(maxAtomId); + choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies()); branchingHeuristic.newNoGoods(obtained.values()); LinkedList> noGoodsToAdd = new LinkedList<>(obtained.entrySet()); @@ -517,7 +518,6 @@ private NoGood fixContradiction(Map.Entry noGoodEntry, Conflict } 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/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java index 28b9b14fe..4cea57caa 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java @@ -93,8 +93,10 @@ public void infoIfTimeForOutput(Logger logger) { 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.", numThrownAway); + logger.info("Heuristic threw away {} preferred choices ({} no choice, {} not active choice points).", numThrownAway, numNoChoicePoint, numNotActiveChoicePoint); logger.info("Atom activity decreased overall by {} or {} per choice on average", activityDecrease, activityDecrease / currentNumberOfChoices); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java index acadd6920..b9c65515d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java @@ -54,10 +54,10 @@ public class HeapOfActiveAtoms { 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]; - private double[] activityScores = new double[0]; + boolean[] incrementedActivityScores = new boolean[0]; + double[] activityScores = new double[0]; final PriorityQueue heap = new PriorityQueue<>(new AtomActivityComparator().reversed()); protected ChoiceManager choiceManager; @@ -65,9 +65,9 @@ public class HeapOfActiveAtoms { private double decayFactor; private int stepsSinceLastDecay; private double currentActivityIncrement = 1.0; - private int numberOfNormalizations; + int numberOfNormalizations; - private final MOMs moms; + final MOMs moms; HeapOfActiveAtoms(int decayPeriod, double decayFactor, ChoiceManager choiceManager) { this.decayPeriod = decayPeriod; @@ -164,7 +164,7 @@ private 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); @@ -233,7 +233,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; LOGGER.trace("Activity of atom {} set to {}", atom, newActivity); @@ -258,7 +258,7 @@ 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; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java new file mode 100644 index 000000000..28dc52f31 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfRelatedChoiceAtoms.java @@ -0,0 +1,42 @@ +package at.ac.tuwien.kr.alpha.solver.heuristics; + +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; +import at.ac.tuwien.kr.alpha.solver.ChoiceManager; + +import static at.ac.tuwien.kr.alpha.common.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/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index 7de6b294b..a13c9e301 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -66,6 +66,8 @@ public class VSIDSWithPhaseSaving implements ActivityBasedBranchingHeuristic { private double activityDecrease; private long numThrownAway; + private long numNoChoicePoint; + private long numNotActiveChoicePoint; private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { this.assignment = assignment; @@ -76,7 +78,7 @@ private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, } private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { - this(assignment, choiceManager, atomChoiceRelation, new HeapOfActiveAtoms(decayPeriod, decayFactor, choiceManager), momsStrategy); + this(assignment, choiceManager, atomChoiceRelation, new HeapOfRelatedChoiceAtoms(decayPeriod, decayFactor, choiceManager, atomChoiceRelation), momsStrategy); } VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { @@ -137,6 +139,14 @@ public long getNumThrownAway() { return numThrownAway; } + public long getNumNoChoicePoint() { + return numNoChoicePoint; + } + + public long getNumNotActiveChoicePoint() { + return numNotActiveChoicePoint; + } + /** * {@link VSIDSWithPhaseSaving} works like {@link VSIDS} for selecting an atom but uses the saved phase to * determine the truth value to choose. @@ -167,6 +177,11 @@ private int chooseAtom() { } return mostActiveAtom; } + if (choiceManager.isAtomChoice(mostActiveAtom)) { + numNotActiveChoicePoint++; + } else { + numNoChoicePoint++; + } numThrownAway++; } return DEFAULT_CHOICE_ATOM; From 6143e82e801caeb700866f4bfd0d2df21454f357 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 12 Nov 2019 01:29:55 +0100 Subject: [PATCH 06/27] Fix bug in AlphaHeadMustBeTrueHeuristic. --- .../alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java index 52df83cd4..06d8cf20e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeadMustBeTrueHeuristic.java @@ -36,6 +36,8 @@ import java.util.Set; import java.util.stream.Stream; +import static at.ac.tuwien.kr.alpha.common.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.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(); } From cd6ea23e4f7dde7c4d93aa458fbe05c11d105ba8 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 12 Nov 2019 02:00:21 +0100 Subject: [PATCH 07/27] Fix Luby restart sequence computation. --- .../java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java index 5e8a552ce..56cf97125 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/MixedRestartStrategy.java @@ -76,6 +76,6 @@ private void nextLuby() { } else { vn <<= 1; } - lubyLimit = vn * LUBY_FACTOR; + lubyLimit = vn * LUBY_FACTOR + learnedNoGoodDeletion.getNumTotalConflicts(); } } From e83c8661ca887e5e4527ac2f81a99e73d7c8bd41 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 12 Nov 2019 04:44:13 +0100 Subject: [PATCH 08/27] Make AtomChoiceRelation a mandatory Grounder component. - Move getAtomChoiceRelation() from NaiveGrounder to Grounder, implement method also in DummyGrounder and ChoiceGrounder. - HeapOfActiveAtoms keeps track of literals occurring in the heap. - More logging stats from VSIDSWithPhaseSaving. - ChoiceInfluenceManager: simplified callbackOnChange --- .../ac/tuwien/kr/alpha/grounder/Grounder.java | 8 ++++ .../kr/alpha/grounder/NaiveGrounder.java | 1 + .../alpha/solver/ChoiceInfluenceManager.java | 10 +++-- .../kr/alpha/solver/PerformanceLog.java | 3 +- .../heuristics/BranchingHeuristicFactory.java | 3 +- .../solver/heuristics/HeapOfActiveAtoms.java | 37 +++++++++++++------ .../heuristics/VSIDSWithPhaseSaving.java | 4 ++ .../kr/alpha/grounder/ChoiceGrounder.java | 11 ++++++ .../kr/alpha/grounder/DummyGrounder.java | 7 ++++ 9 files changed, 65 insertions(+), 19 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java index cee82381e..89503f40f 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/Grounder.java @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import org.apache.commons.lang3.tuple.Pair; import java.util.Iterator; @@ -79,4 +80,11 @@ public interface Grounder { * @return */ int register(NoGood noGood); + + + /** + * Returns the relation between atoms and choices in form of an {@link AtomChoiceRelation} object. + * @return the {@link AtomChoiceRelation} of the grounded program parts. + */ + AtomChoiceRelation getAtomChoiceRelation(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java index 768403d92..7134a6dbe 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java @@ -115,6 +115,7 @@ public NaiveGrounder(Program program, AtomStore atomStore, boolean debugInternal this.debugInternalChecks = debugInternalChecks; } + @Override public AtomChoiceRelation getAtomChoiceRelation() { return atomChoiceRelation; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java index c3111fd84..7ae3cfe7c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ChoiceInfluenceManager.java @@ -196,8 +196,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); } } @@ -207,8 +209,8 @@ public String toString() { } } - public static interface ActivityListener { - void callbackOnChanged(int atom, boolean active); + public interface ActivityListener { + void callbackOnChange(int atom); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java index 4cea57caa..a84b45c69 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/PerformanceLog.java @@ -96,7 +96,8 @@ public void infoIfTimeForOutput(Logger logger) { 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).", numThrownAway, numNoChoicePoint, numNotActiveChoicePoint); + 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); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java index 6d56a9ed9..93a23f018 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactory.java @@ -26,7 +26,6 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; import at.ac.tuwien.kr.alpha.grounder.Grounder; -import at.ac.tuwien.kr.alpha.grounder.ProgramAnalyzingGrounder; import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.WritableAssignment; @@ -121,7 +120,7 @@ private static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfigurati case GDD_VSIDS: return new DependencyDrivenVSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); case VSIDS_PHASE_SAVING: - AtomChoiceRelation atomChoiceRelation = grounder instanceof ProgramAnalyzingGrounder ? ((ProgramAnalyzingGrounder) grounder).getAtomChoiceRelation() : null; + AtomChoiceRelation atomChoiceRelation = grounder.getAtomChoiceRelation(); return new VSIDSWithPhaseSaving(assignment, choiceManager, atomChoiceRelation, heuristicsConfiguration.getMomsStrategy()); } throw new IllegalArgumentException("Unknown branching heuristic requested."); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java index b9c65515d..5182c0948 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java @@ -57,6 +57,7 @@ public class HeapOfActiveAtoms { static final double SCORE_EPSILON = 1E-100; boolean[] incrementedActivityScores = new boolean[0]; + boolean[] occursInHeap = new boolean[0]; double[] activityScores = new double[0]; final PriorityQueue heap = new PriorityQueue<>(new AtomActivityComparator().reversed()); @@ -66,6 +67,7 @@ public class HeapOfActiveAtoms { private int stepsSinceLastDecay; private double currentActivityIncrement = 1.0; int numberOfNormalizations; + private long numAddedToHeapByActivity; final MOMs moms; @@ -186,6 +188,7 @@ protected 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) { @@ -197,8 +200,7 @@ void growForMaxAtomId(int maxAtomId) { if (newCapacity < maxAtomId + 1) { newCapacity = maxAtomId + 1; } - activityScores = Arrays.copyOf(activityScores, newCapacity); - incrementedActivityScores = Arrays.copyOf(incrementedActivityScores, newCapacity); + growToCapacity(newCapacity); } private void initActivityNaive(NoGood newNoGood) { @@ -213,7 +215,11 @@ private void initActivityNaive(NoGood newNoGood) { * Returns the atom with the highest activity score and removes it from the heap. */ Integer getMostActiveAtom() { - return heap.poll(); + Integer mostActiveAtom = heap.poll(); + if (mostActiveAtom != null) { + occursInHeap[mostActiveAtom] = false; + } + return mostActiveAtom; } /** @@ -241,7 +247,11 @@ 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 (choiceManager.isActiveChoiceAtom(atom)) { + numAddedToHeapByActivity++; + occursInHeap[atom] = true; + heap.add(atom); // ignores the fact that atom may already be in the heap for performance reasons (may be revised in future) + } } /** @@ -265,6 +275,10 @@ private void normalizeActivityScores() { return newActivity; } + long getNumAddedToHeapByActivity() { + return numAddedToHeapByActivity; + } + private class AtomActivityComparator implements Comparator { @Override @@ -277,14 +291,13 @@ 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] && 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 */ + occursInHeap[atom] = true; + heap.add(atom); } } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index a13c9e301..c5d35da34 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -147,6 +147,10 @@ public long getNumNotActiveChoicePoint() { return numNotActiveChoicePoint; } + public long getNumAddedToHeapByActivity() { + return heapOfActiveAtoms.getNumAddedToHeapByActivity(); + } + /** * {@link VSIDSWithPhaseSaving} works like {@link VSIDS} for selecting an atom but uses the saved phase to * determine the truth value to choose. diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java index 30df8b212..5583b3617 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java @@ -32,6 +32,7 @@ import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.ChoiceAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Pair; @@ -102,6 +103,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; @@ -115,6 +117,10 @@ public ChoiceGrounder(AtomStore atomStore, java.util.function.Predicate it) { public void forgetAssignment(int[] atomIds) { } + @Override + public AtomChoiceRelation getAtomChoiceRelation() { + return atomChoiceRelation; + } + private int solverDerivedNoGoodIdCounter = 20; private Map solverDerivedNoGoods = new HashMap<>(); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java index 418eb0ae6..621ee195a 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/DummyGrounder.java @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; +import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Pair; @@ -74,6 +75,7 @@ public class DummyGrounder implements Grounder { private static Atom atomCC = new BasicAtom(Predicate.getInstance("c", 0)); private static Rule ruleABC = new Rule(new DisjunctiveHead(Collections.singletonList(atomCC)), Arrays.asList(atomAA.toLiteral(), atomBB.toLiteral())); private static Atom rule1 = new RuleAtom(NonGroundRule.constructNonGroundRule(ruleABC), new Substitution()); + private static AtomChoiceRelation atomChoiceRelation = new AtomChoiceRelation(); private Set returnedNogoods = new HashSet<>(); public DummyGrounder(AtomStore atomStore) { @@ -104,6 +106,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 From a6ccf7018f86dcdb7df7fa3cce412ceea9be8302 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 12 Feb 2020 09:29:22 +0100 Subject: [PATCH 09/27] Fix merge ab122e3c340b1823a92b7af38e379e1e2881a441 --- .../ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java index 9b5e044ed..8d61f6530 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2018-2019 Siemens AG + * Copyright (c) 2018-2020 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -195,7 +195,7 @@ private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrd nonGroundRule.groundingOrder.groundingOrders.put(startingLiteral, groundingOrder); grounder.bootstrap(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore); + TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); final Substitution subst1 = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(1)), new Substitution()); final NaiveGrounder.BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, groundingOrder, subst1, currentAssignment); @@ -245,7 +245,7 @@ public void testGroundingOfRuleNotSwitchedOffByFalseNegativeBody() { */ private void testIfGrounderGroundsRule(Program program, int ruleID, Literal startingLiteral, int startingInstance, ThriceTruth bTruth, boolean expectNoGoods) { AtomStore atomStore = new AtomStoreImpl(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore); + TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, GrounderHeuristicsConfiguration.permissive(), true); int b = atomStore.putIfAbsent(atom("b", 1)); @@ -347,7 +347,7 @@ private void testPermissiveGrounderHeuristicTolerance(Program program, int ruleI */ private void testPermissiveGrounderHeuristicTolerance(Program program, int ruleID, Literal startingLiteral, int startingInstance, int tolerance, ThriceTruth[] truthsOfB, int arityOfB, boolean expectNoGoods, List expectedNumbersOfUnassignedPositiveBodyAtoms) { AtomStore atomStore = new AtomStoreImpl(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore); + TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); GrounderHeuristicsConfiguration heuristicConfiguration = GrounderHeuristicsConfiguration.getInstance(tolerance, tolerance); NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, heuristicConfiguration, true); @@ -393,7 +393,7 @@ private void assign(TrailAssignment currentAssignment, int[] atomIDs, ThriceTrut * and using this temporary assignment to update the grounder's working memory. */ private void addAtomsToWorkingMemoryWithoutChangingTheAssignment(AtomStore atomStore, NaiveGrounder grounder, int[] atomIDs) { - TrailAssignment temporaryAssignment = new TrailAssignment(atomStore); + TrailAssignment temporaryAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); temporaryAssignment.growForMaxAtomId(); for (int b : atomIDs) { temporaryAssignment.assign(b, TRUE); From c944b7e84ca0ccbdf1fd115e2afa694d709d0454 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Fri, 1 May 2020 20:36:26 +0200 Subject: [PATCH 10/27] Better toString in ChoiceRecorder. - Extend Util.join with toString method parameter. --- src/main/java/at/ac/tuwien/kr/alpha/Util.java | 7 ++++++- .../tuwien/kr/alpha/grounder/ChoiceRecorder.java | 14 +++++--------- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Util.java b/src/main/java/at/ac/tuwien/kr/alpha/Util.java index 358012221..f743a10e3 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Util.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/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; @@ -57,9 +58,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/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java index d4b223a60..408626395 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ChoiceRecorder.java @@ -27,6 +27,7 @@ */ package at.ac.tuwien.kr.alpha.grounder; +import at.ac.tuwien.kr.alpha.Util; import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; @@ -115,14 +116,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()).append(", "); - } - 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(); } } From 3770706b50d3a995dce15cf2ccf629b3e310d10e Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sat, 2 May 2020 03:25:58 +0200 Subject: [PATCH 11/27] Fix checkstyle. --- src/main/java/at/ac/tuwien/kr/alpha/Util.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Util.java b/src/main/java/at/ac/tuwien/kr/alpha/Util.java index f743a10e3..67c7cd848 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Util.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/Util.java @@ -61,7 +61,7 @@ public static String join(String prefix, Iterable iterable, String delimi return join(prefix, iterable, E::toString, delimiter, suffix); } - public static String join(String prefix, Iterable iterable, Function toStringMethod, String delimiter, String 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(toStringMethod.apply(element)); From f30057ae67fec94492b96f62b2d7eb5657c9c7e2 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sat, 2 May 2020 03:30:50 +0200 Subject: [PATCH 12/27] Add initial phase setting rules true, rest false. - Change initial phase values from strings to enum. - Add PhaseInitializer for RULESTRUEATOMSFALSE. --- .../kr/alpha/config/CommandLineParser.java | 3 +- .../tuwien/kr/alpha/config/SystemConfig.java | 3 +- .../tuwien/kr/alpha/solver/SolverFactory.java | 2 +- .../kr/alpha/solver/TrailAssignment.java | 2 +- .../heuristics/PhaseInitializerFactory.java | 46 +++++++++++++++---- 5 files changed, 43 insertions(+), 13 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java index 8c93d985f..b8e550cc0 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java @@ -29,6 +29,7 @@ import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.apache.commons.cli.CommandLine; import org.apache.commons.cli.DefaultParser; import org.apache.commons.cli.HelpFormatter; @@ -132,7 +133,7 @@ public class CommandLineParser { + SystemConfig.DEFAULT_ENABLE_RESTARTS + ")") .build(); private static final Option OPT_INITIAL_PHASE = Option.builder("ph").longOpt("initialPhase").hasArg(true).argName("initializer") - .desc("set the initial phase [ alltrue | allfalse | random ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + ")") + .desc("set the initial phase [ " + PhaseInitializerFactory.InitialPhase.listAllowedValues() + " ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + ")") .build(); //@formatter:on diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java index b189bd31b..b053f24fb 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java @@ -30,6 +30,7 @@ import at.ac.tuwien.kr.alpha.grounder.heuristics.GrounderHeuristicsConfiguration; import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import java.util.Arrays; import java.util.Collections; @@ -61,7 +62,7 @@ public class SystemConfig { public static final String DEFAULT_GROUNDER_TOLERANCE_RULES = GrounderHeuristicsConfiguration.STRICT_STRING; public static final boolean DEFAULT_GROUNDER_ACCUMULATOR_ENABLED = false; public static final boolean DEFAULT_ENABLE_RESTARTS = false; - public static final String DEFAULT_PHASE_INITIALIZER = "random"; + public static final String DEFAULT_PHASE_INITIALIZER = PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE.name().toLowerCase(); private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME; private String solverName = SystemConfig.DEFAULT_SOLVER_NAME; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java index 755ad8012..689728c9a 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java @@ -44,7 +44,7 @@ public static Solver getInstance(SystemConfig config, AtomStore atomStore, Groun final boolean debugInternalChecks = config.isDebugInternalChecks(); final HeuristicsConfiguration heuristicsConfiguration = buildHeuristicsConfiguration(config); final PhaseInitializerFactory.PhaseInitializer phaseInitializer = - PhaseInitializerFactory.getInstance(config.getPhaseInitializerName(), random); + PhaseInitializerFactory.getInstance(config.getPhaseInitializerName(), random, atomStore); final WritableAssignment assignment = new TrailAssignment(atomStore, phaseInitializer, debugInternalChecks); NoGoodStore store; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java index 0714640d0..48f9ceb76 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java @@ -469,7 +469,7 @@ public boolean getLastValue(int atom) { if (hasPhaseSet[atom]) { return phase[atom]; } - return phaseInitializer.getNextInitialPhase(); + return phaseInitializer.getNextInitialPhase(atom); } @Override diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java index 095f1435f..e10f5e9f1 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java @@ -1,6 +1,11 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; +import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; + +import java.util.Arrays; import java.util.Random; +import java.util.stream.Collectors; /** * Factory returning atom phase initializers, which determine the initial phase given to atoms that were previously @@ -10,18 +15,32 @@ */ public abstract class PhaseInitializerFactory { + public enum InitialPhase { + ALLTRUE, + ALLFALSE, + RANDOM, + RULESTRUEATOMSFALSE; + + public static String listAllowedValues() { + return Arrays.stream(values()).map(InitialPhase::toString).map(String::toLowerCase).collect(Collectors.joining(", ")); + } + } + public abstract static class PhaseInitializer { - public abstract boolean getNextInitialPhase(); + public abstract boolean getNextInitialPhase(int atom); } - public static PhaseInitializer getInstance(String phaseInitializerName, Random random) { - switch (phaseInitializerName.toLowerCase()) { - case "alltrue": + public static PhaseInitializer getInstance(String phaseInitializerName, Random random, AtomStore atomStore) { + InitialPhase initialPhase = InitialPhase.valueOf(phaseInitializerName.toUpperCase()); + switch (initialPhase) { + case ALLTRUE: return getPhaseInitializerAllTrue(); - case "allfalse": + case ALLFALSE: return getPhaseInitializerAllFalse(); - case "random": + case RANDOM: return getPhaseInitializerRandom(random); + case RULESTRUEATOMSFALSE: + return getPhaseInitializerRulesTrueRestFalse(atomStore); default: throw new IllegalArgumentException("Unknown phase initializer requested:" + phaseInitializerName); } @@ -30,7 +49,7 @@ public static PhaseInitializer getInstance(String phaseInitializerName, Random r public static PhaseInitializer getPhaseInitializerAllTrue() { return new PhaseInitializer() { @Override - public boolean getNextInitialPhase() { + public boolean getNextInitialPhase(int atom) { return true; } }; @@ -39,7 +58,7 @@ public boolean getNextInitialPhase() { private static PhaseInitializer getPhaseInitializerAllFalse() { return new PhaseInitializer() { @Override - public boolean getNextInitialPhase() { + public boolean getNextInitialPhase(int atom) { return false; } }; @@ -49,9 +68,18 @@ private static PhaseInitializer getPhaseInitializerRandom(Random random) { return new PhaseInitializer() { private final Random rand = random; @Override - public boolean getNextInitialPhase() { + 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. + } + }; + } } From 06500967e477d620df1446f674057184b840d95d Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sun, 3 May 2020 21:25:38 +0200 Subject: [PATCH 13/27] Address review comments and use array in AtomChoiceRelation. --- .../kr/alpha/grounder/NoGoodGenerator.java | 4 +--- .../grounder/ProgramAnalyzingGrounder.java | 7 ------ .../structure/AtomChoiceRelation.java | 24 +++++++++++++------ .../kr/alpha/grounder/ChoiceGrounder.java | 1 + 4 files changed, 19 insertions(+), 17 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java index 7a1e015ff..5fc6adb2e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/NoGoodGenerator.java @@ -127,10 +127,8 @@ List generateNoGoodsFromGroundSubstitution(final NonGroundRule nonGround // 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. - if (!negLiterals.isEmpty()) { + // Record atom-choiceAtom relationships for rules that are choice points. atomChoiceRelation.growForMaxAtomId(atomStore.getMaxAtomId()); atomChoiceRelation.addRelation(headId, atomOf(bodyRepresentingLiteral)); for (Integer negLiteral : negLiterals) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java index 57ba291e1..21295d1e7 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/ProgramAnalyzingGrounder.java @@ -3,7 +3,6 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; -import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import java.util.Set; @@ -33,10 +32,4 @@ public interface ProgramAnalyzingGrounder extends Grounder { * @return the corresponding NonGroundRule. */ NonGroundRule getNonGroundRule(Integer ruleId); - - /** - * Provides relationship information between atoms and choice points influencing their truth values. - * @return the {@link AtomChoiceRelation}. - */ - AtomChoiceRelation getAtomChoiceRelation(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java index 8db7941e2..fb5d34c00 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java @@ -1,31 +1,41 @@ package at.ac.tuwien.kr.alpha.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.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, and vice versa. * * Copyright (c) 2019, the Alpha Team. */ public class AtomChoiceRelation { - private final ArrayList> atomToChoiceAtoms = new ArrayList<>(); + @SuppressWarnings("unchecked") + private ArrayList[] atomToChoiceAtoms = new ArrayList[0]; public void addRelation(int atom, int bodyRepresentingAtom) { - while (atom > atomToChoiceAtoms.size() - 1) { - atomToChoiceAtoms.add(new ArrayList<>()); + if (atomToChoiceAtoms[atom] == null) { + atomToChoiceAtoms[atom] = new ArrayList<>(); } - atomToChoiceAtoms.get(atom).add(bodyRepresentingAtom); + atomToChoiceAtoms[atom].add(bodyRepresentingAtom); } public List getRelatedChoiceAtoms(int atom) { - return Collections.unmodifiableList(atomToChoiceAtoms.get(atom)); + return Collections.unmodifiableList(atomToChoiceAtoms[atom]); } public void growForMaxAtomId(int maxAtomId) { - while (maxAtomId > atomToChoiceAtoms.size() - 1) { - atomToChoiceAtoms.add(new ArrayList<>()); + if (maxAtomId >= atomToChoiceAtoms.length) { + int newCapacity = arrayGrowthSize(atomToChoiceAtoms.length); + if (newCapacity < maxAtomId + 1) { + newCapacity = maxAtomId + 1; + } + atomToChoiceAtoms = Arrays.copyOf(atomToChoiceAtoms, newCapacity); } } } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java index e4353fa3a..f91ee540d 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/ChoiceGrounder.java @@ -117,6 +117,7 @@ public ChoiceGrounder(AtomStore atomStore, java.util.function.Predicate Date: Mon, 4 May 2020 12:52:58 +0200 Subject: [PATCH 14/27] Remove unnecessary parameter of TrailAssignment. --- .../tuwien/kr/alpha/solver/TrailAssignment.java | 2 +- .../kr/alpha/grounder/NaiveGrounderTest.java | 15 +++++++-------- .../structure/AnalyzeUnjustifiedTest.java | 9 ++++----- .../kr/alpha/solver/ChoiceManagerTests.java | 3 +-- .../alpha/solver/LearnedNoGoodDeletionTest.java | 3 +-- .../kr/alpha/solver/NaiveNoGoodStoreTest.java | 3 +-- .../alpha/solver/NoGoodStoreAlphaRoamingTest.java | 3 +-- .../kr/alpha/solver/TrailAssignmentTest.java | 3 +-- .../heuristics/AlphaHeuristicTestAssumptions.java | 2 +- .../kr/alpha/solver/heuristics/BerkMinTest.java | 2 +- .../heuristics/BranchingHeuristicFactoryTest.java | 2 +- .../solver/heuristics/HeapOfActiveAtomsTest.java | 2 +- .../solver/heuristics/ReplayHeuristicTest.java | 2 +- .../kr/alpha/solver/heuristics/VSIDSTest.java | 2 +- .../learning/GroundConflictNoGoodLearnerTest.java | 3 +-- 15 files changed, 24 insertions(+), 32 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java index 48f9ceb76..daac8b30e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java @@ -117,7 +117,7 @@ public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitial assignmentsForChoicePosition = 0; } - public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitializer phaseInitializer) { + public TrailAssignment(AtomStore atomStore) { this(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue(), false); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java index 8d61f6530..6c9d6fb39 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounderTest.java @@ -39,7 +39,6 @@ import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Ignore; import org.junit.Test; @@ -85,7 +84,7 @@ public void groundRuleAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue())); + Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false); int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0)))); assertExistsNoGoodContaining(noGoods.values(), litCNeg); @@ -105,7 +104,7 @@ public void groundRuleWithLongerBodyAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue())); + Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); int litANeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("a", 0))), false); int litBNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0))), false); int litCNeg = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("c", 0))), false); @@ -128,7 +127,7 @@ public void groundConstraintAlreadyGround() { AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance("naive", program, atomStore, true); - Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue())); + Map noGoods = grounder.getNoGoods(new TrailAssignment(atomStore)); int litB = Literals.atomToLiteral(atomStore.get(new BasicAtom(Predicate.getInstance("b", 0)))); assertTrue(noGoods.containsValue(NoGood.fromConstraint(Collections.singletonList(litB), Collections.emptyList()))); } @@ -195,7 +194,7 @@ private void testDeadEnd(String predicateNameOfStartingLiteral, RuleGroundingOrd nonGroundRule.groundingOrder.groundingOrders.put(startingLiteral, groundingOrder); grounder.bootstrap(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment currentAssignment = new TrailAssignment(atomStore); final Substitution subst1 = Substitution.unify(startingLiteral, new Instance(ConstantTerm.getInstance(1)), new Substitution()); final NaiveGrounder.BindingResult bindingResult = grounder.getGroundInstantiations(nonGroundRule, groundingOrder, subst1, currentAssignment); @@ -245,7 +244,7 @@ public void testGroundingOfRuleNotSwitchedOffByFalseNegativeBody() { */ private void testIfGrounderGroundsRule(Program program, int ruleID, Literal startingLiteral, int startingInstance, ThriceTruth bTruth, boolean expectNoGoods) { AtomStore atomStore = new AtomStoreImpl(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment currentAssignment = new TrailAssignment(atomStore); NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, GrounderHeuristicsConfiguration.permissive(), true); int b = atomStore.putIfAbsent(atom("b", 1)); @@ -347,7 +346,7 @@ private void testPermissiveGrounderHeuristicTolerance(Program program, int ruleI */ private void testPermissiveGrounderHeuristicTolerance(Program program, int ruleID, Literal startingLiteral, int startingInstance, int tolerance, ThriceTruth[] truthsOfB, int arityOfB, boolean expectNoGoods, List expectedNumbersOfUnassignedPositiveBodyAtoms) { AtomStore atomStore = new AtomStoreImpl(); - TrailAssignment currentAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment currentAssignment = new TrailAssignment(atomStore); GrounderHeuristicsConfiguration heuristicConfiguration = GrounderHeuristicsConfiguration.getInstance(tolerance, tolerance); NaiveGrounder grounder = (NaiveGrounder) GrounderFactory.getInstance("naive", program, atomStore, p -> true, heuristicConfiguration, true); @@ -393,7 +392,7 @@ private void assign(TrailAssignment currentAssignment, int[] atomIDs, ThriceTrut * and using this temporary assignment to update the grounder's working memory. */ private void addAtomsToWorkingMemoryWithoutChangingTheAssignment(AtomStore atomStore, NaiveGrounder grounder, int[] atomIDs) { - TrailAssignment temporaryAssignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment temporaryAssignment = new TrailAssignment(atomStore); temporaryAssignment.growForMaxAtomId(); for (int b : atomIDs) { temporaryAssignment.assign(b, TRUE); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java b/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java index 3889603c3..7e346a90b 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustifiedTest.java @@ -39,7 +39,6 @@ import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Test; import java.util.Arrays; @@ -68,7 +67,7 @@ public void justifySimpleRules() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment assignment = new TrailAssignment(atomStore); int rId = atomStore.get(new BasicAtom(Predicate.getInstance("r", 0))); int nrId = atomStore.get(new BasicAtom(Predicate.getInstance("nr", 0))); assignment.growForMaxAtomId(); @@ -93,7 +92,7 @@ public void justifyLargerRules() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment assignment = new TrailAssignment(atomStore); Atom p1 = parser.parse("p(1).").getFacts().get(0); Atom r2 = parser.parse("r(2).").getFacts().get(0); Atom s12 = parser.parse("s(1,2).").getFacts().get(0); @@ -130,7 +129,7 @@ public void justifyMultipleReasons() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment assignment = new TrailAssignment(atomStore); Atom qa = parser.parse("q(a).").getFacts().get(0); Atom qb = parser.parse("q(b).").getFacts().get(0); Atom qc = parser.parse("q(c).").getFacts().get(0); @@ -186,7 +185,7 @@ public void justifyNegatedFactsRemovedFromReasons() { AtomStore atomStore = new AtomStoreImpl(); NaiveGrounder grounder = new NaiveGrounder(parsedProgram, atomStore, true); grounder.getNoGoods(null); - TrailAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + TrailAssignment assignment = new TrailAssignment(atomStore); int rId = atomStore.get(new BasicAtom(Predicate.getInstance("r", 0))); int nrId = atomStore.get(new BasicAtom(Predicate.getInstance("nr", 0))); assignment.growForMaxAtomId(); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java index 49e06f571..682ddb425 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/ChoiceManagerTests.java @@ -33,7 +33,6 @@ import at.ac.tuwien.kr.alpha.grounder.NaiveGrounder; import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Test; @@ -54,7 +53,7 @@ public void setUp() throws IOException { Program parsedProgram = new ProgramParser().parse(testProgram); this.atomStore = new AtomStoreImpl(); this.grounder = new NaiveGrounder(parsedProgram, atomStore, true); - WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + WritableAssignment assignment = new TrailAssignment(atomStore); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment); this.choiceManager = new ChoiceManager(assignment, store); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java index 2b48555f4..b6356c4f5 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java @@ -32,7 +32,6 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreTest; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Test; @@ -54,7 +53,7 @@ public class LearnedNoGoodDeletionTest { public LearnedNoGoodDeletionTest() { AtomStore atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 200); - WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + WritableAssignment assignment = new TrailAssignment(atomStore); assignment.growForMaxAtomId(); store = new NoGoodStoreAlphaRoaming(assignment); learnedNoGoodDeletion = store.getLearnedNoGoodDeletion(); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java index 5bc9477ca..33a069469 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStoreTest.java @@ -1,7 +1,6 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.*; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Ignore; import org.junit.Test; @@ -23,7 +22,7 @@ public class NaiveNoGoodStoreTest { public NaiveNoGoodStoreTest() { atomStore = new AtomStoreImpl(); - assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + assignment = new TrailAssignment(atomStore); store = new NaiveNoGoodStore(assignment); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java index 20f18ce43..0f6d73acf 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoamingTest.java @@ -1,7 +1,6 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.*; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Ignore; import org.junit.Test; @@ -25,7 +24,7 @@ public class NoGoodStoreAlphaRoamingTest { public NoGoodStoreAlphaRoamingTest() { atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 200); - assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + assignment = new TrailAssignment(atomStore); assignment.growForMaxAtomId(); store = new NoGoodStoreAlphaRoaming(assignment); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java index 14e02e87b..9cbda2250 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/TrailAssignmentTest.java @@ -32,7 +32,6 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.common.AtomStoreTest; import at.ac.tuwien.kr.alpha.common.IntIterator; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Before; import org.junit.Test; @@ -57,7 +56,7 @@ public class TrailAssignmentTest { public TrailAssignmentTest() { AtomStore atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 20); - assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + assignment = new TrailAssignment(atomStore); } @Before diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java index 7bebfc326..bfcd075b8 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/AlphaHeuristicTestAssumptions.java @@ -73,7 +73,7 @@ public void setUp() throws IOException { Program parsedProgram = new ProgramParser().parse(testProgram); this.atomStore = new AtomStoreImpl(); this.grounder = new NaiveGrounder(parsedProgram, atomStore, true); - this.assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + this.assignment = new TrailAssignment(atomStore); this.choiceManager = new TestableChoiceManager(assignment, new NaiveNoGoodStore(assignment)); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java index 5d660946e..29227058f 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMinTest.java @@ -62,7 +62,7 @@ public class BerkMinTest { public void setUp() { AtomStore atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 2); - WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + WritableAssignment assignment = new TrailAssignment(atomStore); assignment.growForMaxAtomId(); this.berkmin = new BerkMin( assignment, diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java index 8254e889d..519f14169 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java @@ -48,7 +48,7 @@ public class BranchingHeuristicFactoryTest { @Before public void setUp() { AtomStore atomStore = new AtomStoreImpl(); - WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + WritableAssignment assignment = new TrailAssignment(atomStore); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks); this.choiceManager = new ChoiceManager(assignment, store); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java index a8955bd78..a73882ed5 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtomsTest.java @@ -55,7 +55,7 @@ public class HeapOfActiveAtomsTest { @Before public void setUp() { atomStore = new AtomStoreImpl(); - assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + assignment = new TrailAssignment(atomStore); noGoodStore = new NoGoodStoreAlphaRoaming(assignment); ChoiceManager choiceManager = new PseudoChoiceManager(assignment, noGoodStore); this.vsids = new VSIDS(assignment, choiceManager, MOMs.DEFAULT_STRATEGY); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java index d6b8796a5..81ec7bbd1 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java @@ -48,7 +48,7 @@ public class ReplayHeuristicTest { @Before public void setUp() { AtomStore atomStore = new AtomStoreImpl(); - WritableAssignment assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + WritableAssignment assignment = new TrailAssignment(atomStore); NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks); this.choiceManager = new PseudoChoiceManager(assignment, store); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java index 71f10e96c..e4f4f714f 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSTest.java @@ -68,7 +68,7 @@ public class VSIDSTest { public void setUp() { atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 4); - assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + assignment = new TrailAssignment(atomStore); assignment.growForMaxAtomId(); noGoodStore = new NoGoodStoreAlphaRoaming(assignment); this.vsids = new VSIDS( diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java index 9ec7ecfdf..238894bbd 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearnerTest.java @@ -5,7 +5,6 @@ import at.ac.tuwien.kr.alpha.common.AtomStoreTest; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.*; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.junit.Ignore; import org.junit.Test; @@ -25,7 +24,7 @@ public class GroundConflictNoGoodLearnerTest { public GroundConflictNoGoodLearnerTest() { atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 20); - this.assignment = new TrailAssignment(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue()); + this.assignment = new TrailAssignment(atomStore); this.assignment.growForMaxAtomId(); this.store = new NoGoodStoreAlphaRoaming(assignment); this.store.growForMaxAtomId(20); From 7d992c24ff38aed48378f9718ad76752ee299720 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 4 May 2020 13:22:52 +0200 Subject: [PATCH 15/27] Fix NullPointerException in AtomChoiceRelation. --- .../tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java index fb5d34c00..65f506059 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java @@ -26,6 +26,9 @@ public void addRelation(int atom, int bodyRepresentingAtom) { } public List getRelatedChoiceAtoms(int atom) { + if (atomToChoiceAtoms[atom] == null) { + return Collections.emptyList(); + } return Collections.unmodifiableList(atomToChoiceAtoms[atom]); } From 48051e6b0c97fac4bbc47a7fe2b7ac08f0a032e6 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 5 May 2020 15:57:25 +0200 Subject: [PATCH 16/27] Make AtomChoiceRelation reflexive on choice atoms. --- .../kr/alpha/grounder/structure/AtomChoiceRelation.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java index 65f506059..5ce99c61b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AtomChoiceRelation.java @@ -10,7 +10,7 @@ /** * 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, and vice versa. + * values. Moreover, each body-representing atom is in relation with itself. * * Copyright (c) 2019, the Alpha Team. */ @@ -23,6 +23,12 @@ public void addRelation(int atom, int bodyRepresentingAtom) { 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) { From 058971555a33ba6736ea6fe85d1186aca22f59c3 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 May 2020 03:54:31 +0200 Subject: [PATCH 17/27] Clean-up logic in HeapOfActiveAtoms. --- .../solver/heuristics/HeapOfActiveAtoms.java | 26 +++++++++++-------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java index 8ffb5daac..2f120ad52 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeapOfActiveAtoms.java @@ -44,10 +44,12 @@ /** * 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); @@ -57,7 +59,7 @@ public class HeapOfActiveAtoms { static final double SCORE_EPSILON = 1E-100; boolean[] incrementedActivityScores = new boolean[0]; - boolean[] occursInHeap = 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()); @@ -215,7 +217,13 @@ private void initActivityNaive(NoGood newNoGood) { * Returns the atom with the highest activity score and removes it from the heap. */ Integer getMostActiveAtom() { - Integer mostActiveAtom = heap.poll(); + 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; } @@ -249,10 +257,9 @@ void setActivity(int atom, double newActivity) { normalizeActivityScores(); } - if (choiceManager.isActiveChoiceAtom(atom)) { + if (occursInHeap[atom]) { numAddedToHeapByActivity++; - occursInHeap[atom] = true; - heap.add(atom); // ignores the fact that atom may already be in the heap for performance reasons (may be revised in future) + heap.add(atom); // For performance reason ignores that the atom may already be in the heap. } } @@ -294,10 +301,7 @@ private class ChoicePointActivityListener implements ChoiceInfluenceManager.Acti @Override public void callbackOnChange(int atom) { - if (!occursInHeap[atom] && 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 */ + if (!occursInHeap[atom]) { occursInHeap[atom] = true; heap.add(atom); } From d9180c4671b1283a956f5ceaa01f37c57e8dd5bb Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 May 2020 05:11:01 +0200 Subject: [PATCH 18/27] Use default PhaseInitializer in TrailAssignment. --- .../java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java | 3 ++- .../kr/alpha/solver/heuristics/PhaseInitializerFactory.java | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java index daac8b30e..f20c818bd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.IntIterator; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.config.SystemConfig; import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -118,7 +119,7 @@ public TrailAssignment(AtomStore atomStore, PhaseInitializerFactory.PhaseInitial } public TrailAssignment(AtomStore atomStore) { - this(atomStore, PhaseInitializerFactory.getPhaseInitializerAllTrue(), false); + this(atomStore, PhaseInitializerFactory.getInstance(SystemConfig.DEFAULT_PHASE_INITIALIZER, null, atomStore), false); } @Override diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java index e10f5e9f1..e3301adf5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java @@ -46,7 +46,7 @@ public static PhaseInitializer getInstance(String phaseInitializerName, Random r } } - public static PhaseInitializer getPhaseInitializerAllTrue() { + private static PhaseInitializer getPhaseInitializerAllTrue() { return new PhaseInitializer() { @Override public boolean getNextInitialPhase(int atom) { From 4b8566a2af9c130d60762ac48fa0c2bd6cedfa29 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Thu, 7 May 2020 03:01:14 +0200 Subject: [PATCH 19/27] Small polish. --- .../solver/heuristics/ChainedBranchingHeuristics.java | 8 ++++---- .../kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java index 7413c871f..f38f138ce 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ChainedBranchingHeuristics.java @@ -102,6 +102,10 @@ public void add(BranchingHeuristic element) { } } + public BranchingHeuristic getFirstElement() { + return chain.get(0); + } + public BranchingHeuristic getLastElement() { return chain.get(chain.size() - 1); } @@ -110,10 +114,6 @@ public static ChainedBranchingHeuristics chainOf(BranchingHeuristic... branching return new ChainedBranchingHeuristics(branchingHeuristics); } - public BranchingHeuristic getFirstElement() { - return chain.get(0); - } - /** * Returns a mapping from individual heuristics to number of decisions made by them. */ diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index c5d35da34..229cbc1aa 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -176,8 +176,8 @@ private int chooseAtom() { } if (choiceManager.isActiveChoiceAtom(mostActiveAtom)) { if (maxActivity > activity) { - double lostActitivyNormalized = (maxActivity - activity) / heapOfActiveAtoms.getCurrentActivityIncrement(); - activityDecrease += lostActitivyNormalized; + double lostActivityNormalized = (maxActivity - activity) / heapOfActiveAtoms.getCurrentActivityIncrement(); + activityDecrease += lostActivityNormalized; } return mostActiveAtom; } From e63651aa35d9f5a2206a47e2647612b4dd79d364 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Thu, 7 May 2020 09:13:52 +0200 Subject: [PATCH 20/27] Use enum instead of string for default initial phase --- .../kr/alpha/config/CommandLineParser.java | 12 +++++-- .../tuwien/kr/alpha/config/SystemConfig.java | 16 ++++++---- .../tuwien/kr/alpha/solver/SolverFactory.java | 6 ++-- .../heuristics/PhaseInitializerFactory.java | 32 +++++++++++++++++-- 4 files changed, 51 insertions(+), 15 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java index b8e550cc0..fb7373101 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java @@ -1,4 +1,4 @@ -/** +/* * Copyright (c) 2016-2020, the Alpha Team. * All rights reserved. * @@ -426,7 +426,13 @@ private void handleEnableRestarts(Option opt, SystemConfig cfg) { cfg.setRestartsEnabled(true); } - private void handleInitialPhase(Option opt, SystemConfig cfg) { - cfg.setPhaseInitializer(opt.getValue(SystemConfig.DEFAULT_PHASE_INITIALIZER)); + 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: " + + PhaseInitializerFactory.InitialPhase.listAllowedValues()); + } } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java index b053f24fb..e97082d2c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/SystemConfig.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. @@ -62,7 +62,7 @@ public class SystemConfig { public static final String DEFAULT_GROUNDER_TOLERANCE_RULES = GrounderHeuristicsConfiguration.STRICT_STRING; public static final boolean DEFAULT_GROUNDER_ACCUMULATOR_ENABLED = false; public static final boolean DEFAULT_ENABLE_RESTARTS = false; - public static final String DEFAULT_PHASE_INITIALIZER = PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE.name().toLowerCase(); + public static final PhaseInitializerFactory.InitialPhase DEFAULT_PHASE_INITIALIZER = PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE; private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME; private String solverName = SystemConfig.DEFAULT_SOLVER_NAME; @@ -83,7 +83,7 @@ public class SystemConfig { private String grounderToleranceRules = DEFAULT_GROUNDER_TOLERANCE_RULES; private boolean grounderAccumulatorEnabled = DEFAULT_GROUNDER_ACCUMULATOR_ENABLED; private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS; - private String phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER; + private PhaseInitializerFactory.InitialPhase phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER; public String getGrounderName() { return this.grounderName; @@ -248,12 +248,16 @@ public void setRestartsEnabled(boolean areRestartsEnabled) { this.areRestartsEnabled = areRestartsEnabled; } - public String getPhaseInitializerName() { + public PhaseInitializerFactory.InitialPhase getPhaseInitializer() { return phaseInitializer; } - public void setPhaseInitializer(String phaseInitializer) { + public void setPhaseInitializer(PhaseInitializerFactory.InitialPhase phaseInitializer) { this.phaseInitializer = phaseInitializer; } + public void setPhaseInitializerName(String phaseInitializerName) { + this.phaseInitializer = PhaseInitializerFactory.InitialPhase.valueOf(phaseInitializerName.toUpperCase()); + } + } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java index 689728c9a..70d784a2a 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/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. @@ -44,7 +44,7 @@ public static Solver getInstance(SystemConfig config, AtomStore atomStore, Groun final boolean debugInternalChecks = config.isDebugInternalChecks(); final HeuristicsConfiguration heuristicsConfiguration = buildHeuristicsConfiguration(config); final PhaseInitializerFactory.PhaseInitializer phaseInitializer = - PhaseInitializerFactory.getInstance(config.getPhaseInitializerName(), random, atomStore); + PhaseInitializerFactory.getInstance(config.getPhaseInitializer(), random, atomStore); final WritableAssignment assignment = new TrailAssignment(atomStore, phaseInitializer, debugInternalChecks); NoGoodStore store; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java index e3301adf5..47785a0fa 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java @@ -1,3 +1,30 @@ +/* + * 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.solver.heuristics; import at.ac.tuwien.kr.alpha.common.AtomStore; @@ -30,8 +57,7 @@ public abstract static class PhaseInitializer { public abstract boolean getNextInitialPhase(int atom); } - public static PhaseInitializer getInstance(String phaseInitializerName, Random random, AtomStore atomStore) { - InitialPhase initialPhase = InitialPhase.valueOf(phaseInitializerName.toUpperCase()); + public static PhaseInitializer getInstance(InitialPhase initialPhase, Random random, AtomStore atomStore) { switch (initialPhase) { case ALLTRUE: return getPhaseInitializerAllTrue(); @@ -42,7 +68,7 @@ public static PhaseInitializer getInstance(String phaseInitializerName, Random r case RULESTRUEATOMSFALSE: return getPhaseInitializerRulesTrueRestFalse(atomStore); default: - throw new IllegalArgumentException("Unknown phase initializer requested:" + phaseInitializerName); + throw new IllegalArgumentException("Unknown phase initializer requested:" + initialPhase); } } From 2e26f69d5e8cbd0416f29dfb8d2b133f3e1345db Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Thu, 7 May 2020 09:52:26 +0200 Subject: [PATCH 21/27] Test parsing of -ph CLI parameter --- .../alpha/config/CommandLineParserTest.java | 33 +++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java b/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java index 65fcb7264..76e75b58c 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/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,6 +27,7 @@ */ package at.ac.tuwien.kr.alpha.config; +import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; import org.apache.commons.cli.ParseException; import org.junit.Test; @@ -148,4 +149,32 @@ public void noInstanceRemoval() throws ParseException { assertTrue(alphaConfig.getAlphaConfig().isGrounderAccumulatorEnabled()); } + @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(PhaseInitializerFactory.InitialPhase.ALLTRUE, alphaConfig.getAlphaConfig().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(PhaseInitializerFactory.InitialPhase.ALLFALSE, alphaConfig.getAlphaConfig().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(PhaseInitializerFactory.InitialPhase.RANDOM, alphaConfig.getAlphaConfig().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(PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE, alphaConfig.getAlphaConfig().getPhaseInitializer()); + } + } From 340ae36772ee47e5362eeb30fcbe5e2ddeec8393 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Thu, 7 May 2020 13:50:43 +0200 Subject: [PATCH 22/27] Small polish. --- .../alpha/solver/heuristics/PhaseInitializerFactory.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java index e3301adf5..3fb6af7e5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/PhaseInitializerFactory.java @@ -31,7 +31,10 @@ public abstract static class PhaseInitializer { } public static PhaseInitializer getInstance(String phaseInitializerName, Random random, AtomStore atomStore) { - InitialPhase initialPhase = InitialPhase.valueOf(phaseInitializerName.toUpperCase()); + return getInstance(InitialPhase.valueOf(phaseInitializerName.toUpperCase()), random, atomStore); + } + + public static PhaseInitializer getInstance(InitialPhase initialPhase, Random random, AtomStore atomStore) { switch (initialPhase) { case ALLTRUE: return getPhaseInitializerAllTrue(); @@ -42,7 +45,7 @@ public static PhaseInitializer getInstance(String phaseInitializerName, Random r case RULESTRUEATOMSFALSE: return getPhaseInitializerRulesTrueRestFalse(atomStore); default: - throw new IllegalArgumentException("Unknown phase initializer requested:" + phaseInitializerName); + throw new IllegalArgumentException("Unknown phase initializer requested:" + initialPhase.name()); } } From e968afabab6e6bd4fa8127b7ae8c19923e6d94da Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 20 Sep 2021 22:58:19 +0200 Subject: [PATCH 23/27] Improve cmdline description of initial_phase flag. --- .../java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java index fb7373101..17e22f160 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java @@ -133,7 +133,8 @@ public class CommandLineParser { + 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 [ " + PhaseInitializerFactory.InitialPhase.listAllowedValues() + " ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + ")") + .desc("set the initial phase [ " + PhaseInitializerFactory.InitialPhase.listAllowedValues() + " ] (default: " + SystemConfig.DEFAULT_PHASE_INITIALIZER + "). " + + "Note: only works in conjunction with the " + Heuristic.VSIDS_PHASE_SAVING + " branching heuristic.") .build(); //@formatter:on From 725734899319e34e43498776befbb98550c01c3f Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 21 Sep 2021 03:50:17 +0200 Subject: [PATCH 24/27] Fix merge conflicts. --- .../tuwien/kr/alpha/config/CommandLineParser.java | 5 +---- .../kr/alpha/config/CommandLineParserTest.java | 14 +++++++------- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java index 0c45bc356..369938bbe 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/config/CommandLineParser.java @@ -27,6 +27,7 @@ */ package at.ac.tuwien.kr.alpha.config; +import at.ac.tuwien.kr.alpha.grounder.transformation.aggregates.AggregateRewritingConfig; import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; @@ -48,10 +49,6 @@ import java.util.Map; import java.util.function.Consumer; -import at.ac.tuwien.kr.alpha.grounder.transformation.aggregates.AggregateRewritingConfig; -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 SystemConfig}s and * {@link InputConfig}s. diff --git a/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java b/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java index fd30e6ff7..a8b624caa 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/config/CommandLineParserTest.java @@ -31,14 +31,14 @@ import org.apache.commons.cli.ParseException; import org.junit.jupiter.api.Test; +import java.util.Arrays; +import java.util.function.Consumer; + 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 java.util.Arrays; -import java.util.function.Consumer; - public class CommandLineParserTest { @@ -185,28 +185,28 @@ public void atomSeparator() throws ParseException { 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(PhaseInitializerFactory.InitialPhase.ALLTRUE, alphaConfig.getAlphaConfig().getPhaseInitializer()); + assertEquals(PhaseInitializerFactory.InitialPhase.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(PhaseInitializerFactory.InitialPhase.ALLFALSE, alphaConfig.getAlphaConfig().getPhaseInitializer()); + assertEquals(PhaseInitializerFactory.InitialPhase.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(PhaseInitializerFactory.InitialPhase.RANDOM, alphaConfig.getAlphaConfig().getPhaseInitializer()); + assertEquals(PhaseInitializerFactory.InitialPhase.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(PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE, alphaConfig.getAlphaConfig().getPhaseInitializer()); + assertEquals(PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE, alphaConfig.getSystemConfig().getPhaseInitializer()); } } From af8a9444a934a6e273d7624e573dcecdbe023642 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 Oct 2021 14:03:16 +0200 Subject: [PATCH 25/27] Refactor VSIDS implementations, extract common fields and methods. - Introduced AbstractVSIDS, bundling code common to all VSIDS implementations. - VSIDS refactored and extends AbstractVSIDS now. - VSIDSWithPhaseSaving refactored and extends AbstractVSIDS now. --- .../solver/heuristics/AbstractVSIDS.java | 101 ++++++++++++++++++ .../kr/alpha/solver/heuristics/VSIDS.java | 97 +++-------------- .../heuristics/VSIDSWithPhaseSaving.java | 82 +++----------- 3 files changed, 128 insertions(+), 152 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AbstractVSIDS.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AbstractVSIDS.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AbstractVSIDS.java new file mode 100644 index 000000000..be41e4adf --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/AbstractVSIDS.java @@ -0,0 +1,101 @@ +package at.ac.tuwien.kr.alpha.solver.heuristics; + +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; +import at.ac.tuwien.kr.alpha.solver.ChoiceManager; +import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProvider; + +import java.util.ArrayList; +import java.util.Collection; + +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; + +/** + * 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, BinaryNoGoodPropagationEstimation.Strategy 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(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/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java index 16b5f0daa..193cbd3c3 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDS.java @@ -26,23 +26,17 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; -import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProvider; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; -import org.apache.commons.collections4.MultiValuedMap; -import org.apache.commons.collections4.multimap.HashSetValuedHashMap; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.ArrayList; import java.util.Arrays; -import java.util.Collection; import static at.ac.tuwien.kr.alpha.Util.arrayGrowthSize; -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.isPositive; /** * This implementation is inspired by the VSIDS implementation in clasp. @@ -58,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, BinaryNoGoodPropagationEstimation.Strategy 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, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { @@ -102,57 +72,17 @@ public VSIDS(Assignment assignment, ChoiceManager choiceManager, BinaryNoGoodPro } @Override - public void violatedNoGood(NoGood violatedNoGood) { + protected void incrementActivityResolutionAtom(int resolutionAtom) { + heapOfActiveAtoms.incrementActivity(resolutionAtom); } @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(); + protected void incrementActivityLearnedNoGood(int literal) { + incrementSignCounter(literal); + heapOfActiveAtoms.incrementActivity(atomOf(literal)); } @Override - public void newNoGood(NoGood newNoGood) { - this.bufferedNoGoods.add(newNoGood); - } - - @Override - public void newNoGoods(Collection newNoGoods) { - this.bufferedNoGoods.addAll(newNoGoods); - } - - 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; @@ -178,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); @@ -186,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); } @@ -209,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); @@ -221,13 +152,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/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index 229cbc1aa..a6a4ea3bf 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -26,55 +26,34 @@ package at.ac.tuwien.kr.alpha.solver.heuristics; import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; import at.ac.tuwien.kr.alpha.solver.ChoiceManager; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; -import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.ArrayList; -import java.util.Collection; - import static at.ac.tuwien.kr.alpha.Util.oops; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; /** - * This implementation is like {@link VSIDS} but uses the saved phase for the truth of the chosen atom. + * This implementation is similar to {@link VSIDS} but uses the saved phase for the truth of the chosen atom. * - * Copyright (c) 2019, the Alpha Team. + * Copyright (c) 2019-2021, the Alpha Team. */ -public class VSIDSWithPhaseSaving implements ActivityBasedBranchingHeuristic { +public class VSIDSWithPhaseSaving extends AbstractVSIDS { protected static final Logger LOGGER = LoggerFactory.getLogger(VSIDSWithPhaseSaving.class); - private 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. - */ - private static final double DEFAULT_DECAY_FACTOR = 1 / 0.92; - - protected final Assignment assignment; - protected final ChoiceManager choiceManager; private final AtomChoiceRelation atomChoiceRelation; - private final HeapOfActiveAtoms heapOfActiveAtoms; - private final Collection bufferedNoGoods = new ArrayList<>(); - private double activityDecrease; private long numThrownAway; private long numNoChoicePoint; private long numNotActiveChoicePoint; private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { - this.assignment = assignment; - this.choiceManager = choiceManager; + super(assignment, choiceManager, heapOfActiveAtoms, momsStrategy); this.atomChoiceRelation = atomChoiceRelation; - this.heapOfActiveAtoms = heapOfActiveAtoms; - this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy); } private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { @@ -86,27 +65,19 @@ private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, } @Override - public void violatedNoGood(NoGood violatedNoGood) { + protected void incrementActivityResolutionAtom(int resolutionAtom) { + incrementActivityOfRelatedChoiceAtoms(resolutionAtom); } @Override - public void analyzedConflict(ConflictAnalysisResult analysisResult) { - ingestBufferedNoGoods(); //analysisResult may contain new atoms whose activity must be initialized - for (int resolutionAtom : analysisResult.resolutionAtoms) { - incrementActivityOfRelatedChoiceAtoms(resolutionAtom); - } - if (analysisResult.learnedNoGood != null) { - for (int literal : analysisResult.learnedNoGood) { - incrementActivityOfRelatedChoiceAtoms(atomOf(literal)); - } - } - heapOfActiveAtoms.decayIfTimeHasCome(); + protected void incrementActivityLearnedNoGood(int literal) { + incrementActivityOfRelatedChoiceAtoms(atomOf(literal)); } private void incrementActivityOfRelatedChoiceAtoms(int toAtom) { if (atomChoiceRelation == null) { heapOfActiveAtoms.incrementActivity(toAtom); - return; + throw new RuntimeException("Condition met: atomChoiceRelation is null."); } for (Integer relatedChoiceAtom : atomChoiceRelation.getRelatedChoiceAtoms(toAtom)) { if (!choiceManager.isAtomChoice(relatedChoiceAtom)) { @@ -116,21 +87,6 @@ private void incrementActivityOfRelatedChoiceAtoms(int toAtom) { } } - @Override - public void newNoGood(NoGood newNoGood) { - this.bufferedNoGoods.add(newNoGood); - } - - @Override - public void newNoGoods(Collection newNoGoods) { - this.bufferedNoGoods.addAll(newNoGoods); - } - - private void ingestBufferedNoGoods() { - heapOfActiveAtoms.newNoGoods(bufferedNoGoods); - bufferedNoGoods.clear(); - } - public double getActivityDecrease() { return activityDecrease; } @@ -151,21 +107,8 @@ public long getNumAddedToHeapByActivity() { return heapOfActiveAtoms.getNumAddedToHeapByActivity(); } - /** - * {@link VSIDSWithPhaseSaving} works like {@link VSIDS} for selecting an atom but uses the saved phase to - * determine the truth value to choose. - */ @Override - public int chooseLiteral() { - int atom = chooseAtom(); - if (atom == DEFAULT_CHOICE_ATOM) { - return DEFAULT_CHOICE_LITERAL; - } - boolean sign = chooseSign(atom); - return atomToLiteral(atom, sign); - } - - private int chooseAtom() { + protected int chooseAtom() { ingestBufferedNoGoods(); Integer mostActiveAtom; double maxActivity = 0.0f; @@ -199,7 +142,8 @@ private int chooseAtom() { * the chosen atom * @return the truth value to assign to the given atom */ - private boolean chooseSign(int atom) { + @Override + protected boolean chooseSign(int atom) { if (assignment.getTruth(atom) == ThriceTruth.MBT) { return true; } @@ -207,7 +151,7 @@ private boolean chooseSign(int atom) { } public void growForMaxAtomId(int maxAtomId) { - heapOfActiveAtoms.growForMaxAtomId(maxAtomId); + super.growForMaxAtomId(maxAtomId); if (atomChoiceRelation != null) { atomChoiceRelation.growForMaxAtomId(maxAtomId); } From 419b8194d5001e5747fe8e9bd1bc211a8bd160d0 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 Oct 2021 14:06:08 +0200 Subject: [PATCH 26/27] Fix copyright statement as per review request. --- .../heuristics/VSIDSWithPhaseSaving.java | 25 ------------------- 1 file changed, 25 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java index a6a4ea3bf..51c082656 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/VSIDSWithPhaseSaving.java @@ -1,28 +1,3 @@ -/** - * Copyright (c) 2018-2019 Siemens AG - * All rights reserved. - * - * 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.solver.heuristics; import at.ac.tuwien.kr.alpha.common.Assignment; From fcd2436c8b92f6ff92f7214ff42b8b97fd39bb6c Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sun, 5 Dec 2021 05:04:43 +0100 Subject: [PATCH 27/27] Modularize phase saving and fix merge. - Extract InitialAtomPhase from PhaseInitializerFactory. - Fix missing/wrong imports. --- .../tuwien/kr/alpha/api/config/Heuristic.java | 3 +- .../kr/alpha/api/config/InitialAtomPhase.java | 24 ++++++++++++++ .../kr/alpha/api/config/SystemConfig.java | 19 +++++------- .../alpha/app/config/CommandLineParser.java | 31 +++++++++---------- .../app/config/CommandLineParserTest.java | 25 +++++++-------- .../alpha/core/grounder/ChoiceRecorder.java | 13 ++++++-- .../structure/AtomChoiceRelation.java | 2 +- .../core/solver/MixedRestartStrategy.java | 8 ++--- .../kr/alpha/core/solver/PerformanceLog.java | 6 ++-- .../kr/alpha/core/solver/TrailAssignment.java | 31 +++++++++---------- .../core/solver/heuristics/AbstractVSIDS.java | 18 +++++------ .../AlphaHeadMustBeTrueHeuristic.java | 2 +- .../heuristics/HeapOfRelatedChoiceAtoms.java | 8 ++--- .../heuristics/PhaseInitializerFactory.java | 20 +++--------- .../alpha/core/solver/heuristics/VSIDS.java | 25 +++++---------- .../heuristics/VSIDSWithPhaseSaving.java | 22 ++++++------- 16 files changed, 130 insertions(+), 127 deletions(-) create mode 100644 alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/InitialAtomPhase.java rename alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/{programs => grounder}/structure/AtomChoiceRelation.java (95%) 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 54b4596f5..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 @@ -27,18 +27,13 @@ */ 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; -import at.ac.tuwien.kr.alpha.core.grounder.heuristics.GrounderHeuristicsConfiguration; -import at.ac.tuwien.kr.alpha.core.grounder.transformation.aggregates.AggregateRewritingConfig; -import at.ac.tuwien.kr.alpha.core.solver.BinaryNoGoodPropagationEstimation; -import at.ac.tuwien.kr.alpha.core.solver.heuristics.BranchingHeuristicFactory.Heuristic; -import at.ac.tuwien.kr.alpha.core.solver.heuristics.PhaseInitializerFactory; - /** * Config structure for {@link Alpha} instances. * @@ -70,7 +65,7 @@ public class SystemConfig { 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 PhaseInitializerFactory.InitialPhase DEFAULT_PHASE_INITIALIZER = PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE; + public static final InitialAtomPhase DEFAULT_PHASE_INITIALIZER = InitialAtomPhase.RULESTRUEATOMSFALSE; private String grounderName = DEFAULT_GROUNDER_NAME; private String solverName = DEFAULT_SOLVER_NAME; @@ -93,7 +88,7 @@ public class SystemConfig { private String atomSeparator = DEFAULT_ATOM_SEPARATOR; private AggregateRewritingConfig aggregateRewritingConfig = DEFAULT_AGGREGATE_REWRITING_CONFIG; private boolean areRestartsEnabled = SystemConfig.DEFAULT_ENABLE_RESTARTS; - private PhaseInitializerFactory.InitialPhase phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER; + private InitialAtomPhase phaseInitializer = SystemConfig.DEFAULT_PHASE_INITIALIZER; public String getGrounderName() { return this.grounderName; @@ -297,15 +292,15 @@ public void setRestartsEnabled(boolean areRestartsEnabled) { this.areRestartsEnabled = areRestartsEnabled; } - public PhaseInitializerFactory.InitialPhase getPhaseInitializer() { + public InitialAtomPhase getPhaseInitializer() { return phaseInitializer; } - public void setPhaseInitializer(PhaseInitializerFactory.InitialPhase phaseInitializer) { + public void setPhaseInitializer(InitialAtomPhase phaseInitializer) { this.phaseInitializer = phaseInitializer; } public void setPhaseInitializerName(String phaseInitializerName) { - this.phaseInitializer = PhaseInitializerFactory.InitialPhase.valueOf(phaseInitializerName.toUpperCase()); + 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 22e623e4e..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 @@ -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,13 +45,12 @@ 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 at.ac.tuwien.kr.alpha.commons.solver.heuristics.PhaseInitializerFactory; +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; /** @@ -156,7 +155,7 @@ public class CommandLineParser { + 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 [ " + PhaseInitializerFactory.InitialPhase.listAllowedValues() + " ] (default: " + SystemConfig.DEFAULT_PHASE_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 @@ -495,7 +494,7 @@ private void handleInitialPhase(Option opt, SystemConfig cfg) throws ParseExcept cfg.setPhaseInitializerName(initialPhase); } catch (IllegalArgumentException e) { throw new ParseException("Unknown initial phase: " + initialPhase + ". Please try one of the following: " - + PhaseInitializerFactory.InitialPhase.listAllowedValues()); + + 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 faf8ca91a..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 @@ -27,19 +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 at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; +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 { @@ -186,28 +185,28 @@ public void atomSeparator() throws ParseException { 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(PhaseInitializerFactory.InitialPhase.ALLTRUE, alphaConfig.getSystemConfig().getPhaseInitializer()); + 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(PhaseInitializerFactory.InitialPhase.ALLFALSE, alphaConfig.getSystemConfig().getPhaseInitializer()); + 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(PhaseInitializerFactory.InitialPhase.RANDOM, alphaConfig.getSystemConfig().getPhaseInitializer()); + 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(PhaseInitializerFactory.InitialPhase.RULESTRUEATOMSFALSE, alphaConfig.getSystemConfig().getPhaseInitializer()); + assertEquals(InitialAtomPhase.RULESTRUEATOMSFALSE, alphaConfig.getSystemConfig().getPhaseInitializer()); } } 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 b4d1502ea..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 { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/structure/AtomChoiceRelation.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AtomChoiceRelation.java similarity index 95% rename from alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/structure/AtomChoiceRelation.java rename to alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AtomChoiceRelation.java index 49c0f8beb..d5b8e7a63 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/structure/AtomChoiceRelation.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/structure/AtomChoiceRelation.java @@ -5,7 +5,7 @@ import java.util.Collections; import java.util.List; -import static at.ac.tuwien.kr.alpha.Util.arrayGrowthSize; +import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; /** * Stores and provides relationships between ordinary atoms and those that represent choice points. 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 index fd9c635d0..058888fdc 100644 --- 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 @@ -1,7 +1,7 @@ package at.ac.tuwien.kr.alpha.core.solver; -import static at.ac.tuwien.kr.alpha.Util.oops; -import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE; +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. @@ -59,9 +59,9 @@ void newConflictWithLbd(int lbd) { throw oops("Conflict has no LBD value."); } fast -= fast >> 5; - fast += lbd << (32 - 5); + fast += (long) lbd << (32 - 5); slow -= slow >> 14; - slow += lbd << (32 - 14); + slow += (long) lbd << (32 - 14); } int getTotalRestarts() { 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 5ca54f4b9..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,9 +25,9 @@ */ package at.ac.tuwien.kr.alpha.core.solver; -import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristic; -import at.ac.tuwien.kr.alpha.solver.heuristics.ChainedBranchingHeuristics; -import at.ac.tuwien.kr.alpha.solver.heuristics.VSIDSWithPhaseSaving; +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; /** 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 2fc0f6c73..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,22 +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 at.ac.tuwien.kr.alpha.config.SystemConfig; -import at.ac.tuwien.kr.alpha.solver.heuristics.PhaseInitializerFactory; -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. 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 index 8096ef90b..c6bba298c 100644 --- 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 @@ -1,16 +1,16 @@ package at.ac.tuwien.kr.alpha.core.solver.heuristics; -import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; -import at.ac.tuwien.kr.alpha.solver.ChoiceManager; -import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProvider; +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.common.Literals.atomToLiteral; -import static at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; +import static at.ac.tuwien.kr.alpha.core.atoms.Literals.atomToLiteral; /** * Combines fields and methods common to several VSIDS variants. @@ -29,7 +29,7 @@ public abstract class AbstractVSIDS implements ActivityBasedBranchingHeuristic { protected final HeapOfActiveAtoms heapOfActiveAtoms; protected final Collection bufferedNoGoods = new ArrayList<>(); - public AbstractVSIDS(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + public AbstractVSIDS(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { this.assignment = assignment; this.choiceManager = choiceManager; this.heapOfActiveAtoms = heapOfActiveAtoms; @@ -78,7 +78,7 @@ public int chooseLiteral() { } @Override - public void analyzedConflict(ConflictAnalysisResult analysisResult) { + 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); 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 c56e33a54..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,7 +36,7 @@ import java.util.Set; import java.util.stream.Stream; -import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +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 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 index c1c5bfa26..48675b412 100644 --- 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 @@ -1,10 +1,10 @@ package at.ac.tuwien.kr.alpha.core.solver.heuristics; -import at.ac.tuwien.kr.alpha.common.NoGood; -import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; -import at.ac.tuwien.kr.alpha.solver.ChoiceManager; +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.common.Literals.atomOf; +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. 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 index 8cc93131c..4398c3026 100644 --- 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 @@ -27,12 +27,11 @@ */ package at.ac.tuwien.kr.alpha.core.solver.heuristics; -import at.ac.tuwien.kr.alpha.common.AtomStore; -import at.ac.tuwien.kr.alpha.grounder.atoms.RuleAtom; +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.Arrays; import java.util.Random; -import java.util.stream.Collectors; /** * Factory returning atom phase initializers, which determine the initial phase given to atoms that were previously @@ -42,22 +41,11 @@ */ public abstract class PhaseInitializerFactory { - public enum InitialPhase { - ALLTRUE, - ALLFALSE, - RANDOM, - RULESTRUEATOMSFALSE; - - public static String listAllowedValues() { - return Arrays.stream(values()).map(InitialPhase::toString).map(String::toLowerCase).collect(Collectors.joining(", ")); - } - } - public abstract static class PhaseInitializer { public abstract boolean getNextInitialPhase(int atom); } - public static PhaseInitializer getInstance(InitialPhase initialPhase, Random random, AtomStore atomStore) { + public static PhaseInitializer getInstance(InitialAtomPhase initialPhase, Random random, AtomStore atomStore) { switch (initialPhase) { case ALLTRUE: return getPhaseInitializerAllTrue(); 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 19b63bdba..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. 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 index 727155eea..40c9b97f6 100644 --- 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 @@ -1,16 +1,16 @@ package at.ac.tuwien.kr.alpha.core.solver.heuristics; -import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.grounder.structure.AtomChoiceRelation; -import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; -import at.ac.tuwien.kr.alpha.solver.ChoiceManager; -import at.ac.tuwien.kr.alpha.solver.ThriceTruth; +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.Util.oops; -import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; -import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +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. @@ -26,16 +26,16 @@ public class VSIDSWithPhaseSaving extends AbstractVSIDS { private long numNoChoicePoint; private long numNotActiveChoicePoint; - private VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + 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, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + 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, BinaryNoGoodPropagationEstimation.Strategy momsStrategy) { + VSIDSWithPhaseSaving(Assignment assignment, ChoiceManager choiceManager, AtomChoiceRelation atomChoiceRelation, BinaryNoGoodPropagationEstimationStrategy momsStrategy) { this(assignment, choiceManager, atomChoiceRelation, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR, momsStrategy); }