From 32e7ec92535b6c69f4965ef353c2da08cbed75d3 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 12 Sep 2018 16:25:26 +0200 Subject: [PATCH 01/36] Re-enable some unit tests that were disabled to save resources during CI --- .../at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 7 +++++-- .../ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 3 +-- .../at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java | 10 +++------- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index 45b8f9d58..fb19b69e9 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -48,26 +48,29 @@ * Tests {@link AbstractSolver} using some hanoi tower test cases (see https://en.wikipedia.org/wiki/Tower_of_Hanoi). * */ -@Ignore("disabled to save resources during CI") public class HanoiTowerTest extends AbstractSolverTests { private final ProgramParser parser = new ProgramParser(); @Test(timeout = 10000) + @Ignore("disabled to save resources during CI") public void testInstance1() throws IOException { testHanoiTower(1); } @Test(timeout = 10000) + @Ignore("disabled to save resources during CI") public void testInstance2() throws IOException { testHanoiTower(2); } @Test(timeout = 10000) + @Ignore("disabled to save resources during CI") public void testInstance3() throws IOException { testHanoiTower(3); } @Test(timeout = 10000) + @Ignore("disabled to save resources during CI") public void testInstance4() throws IOException { testHanoiTower(4); } @@ -87,7 +90,7 @@ private void testHanoiTower(String instance) throws IOException { Solver solver = getInstance(parsedProgram); Optional answerSet = solver.stream().findFirst(); assertTrue(answerSet.isPresent()); - //System.out.println(answerSet.get()); + System.out.println(answerSet.get()); checkGoal(parsedProgram, answerSet.get()); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index bb23b37fe..2f1c9ed37 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017 Siemens AG + * Copyright (c) 2017-2018 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -75,7 +75,6 @@ public void testLocstrat_400() throws IOException { } @Test(timeout = 10000) - @Ignore("disabled to save resources during CI") public void testReach_1() throws IOException { test("reach", "reach-1.txt"); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java index 23360132a..418412e2d 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/PigeonHoleTest.java @@ -58,25 +58,21 @@ public void test2Pigeons3Holes() throws IOException { } @Test(timeout = 1000) - @Ignore("disabled to save resources during CI") public void test3Pigeons3Holes() throws IOException { testPigeonsHoles(3, 3); } - @Test(timeout = 1000) - @Ignore("disabled to save resources during CI") + @Test(timeout = 3000) public void test4Pigeons3Holes() throws IOException { testPigeonsHoles(4, 3); } - @Test(timeout = 1000) - @Ignore("disabled to save resources during CI") + @Test(timeout = 3000) public void test3Pigeons4Holes() throws IOException { testPigeonsHoles(3, 4); } - @Test(timeout = 1000) - @Ignore("disabled to save resources during CI") + @Test(timeout = 3000) public void test4Pigeons4Holes() throws IOException { testPigeonsHoles(4, 4); } From 82ea254e45f54ad3282434034a53a0ffe2d6bfb1 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Thu, 14 Mar 2019 10:27:41 +0100 Subject: [PATCH 02/36] Introduce ReplayHeuristic Fixes #172 --- .../java/at/ac/tuwien/kr/alpha/Alpha.java | 1 + .../kr/alpha/config/CommandLineParser.java | 14 +++ .../tuwien/kr/alpha/config/SystemConfig.java | 19 ++++ .../heuristics/BranchingHeuristicFactory.java | 7 +- .../heuristics/HeuristicsConfiguration.java | 25 +++++- .../HeuristicsConfigurationBuilder.java | 15 +++- .../solver/heuristics/ReplayHeuristic.java | 86 +++++++++++++++++++ 7 files changed, 160 insertions(+), 7 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java index 439510106..596ff6a37 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java @@ -115,6 +115,7 @@ public Solver prepareSolverFor(Program program) { HeuristicsConfigurationBuilder heuristicsConfigurationBuilder = HeuristicsConfiguration.builder(); heuristicsConfigurationBuilder.setHeuristic(this.config.getBranchingHeuristic()); heuristicsConfigurationBuilder.setMomsStrategy(this.config.getMomsStrategy()); + heuristicsConfigurationBuilder.setReplayChoices(this.config.getReplayChoices()); AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, doDebugChecks); 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 260b7c100..8ba0f5dce 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 @@ -89,6 +89,9 @@ public class CommandLineParser { private static final Option OPT_MOMS_STRATEGY = Option.builder("ms").longOpt("momsStrategy").hasArg(true).argName("strategy") .desc("strategy for mom's heuristic (CountBinaryWatches or BinaryNoGoodPropagation, default: " + SystemConfig.DEFAULT_MOMS_STRATEGY.name() + ")") .build(); + private static final Option OPT_REPLAY_CHOICES = Option.builder("rc").longOpt("replayChoices").hasArg().argName("choices") + .desc("list of signed atoms to be chosen (only applicable if " + OPT_BRANCHING_HEURISTIC.getOpt() + "=" + Heuristic.REPLAY.name() + ")") + .build(); private static final Option OPT_QUIET = Option.builder("q").longOpt("quiet").desc("do not print answer sets (default: " + SystemConfig.DEFAULT_QUIET) .build(); private static final Option OPT_STATS = Option.builder("st").longOpt("stats").desc("print statistics (default: " + SystemConfig.DEFAULT_PRINT_STATS + ")") @@ -124,6 +127,7 @@ public class CommandLineParser { CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_DEBUG_INTERNAL_CHECKS); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_BRANCHING_HEURISTIC); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_MOMS_STRATEGY); + CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_REPLAY_CHOICES); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_QUIET); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_STATS); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_JUSTIFICATION); @@ -165,6 +169,7 @@ public CommandLineParser(String cmdLineSyntax, Consumer abortAction) { this.globalOptionHandlers.put(CommandLineParser.OPT_DEBUG_INTERNAL_CHECKS.getOpt(), this::handleInternalChecks); this.globalOptionHandlers.put(CommandLineParser.OPT_BRANCHING_HEURISTIC.getOpt(), this::handleBranchingHeuristic); this.globalOptionHandlers.put(CommandLineParser.OPT_MOMS_STRATEGY.getOpt(), this::handleMomsStrategy); + this.globalOptionHandlers.put(CommandLineParser.OPT_REPLAY_CHOICES.getOpt(), this::handleReplayChoices); this.globalOptionHandlers.put(CommandLineParser.OPT_QUIET.getOpt(), this::handleQuiet); this.globalOptionHandlers.put(CommandLineParser.OPT_STATS.getOpt(), this::handleStats); this.globalOptionHandlers.put(CommandLineParser.OPT_NO_JUSTIFICATION.getOpt(), this::handleNoJustification); @@ -315,6 +320,15 @@ private void handleMomsStrategy(Option opt, SystemConfig cfg) throws ParseExcept throw new ParseException("Unknown mom's strategy: " + momsStrategyName + ". Please try one of the following: " + MOMs.Strategy.listAllowedValues()); } } + + private void handleReplayChoices(Option opt, SystemConfig cfg) throws ParseException { + String replayChoices = opt.getValue(SystemConfig.DEFAULT_REPLAY_CHOICES.toString()); + try { + cfg.setReplayChoices(replayChoices); + } catch (NumberFormatException e) { + throw new ParseException("Cannot parse list of signed integers indicating choices to be replayed: " + replayChoices); + } + } private void handleQuiet(Option opt, SystemConfig cfg) { cfg.setQuiet(true); 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 ea3472dec..f02e6e08c 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,11 @@ import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; import at.ac.tuwien.kr.alpha.solver.heuristics.MOMs; +import java.util.Arrays; +import java.util.Collections; +import java.util.List; +import java.util.stream.Collectors; + public class SystemConfig { // Note: Defining constants for default values here rather than just @@ -49,6 +54,7 @@ public class SystemConfig { public static final boolean DEFAULT_DEBUG_INTERNAL_CHECKS = false; public static final boolean DEFAULT_USE_NORMALIZATION_GRID = false; public static final boolean DEFAULT_SORT_ANSWER_SETS = false; + public static final List DEFAULT_REPLAY_CHOICES = Collections.emptyList(); private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME; private String solverName = SystemConfig.DEFAULT_SOLVER_NAME; @@ -63,6 +69,7 @@ public class SystemConfig { private boolean disableJustificationSearch = SystemConfig.DEFAULT_DISABLE_JUSTIFICATION_SEARCH; private boolean useNormalizationGrid = SystemConfig.DEFAULT_USE_NORMALIZATION_GRID; private boolean sortAnswerSets = SystemConfig.DEFAULT_SORT_ANSWER_SETS; + private List replayChoices = SystemConfig.DEFAULT_REPLAY_CHOICES; public String getGrounderName() { return this.grounderName; @@ -176,4 +183,16 @@ public void setSortAnswerSets(boolean sortAnswerSets) { this.sortAnswerSets = sortAnswerSets; } + public List getReplayChoices() { + return replayChoices; + } + + public void setReplayChoices(List replayChoices) { + this.replayChoices = replayChoices; + } + + public void setReplayChoices(String replayChoices) { + this.replayChoices = Arrays.stream(replayChoices.split(", ")).map(Integer::valueOf).collect(Collectors.toList()); + } + } 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 7af7ab004..56e1d738c 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 @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017 Siemens AG + * Copyright (c) 2017-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -55,7 +55,8 @@ public enum Heuristic { ALPHA_ACTIVE_RULE, ALPHA_HEAD_MBT, VSIDS, - GDD_VSIDS; + GDD_VSIDS, + REPLAY; /** * @return a comma-separated list of names of known heuristics @@ -105,6 +106,8 @@ public static BranchingHeuristic getInstance(HeuristicsConfiguration heuristicsC return new VSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); case GDD_VSIDS: return new DependencyDrivenVSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); + case REPLAY: + return new ReplayHeuristic(heuristicsConfiguration.getReplayChoices(), choiceManager); } throw new IllegalArgumentException("Unknown branching heuristic requested."); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfiguration.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfiguration.java index 07cecd9d3..02a224eb5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfiguration.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfiguration.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2018 Siemens AG + * Copyright (c) 2018-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -28,6 +28,8 @@ import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; import at.ac.tuwien.kr.alpha.solver.heuristics.MOMs.Strategy; +import java.util.List; + /** * Configuration class holding parameters for {@link BranchingHeuristic}s. */ @@ -35,15 +37,18 @@ public class HeuristicsConfiguration { private Heuristic heuristic; private MOMs.Strategy momsStrategy; - + private List replayChoices; + /** * @param heuristic * @param momsStrategy + * @param replayChoices */ - public HeuristicsConfiguration(Heuristic heuristic, Strategy momsStrategy) { + public HeuristicsConfiguration(Heuristic heuristic, Strategy momsStrategy, List replayChoices) { super(); this.heuristic = heuristic; this.momsStrategy = momsStrategy; + this.replayChoices = replayChoices; } /** @@ -74,6 +79,20 @@ public void setMomsStrategy(MOMs.Strategy momsStrategy) { this.momsStrategy = momsStrategy; } + /** + * @return the replayChoices + */ + public List getReplayChoices() { + return replayChoices; + } + + /** + * @param replayChoices the replayChoices to set + */ + public void setReplayChoices(List replayChoices) { + this.replayChoices = replayChoices; + } + public static HeuristicsConfigurationBuilder builder() { return new HeuristicsConfigurationBuilder(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfigurationBuilder.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfigurationBuilder.java index da1f12157..2a41c11b8 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfigurationBuilder.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/HeuristicsConfigurationBuilder.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2018 Siemens AG + * Copyright (c) 2018-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -27,6 +27,8 @@ import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; +import java.util.List; + /** * Builder for {@link HeuristicsConfiguration} objects */ @@ -34,6 +36,7 @@ public class HeuristicsConfigurationBuilder { private Heuristic heuristic; private MOMs.Strategy momsStrategy; + private List replayChoices; /** * @param heuristic the heuristic to set @@ -51,8 +54,16 @@ public HeuristicsConfigurationBuilder setMomsStrategy(MOMs.Strategy momsStrategy return this; } + /** + * @param replayChoices the replayChoices to set + */ + public HeuristicsConfigurationBuilder setReplayChoices(List replayChoices) { + this.replayChoices = replayChoices; + return this; + } + public HeuristicsConfiguration build() { - return new HeuristicsConfiguration(heuristic, momsStrategy); + return new HeuristicsConfiguration(heuristic, momsStrategy, replayChoices); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java new file mode 100644 index 000000000..1fd453ce0 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java @@ -0,0 +1,86 @@ +/** + * Copyright (c) 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.Literals; +import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.solver.ChoiceManager; +import at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult; + +import java.util.Iterator; +import java.util.List; + +/** + * A heuristic that replays a fixed list of choices. + */ +public class ReplayHeuristic implements BranchingHeuristic { + + private final Iterator choicesIterator; + private final ChoiceManager choiceManager; + + /** + * Initializes the heuristic + * @param choices a list of signed atoms (positive if atom shall be made true, negative otherwise) + * @param choiceManager + */ + public ReplayHeuristic(List choices, ChoiceManager choiceManager) { + super(); + this.choicesIterator = choices.iterator(); + this.choiceManager = choiceManager; + } + + @Override + public void violatedNoGood(NoGood violatedNoGood) { + } + + @Override + public void analyzedConflict(ConflictAnalysisResult analysisResult) { + } + + @Override + public void newNoGood(NoGood newNoGood) { + } + + @Override + public int chooseLiteral() { + if (!choicesIterator.hasNext()) { + return DEFAULT_CHOICE_LITERAL; + } + int replayChoiceSignedAtom = choicesIterator.next(); + int replayChoiceAtom = Math.abs(replayChoiceSignedAtom); + int replayChoiceLiteral = Literals.atomToLiteral(replayChoiceAtom, replayChoiceSignedAtom > 0); + if (!choiceManager.isActiveChoiceAtom(replayChoiceAtom)) { + throw new IllegalStateException("Replay choice is not an active choice point: " + replayChoiceAtom); + } + return replayChoiceLiteral; + } + + @Override + public String toString() { + return this.getClass().getSimpleName(); + } + +} From 707047c3af0bfc3b00ec6a59f24218d4135c3cdf Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Thu, 14 Mar 2019 14:23:08 +0100 Subject: [PATCH 03/36] Use ReplayHeuristic as first element of ChainedBranchingHeuristic if choices to be replayed are given --- .../kr/alpha/config/CommandLineParser.java | 2 +- .../tuwien/kr/alpha/solver/DefaultSolver.java | 15 ++++++++++++--- .../heuristics/BranchingHeuristicFactory.java | 17 +++++++++++++---- .../heuristics/ChainedBranchingHeuristics.java | 6 +++++- 4 files changed, 31 insertions(+), 9 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 8ba0f5dce..a1642d279 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 @@ -90,7 +90,7 @@ public class CommandLineParser { .desc("strategy for mom's heuristic (CountBinaryWatches or BinaryNoGoodPropagation, default: " + SystemConfig.DEFAULT_MOMS_STRATEGY.name() + ")") .build(); private static final Option OPT_REPLAY_CHOICES = Option.builder("rc").longOpt("replayChoices").hasArg().argName("choices") - .desc("list of signed atoms to be chosen (only applicable if " + OPT_BRANCHING_HEURISTIC.getOpt() + "=" + Heuristic.REPLAY.name() + ")") + .desc("list of choices (signed atom IDs) to be replayed") .build(); private static final Option OPT_QUIET = Option.builder("q").longOpt("quiet").desc("do not print answer sets (default: " + SystemConfig.DEFAULT_QUIET) .build(); 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 3964795b9..6b724fae8 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 @@ -83,13 +83,22 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.store = store; this.choiceManager = new ChoiceManager(assignment, store); this.learner = new GroundConflictNoGoodLearner(assignment); - this.branchingHeuristic = ChainedBranchingHeuristics.chainOf( - BranchingHeuristicFactory.getInstance(heuristicsConfiguration, grounder, assignment, choiceManager, random), - new NaiveHeuristic(choiceManager)); + this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration); this.disableJustifications = disableJustifications; this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000); } + private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) { + BranchingHeuristic branchingHeuristic = BranchingHeuristicFactory.getInstance(heuristicsConfiguration, grounder, assignment, choiceManager, random); + if (branchingHeuristic instanceof NaiveHeuristic) { + return branchingHeuristic; + } + if (branchingHeuristic instanceof ChainedBranchingHeuristics && ((ChainedBranchingHeuristics)branchingHeuristic).getLastElement() instanceof NaiveHeuristic) { + return branchingHeuristic; + } + return ChainedBranchingHeuristics.chainOf(branchingHeuristic, new NaiveHeuristic(choiceManager)); + } + @Override protected boolean tryAdvance(Consumer action) { boolean didChange = false; 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 56e1d738c..5d7d67d95 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 @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.solver.heuristics.activity.BodyActivityProviderFactory.BodyActivityType; import java.util.Arrays; +import java.util.List; import java.util.Random; import java.util.stream.Collectors; @@ -55,8 +56,7 @@ public enum Heuristic { ALPHA_ACTIVE_RULE, ALPHA_HEAD_MBT, VSIDS, - GDD_VSIDS, - REPLAY; + GDD_VSIDS; /** * @return a comma-separated list of names of known heuristics @@ -67,6 +67,17 @@ public static String listAllowedValues() { } public static BranchingHeuristic getInstance(HeuristicsConfiguration heuristicsConfiguration, Grounder grounder, WritableAssignment assignment, ChoiceManager choiceManager, Random random) { + BranchingHeuristic heuristicWithoutReplay = getInstanceWithoutReplay(heuristicsConfiguration, grounder, assignment, choiceManager, random); + List replayChoices = heuristicsConfiguration.getReplayChoices(); + if (replayChoices != null && !replayChoices.isEmpty() ) { + return ChainedBranchingHeuristics.chainOf( + new ReplayHeuristic(replayChoices, choiceManager), + heuristicWithoutReplay); + } + return heuristicWithoutReplay; + } + + public static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfiguration heuristicsConfiguration, Grounder grounder, WritableAssignment assignment, ChoiceManager choiceManager, Random random) { switch (heuristicsConfiguration.getHeuristic()) { case NAIVE: return new NaiveHeuristic(choiceManager); @@ -106,8 +117,6 @@ public static BranchingHeuristic getInstance(HeuristicsConfiguration heuristicsC return new VSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); case GDD_VSIDS: return new DependencyDrivenVSIDS(assignment, choiceManager, random, heuristicsConfiguration.getMomsStrategy()); - case REPLAY: - return new ReplayHeuristic(heuristicsConfiguration.getReplayChoices(), choiceManager); } throw new IllegalArgumentException("Unknown branching heuristic requested."); } 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 69eabb511..14e57ecf1 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 @@ -1,5 +1,5 @@ /** - * Copyright (c) 2018 Siemens AG + * Copyright (c) 2018-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -90,6 +90,10 @@ public void add(BranchingHeuristic element) { } chain.add(element); } + + public BranchingHeuristic getLastElement() { + return chain.get(chain.size() - 1); + } public static ChainedBranchingHeuristics chainOf(BranchingHeuristic... branchingHeuristics) { return new ChainedBranchingHeuristics(branchingHeuristics); From 5fe27d694728d8facba7020a39a121a4942aeab4 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Thu, 14 Mar 2019 14:26:46 +0100 Subject: [PATCH 04/36] Satisfy CheckStyle --- .../kr/alpha/solver/heuristics/BranchingHeuristicFactory.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 5d7d67d95..d78567b27 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 @@ -69,7 +69,7 @@ public static String listAllowedValues() { public static BranchingHeuristic getInstance(HeuristicsConfiguration heuristicsConfiguration, Grounder grounder, WritableAssignment assignment, ChoiceManager choiceManager, Random random) { BranchingHeuristic heuristicWithoutReplay = getInstanceWithoutReplay(heuristicsConfiguration, grounder, assignment, choiceManager, random); List replayChoices = heuristicsConfiguration.getReplayChoices(); - if (replayChoices != null && !replayChoices.isEmpty() ) { + if (replayChoices != null && !replayChoices.isEmpty()) { return ChainedBranchingHeuristics.chainOf( new ReplayHeuristic(replayChoices, choiceManager), heuristicWithoutReplay); From 4413cf8e62e28d3af4e2f1b8a30a436f8524e4c0 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 5 Aug 2019 08:36:59 +0200 Subject: [PATCH 05/36] Add reference to LPNMR 2019 paper --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 458c88a15..f1dc09b24 100644 --- a/README.md +++ b/README.md @@ -81,6 +81,7 @@ run into trouble feel free to file an issue. Peer-reviewed publications part of journals, conferences and workshops: + * [Degrees of Laziness in Grounding: Effects of Lazy-Grounding Strategies on ASP Solving](https://doi.org/10.1007/978-3-030-20528-7_22) ([preprint](https://arxiv.org/abs/1903.12510) | [supplementary material](https://git-ainf.aau.at/DynaCon/website/tree/master/supplementary_material/2019_LPNMR_Degrees_of_Laziness)) * [Exploiting Justifications for Lazy Grounding of Answer Set Programs](https://doi.org/10.24963/ijcai.2018/240) * [Lazy Grounding for Dynamic Configuration: Efficient Large-Scale (Re)Configuration of Cyber-Physical Systems with ASP](https://doi.org/10.1007/s13218-018-0536-x) * [Blending Lazy-Grounding and CDNL Search for Answer-Set Solving](https://doi.org/10.1007/978-3-319-61660-5_17) ([preprint](http://www.kr.tuwien.ac.at/research/systems/alpha/blending_lazy_grounding.pdf)) From 3e3eec6ad9669df16c48d92d6abdf8690df07a48 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Fri, 9 Aug 2019 18:06:58 +0200 Subject: [PATCH 06/36] Make method private --- .../kr/alpha/solver/heuristics/BranchingHeuristicFactory.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 29128d54f..b54cfdd53 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 @@ -77,7 +77,7 @@ public static BranchingHeuristic getInstance(HeuristicsConfiguration heuristicsC return heuristicWithoutReplay; } - public static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfiguration heuristicsConfiguration, Grounder grounder, WritableAssignment assignment, ChoiceManager choiceManager, Random random) { + private static BranchingHeuristic getInstanceWithoutReplay(HeuristicsConfiguration heuristicsConfiguration, Grounder grounder, WritableAssignment assignment, ChoiceManager choiceManager, Random random) { switch (heuristicsConfiguration.getHeuristic()) { case NAIVE: return new NaiveHeuristic(choiceManager); From 5077d6681ede4cbbd01ada1bb5c9c033ec6c25f3 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Fri, 9 Aug 2019 18:07:34 +0200 Subject: [PATCH 07/36] Coverage for replay heuristics --- .../BranchingHeuristicFactoryTest.java | 72 ++++++++++++++++++ .../heuristics/ReplayHeuristicTest.java | 74 +++++++++++++++++++ 2 files changed, 146 insertions(+) create mode 100644 src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java create mode 100644 src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java 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 new file mode 100644 index 000000000..519f14169 --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/BranchingHeuristicFactoryTest.java @@ -0,0 +1,72 @@ +/** + * Copyright (c) 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.AtomStore; +import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.solver.*; +import org.junit.Before; +import org.junit.Test; + +import java.util.Arrays; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + +/** + * Tests {@link BranchingHeuristicFactory} + */ +public class BranchingHeuristicFactoryTest { + + private final BranchingHeuristicFactory factory = new BranchingHeuristicFactory(); + private final boolean debugInternalChecks = true; + private ChoiceManager choiceManager; + + @Before + public void setUp() { + AtomStore atomStore = new AtomStoreImpl(); + WritableAssignment assignment = new TrailAssignment(atomStore); + NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks); + this.choiceManager = new ChoiceManager(assignment, store); + } + + @Test + public void testChainedHeuristicWithReplay() { + HeuristicsConfigurationBuilder builder = new HeuristicsConfigurationBuilder().setHeuristic(BranchingHeuristicFactory.Heuristic.VSIDS).setReplayChoices(Arrays.asList(1, 2, 3)); + BranchingHeuristic branchingHeuristic = factory.getInstance(builder.build(), null, null, choiceManager, null); + assertEquals(ChainedBranchingHeuristics.class, branchingHeuristic.getClass()); + assertTrue("Unexpected type of branchingHeuristic: " + branchingHeuristic.getClass(), branchingHeuristic instanceof ChainedBranchingHeuristics); + assertEquals(ChainedBranchingHeuristics.class.getSimpleName() + "[" + ReplayHeuristic.class.getSimpleName() + ", " + VSIDS.class.getSimpleName() + "]", branchingHeuristic.toString()); + } + + @Test + public void testChainedHeuristicWithoutReplay() { + HeuristicsConfigurationBuilder builder = new HeuristicsConfigurationBuilder().setHeuristic(BranchingHeuristicFactory.Heuristic.VSIDS).setReplayChoices(null); + BranchingHeuristic branchingHeuristic = factory.getInstance(builder.build(), null, null, choiceManager, null); + assertEquals(VSIDS.class, branchingHeuristic.getClass()); + } + +} 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 new file mode 100644 index 000000000..81ec7bbd1 --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristicTest.java @@ -0,0 +1,74 @@ +/** + * Copyright (c) 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.AtomStore; +import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; +import at.ac.tuwien.kr.alpha.solver.*; +import org.junit.Before; +import org.junit.Test; + +import java.util.Arrays; +import java.util.List; + +import static at.ac.tuwien.kr.alpha.common.Literals.atomToLiteral; +import static org.junit.Assert.assertEquals; + +/** + * Tests {@link ReplayHeuristic} + */ +public class ReplayHeuristicTest { + + private final boolean debugInternalChecks = true; + private ChoiceManager choiceManager; + + @Before + public void setUp() { + AtomStore atomStore = new AtomStoreImpl(); + WritableAssignment assignment = new TrailAssignment(atomStore); + NoGoodStore store = new NoGoodStoreAlphaRoaming(assignment, debugInternalChecks); + this.choiceManager = new PseudoChoiceManager(assignment, store); + } + + @Test + public void testBasicChoiceSequence() { + final int literal1 = atomToLiteral(2); + final int signedAtom1 = 2; + + final int literal2 = atomToLiteral(4, false); + final int signedAtom2 = -4; + + final int literal3 = atomToLiteral(7); + final int signedAtom3 = 7; + + final List chosenSignedAtoms = Arrays.asList(signedAtom1, signedAtom2, signedAtom3); + final ReplayHeuristic replayHeuristic = new ReplayHeuristic(chosenSignedAtoms, choiceManager); + assertEquals(literal1, replayHeuristic.chooseLiteral()); + assertEquals(literal2, replayHeuristic.chooseLiteral()); + assertEquals(literal3, replayHeuristic.chooseLiteral()); + } + +} From 4383f95ae6bc6c7958b0e74aed2cf335cf05ce3f Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Fri, 9 Aug 2019 18:33:36 +0200 Subject: [PATCH 08/36] Fix HanoiTowerTest --- .../java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index fb19b69e9..2303c6526 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017 Siemens AG + * Copyright (c) 2017-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -105,9 +105,9 @@ private void checkGoal(Program parsedProgram, AnswerSet answerSet) { SortedSet onInstancesInAnswerSet = answerSet.getPredicateInstances(on); for (Atom atom : parsedProgram.getFacts()) { if (atom.getPredicate().getName().equals(ongoal.getName()) && atom.getPredicate().getArity() == ongoal.getArity()) { - Term expectedTop = ConstantTerm.getInstance(atom.getTerms().get(0).toString()); - Term expectedBottom = ConstantTerm.getInstance(atom.getTerms().get(1).toString()); - Term expectedSteps = ConstantTerm.getInstance(String.valueOf(steps)); + Term expectedTop = atom.getTerms().get(0); + Term expectedBottom = atom.getTerms().get(1); + Term expectedSteps = ConstantTerm.getInstance(steps); Atom expectedAtom = new BasicAtom(on, expectedSteps, expectedBottom, expectedTop); assertTrue("Answer set does not contain " + expectedAtom, onInstancesInAnswerSet.contains(expectedAtom)); } From f2631e103850fcedbd603829c74584eb8b4e6bbc Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Fri, 9 Aug 2019 18:45:15 +0200 Subject: [PATCH 09/36] Coverage for replay heuristics --- .../alpha/config/CommandLineParserTest.java | 44 ++++++++++++++++++- 1 file changed, 42 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 a41016f29..b89888c44 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,11 +1,38 @@ +/** + * Copyright (c) 2019, 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.config; -import java.util.Arrays; - import org.apache.commons.cli.ParseException; import org.junit.Assert; import org.junit.Test; +import java.util.Arrays; + public class CommandLineParserTest { /** @@ -67,4 +94,17 @@ public void noInputGiven() throws ParseException { parser.parseCommandLine(new String[] {}); } + @Test + public void replay() throws ParseException { + CommandLineParser parser = new CommandLineParser("java -jar Alpha-bundled.jar", (msg) -> { }); + AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-rc", "\"1, 2, 3\""}); + Assert.assertEquals(Arrays.asList(1, 2, 3), alphaConfig.getAlphaConfig().getReplayChoices()); + } + + @Test(expected = ParseException.class) + public void replayWithNonNumericLiteral() throws ParseException { + CommandLineParser parser = new CommandLineParser("java -jar Alpha-bundled.jar", (msg) -> { }); + AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-rc", "\"1, 2, x\""}); + } + } From 0661ab070f26767a82614b13f5c66c8ed5e08f4d Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Fri, 9 Aug 2019 19:08:17 +0200 Subject: [PATCH 10/36] Fix bug in old domain-specific heuristics discovered by HanoiTowerTest --- .../at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java | 8 +++++--- .../solver/heuristics/DependencyDrivenHeuristic.java | 8 +++++--- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java index c5b20cc09..2c30459dc 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2016-2018 Siemens AG + * Copyright (c) 2016-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -121,8 +121,10 @@ public void analyzedConflict(ConflictAnalysisResult analysisResult) { incrementActivityCounter(atomToLiteral(resolutionAtom, true)); incrementActivityCounter(atomToLiteral(resolutionAtom, false)); } - for (int literal : analysisResult.learnedNoGood) { - incrementActivityCounter(literal); + if (analysisResult.learnedNoGood != null) { + for (int literal : analysisResult.learnedNoGood) { + incrementActivityCounter(literal); + } } decayAllIfTimeHasCome(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java index 2f8733ed5..e24f29da0 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017-2018 Siemens AG + * Copyright (c) 2017-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -155,8 +155,10 @@ public void analyzedConflict(ConflictAnalysisResult analysisResult) { incrementActivityCounter(atomToLiteral(resolutionAtom, true)); incrementActivityCounter(atomToLiteral(resolutionAtom, false)); } - for (Integer literal : analysisResult.learnedNoGood) { - incrementSignCounter(literal); + if (analysisResult.learnedNoGood != null) { + for (Integer literal : analysisResult.learnedNoGood) { + incrementSignCounter(literal); + } } decayAllIfTimeHasCome(); } From 631663bc875df9f6260c36c083bdb80fd5b32101 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 12 Aug 2019 09:38:03 +0200 Subject: [PATCH 11/36] Disable unit tests to save resources during CI --- .../at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index 2303c6526..0ec7055f3 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -36,6 +36,8 @@ import org.antlr.v4.runtime.CharStreams; import org.junit.Ignore; import org.junit.Test; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; import java.io.IOException; import java.nio.file.Paths; @@ -49,6 +51,9 @@ * */ public class HanoiTowerTest extends AbstractSolverTests { + + private static final Logger LOGGER = LoggerFactory.getLogger(HanoiTowerTest.class); + private final ProgramParser parser = new ProgramParser(); @Test(timeout = 10000) @@ -85,6 +90,10 @@ private void testHanoiTower(int instance) throws IOException { } private void testHanoiTower(String instance) throws IOException { + if ("naive".equals(solverName)) { + LOGGER.warn(this.getClass().getSimpleName() + " disabled for naive solver to save resources during CI"); + return; + } Program parsedProgram = parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_Alpha.asp"))); parsedProgram.accumulate(parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_instances", instance + ".asp")))); Solver solver = getInstance(parsedProgram); From 350c7d2ae30ba8fbf7e602b3d0f1bca89425318f Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 12 Aug 2019 23:08:40 +0200 Subject: [PATCH 12/36] Remove oraclejdk8 from tested JVMs due to lack of support on Travis. --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index db6b972a4..f9d534d9d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -16,7 +16,7 @@ language: java jdk: # LTS and in "Premier Support" as of 2019-03 (until 2022-03) - openjdk8 - - oraclejdk8 + # - oraclejdk8 # Removed due to not being supported on Ubuntu xenial # LTS and in "Premier Support" as of 2019-03 (until 2023-09) - openjdk11 - oraclejdk11 From 316a655fb4ed6dc546595ab4dfebbac99588c835 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 14 Aug 2019 09:15:05 +0200 Subject: [PATCH 13/36] Re-enable more unit tests (and increase time limits) --- .../tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index 2f1c9ed37..4aa26791b 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017-2018 Siemens AG + * Copyright (c) 2017-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -50,14 +50,12 @@ public void test3Col_20_38() throws IOException { test("3col", "3col-20-38.txt"); } - @Test(timeout = 10000) - @Ignore("disabled to save resources during CI") + @Test(timeout = 15000) public void testCutedge_100_30() throws IOException { test("cutedge", "cutedge-100-30.txt"); } - @Test(timeout = 10000) - @Ignore("disabled to save resources during CI") + @Test(timeout = 15000) public void testCutedge_100_50() throws IOException { test("cutedge", "cutedge-100-50.txt"); } @@ -74,12 +72,12 @@ public void testLocstrat_400() throws IOException { test("locstrat", "locstrat-400.txt"); } - @Test(timeout = 10000) + @Test(timeout = 15000) public void testReach_1() throws IOException { test("reach", "reach-1.txt"); } - @Test(timeout = 10000) + @Test(timeout = 15000) @Ignore("disabled to save resources during CI") public void testReach_4() throws IOException { test("reach", "reach-4.txt"); From c9ef0065257e3ca4a0b092caf655b64c6ccdec86 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 14 Aug 2019 09:49:53 +0200 Subject: [PATCH 14/36] Disable unit tests to save resources during CI --- .../ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index 4aa26791b..7e5373b27 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -30,6 +30,8 @@ import org.antlr.v4.runtime.CharStreams; import org.junit.Ignore; import org.junit.Test; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; import java.io.IOException; import java.nio.file.Paths; @@ -40,6 +42,9 @@ * */ public class OmigaBenchmarksTest extends AbstractSolverTests { + + private static final Logger LOGGER = LoggerFactory.getLogger(OmigaBenchmarksTest.class); + @Test(timeout = 10000) public void test3Col_10_18() throws IOException { test("3col", "3col-10-18.txt"); @@ -84,6 +89,10 @@ public void testReach_4() throws IOException { } private void test(String folder, String aspFileName) throws IOException { + if ("naive".equals(solverName)) { + LOGGER.warn(this.getClass().getSimpleName() + " disabled for naive solver to save resources during CI"); + return; + } CharStream programInputStream = CharStreams.fromPath( Paths.get("benchmarks", "omiga", "omiga-testcases", folder, aspFileName) ); From a699c22c717de0737b1854cde71f759622188249 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 14 Aug 2019 12:02:21 +0200 Subject: [PATCH 15/36] =?UTF-8?q?Use=20JUnit=C2=B4s=20assumeFalse=20to=20r?= =?UTF-8?q?un=20tests=20conditionally?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 6 ++---- .../at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 7 +++---- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index 0ec7055f3..83bcc9b59 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -45,6 +45,7 @@ import java.util.SortedSet; import static org.junit.Assert.assertTrue; +import static org.junit.Assume.assumeFalse; /** * Tests {@link AbstractSolver} using some hanoi tower test cases (see https://en.wikipedia.org/wiki/Tower_of_Hanoi). @@ -90,10 +91,7 @@ private void testHanoiTower(int instance) throws IOException { } private void testHanoiTower(String instance) throws IOException { - if ("naive".equals(solverName)) { - LOGGER.warn(this.getClass().getSimpleName() + " disabled for naive solver to save resources during CI"); - return; - } + assumeFalse("naive".equals(solverName)); // disabled for naive solver to save resources during CI Program parsedProgram = parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_Alpha.asp"))); parsedProgram.accumulate(parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_instances", instance + ".asp")))); Solver solver = getInstance(parsedProgram); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index 7e5373b27..414d6247c 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -37,6 +37,8 @@ import java.nio.file.Paths; import java.util.Optional; +import static org.junit.Assume.assumeFalse; + /** * Tests {@link AbstractSolver} using Omiga benchmark problems. * @@ -89,10 +91,7 @@ public void testReach_4() throws IOException { } private void test(String folder, String aspFileName) throws IOException { - if ("naive".equals(solverName)) { - LOGGER.warn(this.getClass().getSimpleName() + " disabled for naive solver to save resources during CI"); - return; - } + assumeFalse("naive".equals(solverName)); // disabled for naive solver to save resources during CI CharStream programInputStream = CharStreams.fromPath( Paths.get("benchmarks", "omiga", "omiga-testcases", folder, aspFileName) ); From 273fe461f2c48c87b4a6206ec1f83435ddad4551 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 14 Aug 2019 14:59:10 +0200 Subject: [PATCH 16/36] Use AbstractSolverTests#ignoreTestForNaiveSolver --- .../java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 3 +-- .../at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 4 +--- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index 83bcc9b59..c1cd7e4f6 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -45,7 +45,6 @@ import java.util.SortedSet; import static org.junit.Assert.assertTrue; -import static org.junit.Assume.assumeFalse; /** * Tests {@link AbstractSolver} using some hanoi tower test cases (see https://en.wikipedia.org/wiki/Tower_of_Hanoi). @@ -91,7 +90,7 @@ private void testHanoiTower(int instance) throws IOException { } private void testHanoiTower(String instance) throws IOException { - assumeFalse("naive".equals(solverName)); // disabled for naive solver to save resources during CI + ignoreTestForNaiveSolver(); Program parsedProgram = parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_Alpha.asp"))); parsedProgram.accumulate(parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_instances", instance + ".asp")))); Solver solver = getInstance(parsedProgram); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index 414d6247c..89023e06e 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -37,8 +37,6 @@ import java.nio.file.Paths; import java.util.Optional; -import static org.junit.Assume.assumeFalse; - /** * Tests {@link AbstractSolver} using Omiga benchmark problems. * @@ -91,7 +89,7 @@ public void testReach_4() throws IOException { } private void test(String folder, String aspFileName) throws IOException { - assumeFalse("naive".equals(solverName)); // disabled for naive solver to save resources during CI + ignoreTestForNaiveSolver(); CharStream programInputStream = CharStreams.fromPath( Paths.get("benchmarks", "omiga", "omiga-testcases", folder, aspFileName) ); From fea027f9fed457da609661d5c86b930931cfca70 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Wed, 14 Aug 2019 15:00:55 +0200 Subject: [PATCH 17/36] Use Integer.parseInt instead of Integer.valueOf --- src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index c1cd7e4f6..71219b07a 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -124,7 +124,7 @@ private int getSteps(Program parsedProgram) { Predicate steps = Predicate.getInstance("steps", 1); for (Atom atom : parsedProgram.getFacts()) { if (atom.getPredicate().getName().equals(steps.getName()) && atom.getPredicate().getArity() == steps.getArity()) { - return Integer.valueOf(atom.getTerms().get(0).toString()); + return Integer.parseInt(atom.getTerms().get(0).toString()); } } throw new IllegalArgumentException("No steps atom found in input program."); From 5f22caf4c65fd08394e616664109f82ae2cb2260 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 9 Sep 2019 00:05:06 +0200 Subject: [PATCH 18/36] Add learned-NoGood deletion and trail-using conflict-driven learning. - NoGoods provide literals array as reasons. - GroundConflictNoGoodLearner provides conflict analysis using trail. - DefaultSolver runs learned NoGood deletion. - ImplicationReasonProvider provides antecedents/reasons. - A basic LearnedNoGoodDeletion strategy, currently never running. - NoGoodStore provides cleanupLearnedNoGoods method. - NaiveNoGoodStore provides empty cleanupLearnedNoGoods. - NoGoodStoreAlphaRoaming adds NoGoods with LBD, integrates with basic LearnedNoGoodDeletion strategy. - TrailAssignment keeps literals on the trail, provides reasons literals as array of ints, and provides a walker for the trail. - WatchedNoGoods are prepared to hold an activity and LBD. --- .../at/ac/tuwien/kr/alpha/common/NoGood.java | 8 +- .../tuwien/kr/alpha/solver/DefaultSolver.java | 19 +- .../solver/ImplicationReasonProvider.java | 2 + .../alpha/solver/LearnedNoGoodDeletion.java | 86 +++++++++ .../kr/alpha/solver/NaiveNoGoodStore.java | 4 + .../tuwien/kr/alpha/solver/NoGoodStore.java | 2 + .../alpha/solver/NoGoodStoreAlphaRoaming.java | 68 ++++++-- .../kr/alpha/solver/TrailAssignment.java | 59 ++++++- .../tuwien/kr/alpha/solver/WatchedNoGood.java | 33 ++++ .../learning/GroundConflictNoGoodLearner.java | 164 ++++++++++++++++-- 10 files changed, 404 insertions(+), 41 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java index 7139e79f1..cd603eeaa 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java @@ -266,7 +266,13 @@ public String toString() { public NoGood getNoGood(int impliedAtom) { return this; } - + + @Override + public int[] getReasonLiterals() { + // TODO: this is dangerous and should not be necessary (requires further solver internal changes). + return literals; + } + /** * The possible nogood types */ 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 0b02c1fae..66f7da581 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 @@ -122,7 +122,7 @@ protected boolean tryAdvance(Consumer action) { // Backjump instead of backtrackSlow, enumerationNoGood will invert last choice. choiceManager.backjump(backjumpLevel - 1); LOGGER.debug("Adding enumeration nogood: {}", enumerationNoGood); - if (!addAndBackjumpIfNecessary(grounder.register(enumerationNoGood), enumerationNoGood)) { + if (!addAndBackjumpIfNecessary(grounder.register(enumerationNoGood), enumerationNoGood, -1)) { return false; } } @@ -135,6 +135,10 @@ protected boolean tryAdvance(Consumer action) { ConflictCause conflictCause = store.propagate(); didChange |= store.didPropagate(); LOGGER.trace("Assignment after propagation is: {}", assignment); + if (conflictCause == null) { + // Run learned NoGood deletion strategy. + store.cleanupLearnedNoGoods(); + } if (conflictCause != null) { // Learn from conflict. NoGood violatedNoGood = conflictCause.getViolatedNoGood(); @@ -193,8 +197,8 @@ protected boolean tryAdvance(Consumer action) { * @param noGoodId * @param noGood */ - private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood) { - while (store.add(noGoodId, noGood) != null) { + private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd) { + while (((NoGoodStoreAlphaRoaming)store).add(noGoodId, noGood, lbd) != null) { LOGGER.debug("Adding noGood (again) caused conflict, computing real backjumping level now."); int backjumpLevel = learner.computeConflictFreeBackjumpingLevel(noGood); if (backjumpLevel < 0) { @@ -235,7 +239,7 @@ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) { final NoGood learnedNoGood = analysisResult.learnedNoGood; int noGoodId = grounder.register(learnedNoGood); - if (!addAndBackjumpIfNecessary(noGoodId, learnedNoGood)) { + if (!addAndBackjumpIfNecessary(noGoodId, learnedNoGood, analysisResult.lbd)) { return false; } return true; @@ -467,11 +471,14 @@ private NoGood fixContradiction(Map.Entry noGoodEntry, Conflict return null; } - GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGood(conflictCause.getViolatedNoGood()); + GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictFromAddingNoGood(conflictCause.getViolatedNoGood()); if (conflictAnalysisResult == UNSAT) { return NoGood.UNSAT; } branchingHeuristic.analyzedConflict(conflictAnalysisResult); + if (conflictAnalysisResult.learnedNoGood != null || conflictAnalysisResult.clearLastChoiceAfterBackjump) { + throw oops("Unexpectedly learned NoGood after addition of new NoGood caused a conflict."); + } choiceManager.backjump(conflictAnalysisResult.backjumpLevel); if (conflictAnalysisResult.clearLastChoiceAfterBackjump) { @@ -481,7 +488,7 @@ private NoGood fixContradiction(Map.Entry noGoodEntry, Conflict // If NoGood was learned, add it to the store. // Note that the learned NoGood may cause further conflicts, since propagation on lower decision levels is lazy, // hence backtracking once might not be enough to remove the real conflict cause. - if (!addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue())) { + if (!addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue(), -1)) { return NoGood.UNSAT; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java index daae69508..e7a63169b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java @@ -7,4 +7,6 @@ */ public interface ImplicationReasonProvider { NoGood getNoGood(int impliedLiteral); + + int[] getReasonLiterals(); } 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 new file mode 100644 index 000000000..765edcc94 --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java @@ -0,0 +1,86 @@ +package at.ac.tuwien.kr.alpha.solver; + +import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.NoGood; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Iterator; + +import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; + +/** + * Realizes a learned NoGood deletion strategy based on LBD and activity of NoGoods. + * + * Copyright (c) 2019, the Alpha Team. + */ +class LearnedNoGoodDeletion { + private static final Logger LOGGER = LoggerFactory.getLogger(LearnedNoGoodDeletion.class); + private final ArrayList learnedNoGoods = new ArrayList<>(); // List of learned NoGoods that can be removed again. Note: should only contain NoGoods of size > 2. + private final NoGoodStoreAlphaRoaming store; + private final Assignment assignment; + private int conflictCounter; + + LearnedNoGoodDeletion(NoGoodStoreAlphaRoaming store, Assignment assignment) { + this.store = store; + this.assignment = assignment; + } + + void recordLearnedNoGood(WatchedNoGood learnedWatchedNoGood) { + learnedNoGoods.add(learnedWatchedNoGood); + } + + void increaseConflictCounter() { + conflictCounter++; + } + + boolean needToRunNoGoodDeletion() { + return false; //TODO: disable running of the NoGood deletion for now. Later use something like conflictCounter > 2000; + } + + void runNoGoodDeletion() { + conflictCounter = 0; + int deletedNoGoods = 0; + int originalSize = learnedNoGoods.size(); + if (originalSize == 0) { + return; + } + int toDeleteMax = originalSize / 2; + long activitySum = 0; + for (WatchedNoGood learnedNoGood : learnedNoGoods) { + activitySum += learnedNoGood.getActivity(); + } + double avgActivity = activitySum / originalSize; + double scoreThreshold = avgActivity * 1.5; + for (Iterator iterator = learnedNoGoods.iterator(); iterator.hasNext();) { + WatchedNoGood learnedNoGood = iterator.next(); + if (deletedNoGoods >= toDeleteMax) { + break; + } + boolean keepNoGood = isLocked(learnedNoGood, assignment) + || learnedNoGood.getActivity() > scoreThreshold + || learnedNoGood.isLbdLessOrEqual2(); + if (!keepNoGood) { + iterator.remove(); + store.removeFromWatches(learnedNoGood); + learnedNoGood.decreaseActivity(); + deletedNoGoods++; + LOGGER.trace("Removed from store the NoGood: {}", learnedNoGood); + } + } + LOGGER.debug("Removed {} NoGoods from store.", deletedNoGoods); + } + + private boolean isLocked(WatchedNoGood noGood, Assignment assignment) { + int watchedAtom1 = atomOf(noGood.getLiteral(0)); + int watchedAtom2 = atomOf(noGood.getLiteral(1)); + if (!assignment.isAssigned(watchedAtom1) || !assignment.isAssigned(watchedAtom2)) { + return false; + } + NoGood helperNoGood = new NoGood(noGood.getLiteralsClone()); + // TODO: this is inefficient, the equality check should be a simple object comparison. For that, the assignment needs to store WatchedNoGoods. + return helperNoGood.equals(assignment.getImpliedBy(watchedAtom1)) + || helperNoGood.equals(assignment.getImpliedBy(watchedAtom2)); + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java index eeb2b9ef9..5089664b9 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java @@ -99,6 +99,10 @@ public void backtrack() { public void growForMaxAtomId(int maxAtomId) { } + @Override + public void cleanupLearnedNoGoods() { + } + /** * Infer an assignment from a nogood if it is weakly unit. * diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java index 30fc4d260..36b06172a 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java @@ -35,4 +35,6 @@ public interface NoGoodStore { void backtrack(); void growForMaxAtomId(int maxAtomId); + + void cleanupLearnedNoGoods(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index 21f1bbaa9..9fbde4056 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -27,9 +27,7 @@ */ package at.ac.tuwien.kr.alpha.solver; -import at.ac.tuwien.kr.alpha.Util; import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.common.Literals; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.common.NoGoodInterface; import org.slf4j.Logger; @@ -60,6 +58,7 @@ public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropaga private static final int UNASSIGNED = Integer.MAX_VALUE; private final WritableAssignment assignment; + private LearnedNoGoodDeletion learnedNoGoodDeletion; @SuppressWarnings("unchecked") private ArrayList[] watches = new ArrayList[0]; @SuppressWarnings("unchecked") @@ -71,9 +70,10 @@ public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropaga private boolean didPropagate; private boolean hasBinaryNoGoods; - public NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) { + NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) { this.assignment = assignment; this.checksEnabled = checksEnabled; + this.learnedNoGoodDeletion = new LearnedNoGoodDeletion(this, assignment); } public NoGoodStoreAlphaRoaming(WritableAssignment assignment) { @@ -128,6 +128,25 @@ public void growForMaxAtomId(int maxAtomId) { this.maxAtomId = maxAtomId; } + @Override + public void cleanupLearnedNoGoods() { + if (learnedNoGoodDeletion.needToRunNoGoodDeletion()) { + learnedNoGoodDeletion.runNoGoodDeletion(); + } + } + + void removeFromWatches(WatchedNoGood toRemove) { + int watchedLiteral1 = toRemove.getLiteral(0); + int watchedLiteral2 = toRemove.getLiteral(1); + if (!watches(watchedLiteral2).remove(toRemove) + || !watches(watchedLiteral1).remove(toRemove)) { + throw oops("Could not remove learned NoGood from watch lists."); + } + if (toRemove.hasHead()) { + throw oops("NoGood has a head."); // If this occurs, we need to remove the alpha watch too. + } + } + private ArrayList watches(int literal) { return watches[literal]; } @@ -146,8 +165,7 @@ private void addAlphaWatch(WatchedNoGood wng) { watchesAlpha(literal).add(wng); } - @Override - public ConflictCause add(int id, NoGood noGood) { + public ConflictCause add(int id, NoGood noGood, int lbd) { LOGGER.trace("Adding {}", noGood); if (noGood.isUnary()) { @@ -155,10 +173,15 @@ public ConflictCause add(int id, NoGood noGood) { } else if (noGood.isBinary()) { return addAndWatchBinary(noGood); } else { - return addAndWatch(noGood); + return addAndWatch(noGood, lbd); } } + @Override + public ConflictCause add(int id, NoGood noGood) { + return add(id, noGood, -1); + } + /** * Takes a noGood containing only a single literal and translates it into an assignment (because it * is trivially unit). Still, a check for conflict is performed. @@ -180,7 +203,7 @@ private int strongDecisionLevel(int atom) { return strongDecisionLevel == -1 ? UNASSIGNED : strongDecisionLevel; } - private ConflictCause addAndWatch(final NoGood noGood) { + private ConflictCause addAndWatch(final NoGood noGood, int lbd) { // Collect potential watch candidates. int posWeakUnassigned1 = -1; int posWeakUnassigned2 = -1; @@ -319,6 +342,12 @@ private ConflictCause addAndWatch(final NoGood noGood) { WatchedNoGood wng = new WatchedNoGood(noGood, watch1, watch2, watchAlpha); LOGGER.trace("WatchedNoGood is {}.", wng); + // Record for eventual removal if this NoGood is learned. + if (noGood.getType() == NoGood.Type.LEARNT) { + wng.setLBD(lbd); + learnedNoGoodDeletion.recordLearnedNoGood(wng); + } + if (wng.getAlphaPointer() == -1 && noGood.hasHead()) { throw oops("Did not set alpha watch for nogood with head."); } @@ -552,10 +581,14 @@ private ConflictCause processStronglyWatchedNoGood(WatchedNoGood watchedNoGood, @Override public ConflictCause propagate() { - return propagate(false); + ConflictCause conflictCause = propagate(false); + if (conflictCause != null) { + learnedNoGoodDeletion.increaseConflictCounter(); + } + return conflictCause; } - public ConflictCause propagateOnlyBinaryNoGoods() { + private ConflictCause propagateOnlyBinaryNoGoods() { return propagate(true); } @@ -629,7 +662,7 @@ ConflictCause add(NoGood noGood) { private ConflictCause addHeadedNoGood(NoGood noGood) { if (noGoodsWithHeadSize + 1 > noGoodsWithHead.length) { - noGoodsWithHead = Arrays.copyOf(noGoodsWithHead, Util.arrayGrowthSize(noGoodsWithHeadSize)); + noGoodsWithHead = Arrays.copyOf(noGoodsWithHead, arrayGrowthSize(noGoodsWithHeadSize)); } int otherLiteral = noGood.getLiteral(0) == forLiteral ? noGood.getLiteral(1) : noGood.getLiteral(0); if (isPositive(otherLiteral)) { @@ -655,7 +688,7 @@ private ConflictCause addHeadedNoGood(NoGood noGood) { private ConflictCause addOrdinaryNoGood(NoGood noGood) { if (noGoodsWithoutHeadSize + 1 > noGoodsWithoutHead.length) { - noGoodsWithoutHead = Arrays.copyOf(noGoodsWithoutHead, Util.arrayGrowthSize(noGoodsWithoutHeadSize)); + noGoodsWithoutHead = Arrays.copyOf(noGoodsWithoutHead, arrayGrowthSize(noGoodsWithoutHeadSize)); } int otherLiteral = noGood.getLiteral(0) == forLiteral ? noGood.getLiteral(1) : noGood.getLiteral(0); noGoodsWithoutHead[noGoodsWithoutHeadSize++] = otherLiteral; @@ -672,7 +705,12 @@ private ConflictCause addOrdinaryNoGood(NoGood noGood) { public NoGood getNoGood(int impliedAtom) { return new NoGood(impliedAtom, forLiteral); } - + + @Override + public int[] getReasonLiterals() { + return new int[] {forLiteral}; + } + ConflictCause propagateWeakly() { didPropagate |= noGoodsWithHeadSize > 0 || noGoodsWithoutHeadSize > 0; for (int i = 0; i < noGoodsWithoutHeadSize; i++) { @@ -736,7 +774,7 @@ public int estimate(int atom, boolean truth, Strategy strategy) { } private int getNumberOfBinaryWatches(int atom, boolean truth) { - return binaryWatches[Literals.atomToLiteral(atom, truth)].size(); + return binaryWatches[atomToLiteral(atom, truth)].size(); } private int estimateEffectsOfBinaryNoGoodPropagation(int atom, boolean truth) { @@ -853,6 +891,10 @@ private void checkOrdinaryWatchesInvariant(int atom, boolean truth) { int otherPointer = atom == atomOf(watchedNoGood.getLiteral(1)) ? 0 : 1; int otherLiteral = watchedNoGood.getLiteral(otherPointer); int otherAtom = atomOf(otherLiteral); + int thisAtom = atomOf(watchedNoGood.getLiteral(1 - otherPointer)); + if (thisAtom != atom) { + throw oops("Watched atom is not at first/second position in literals array."); + } Assignment.Entry otherEntry = assignment.get(otherAtom); int otherDecisionLevel = weakDecisionLevel(otherEntry); int otherReplayLevel = weakReplayLevel(otherAtom); 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 feda6d8c0..af67a82d9 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 @@ -62,6 +62,7 @@ public class TrailAssignment implements WritableAssignment, Checkable { private int[] strongDecisionLevels; private ImplicationReasonProvider[] impliedBy; + private int[][] impliedByLiterals; private int[] propagationLevels; private int currentPropagationLevel; private boolean[] callbackUponChange; @@ -84,6 +85,7 @@ public TrailAssignment(AtomStore atomStore, boolean checksEnabled) { this.values = new int[0]; this.strongDecisionLevels = new int[0]; this.impliedBy = new ImplicationReasonProvider[0]; + this.impliedByLiterals = new int[0][]; // TODO: temporary solution, impliedBy should be unified with impliedByLiterals, for that the ImplicationReasonProvider interface must be reworked. this.propagationLevels = new int[0]; this.callbackUponChange = new boolean[0]; this.trailIndicesOfDecisionLevels = new ArrayList<>(); @@ -104,6 +106,7 @@ public void clear() { Arrays.fill(values, 0); Arrays.fill(strongDecisionLevels, -1); Arrays.fill(impliedBy, null); + Arrays.fill(impliedByLiterals, null); currentPropagationLevel = 0; Arrays.fill(propagationLevels, 0); Arrays.fill(callbackUponChange, false); @@ -198,7 +201,7 @@ private void removeLastDecisionLevel() { int start = trailIndicesOfDecisionLevels.get(getDecisionLevel()); ListIterator backtrackIterator = trail.listIterator(start); while (backtrackIterator.hasNext()) { - Integer backtrackAtom = backtrackIterator.next(); + int backtrackAtom = atomOf(backtrackIterator.next()); // Skip already backtracked atoms. if (getTruth(backtrackAtom) == null) { continue; @@ -340,9 +343,11 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationRe // If the atom currently is not assigned, simply record the assignment. final ThriceTruth currentTruth = getTruth(atom); if (currentTruth == null) { - trail.add(atom); + trail.add(atomToLiteral(atom, value.toBoolean())); values[atom] = (getDecisionLevel() << 2) | translateTruth(value); this.impliedBy[atom] = impliedBy; + this.impliedByLiterals[atom] = impliedBy != null ? impliedBy.getReasonLiterals() : null; + // TODO: should be linked to a WatchedNoGood here in order to bump its activity upon getReason()! this.propagationLevels[atom] = ++currentPropagationLevel; // Adjust MBT counter. if (value == MBT) { @@ -375,7 +380,7 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationRe // There is nothing to do except if MBT becomes TRUE. if (currentTruth == MBT && value == TRUE) { // Record new truth value but keep weak decision level unchanged. - trail.add(atom); + trail.add(atomToLiteral(atom, true)); values[atom] = (getWeakDecisionLevel(atom) << 2) | translateTruth(TRUE); // Record strong decision level. strongDecisionLevels[atom] = getDecisionLevel(); @@ -438,11 +443,16 @@ public int getStrongDecisionLevel(int atom) { @Override public NoGood getImpliedBy(int atom) { + // TODO: this method should be retired/refactored. int assignedLiteral = atomToLiteral(atom, getTruth(atom).toBoolean()); // Note that any atom was implied by a literal of opposite truth. return impliedBy[atom] != null ? impliedBy[atom].getNoGood(negateLiteral(assignedLiteral)) : null; } + public int[] getReason(int atom) { + return impliedByLiterals[atom]; + } + @Override public Set getTrueAssignments() { Set result = new HashSet<>(); @@ -531,6 +541,7 @@ public void growForMaxAtomId() { strongDecisionLevels = Arrays.copyOf(strongDecisionLevels, newCapacity); Arrays.fill(strongDecisionLevels, oldLength, strongDecisionLevels.length, -1); impliedBy = Arrays.copyOf(impliedBy, newCapacity); + impliedByLiterals = Arrays.copyOf(impliedByLiterals, newCapacity); propagationLevels = Arrays.copyOf(propagationLevels, newCapacity); callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity); } @@ -544,13 +555,13 @@ public int getNumberOfAssignedAtoms() { } return n; } - + @Override public int getNumberOfAtomsAssignedSinceLastDecision() { Set newlyAssignedAtoms = new HashSet<>(); int trailIndex = trailIndicesOfDecisionLevels.get(getDecisionLevel()); for (; trailIndex < trail.size(); trailIndex++) { - newlyAssignedAtoms.add(trail.get(trailIndex)); + newlyAssignedAtoms.add(atomOf(trail.get(trailIndex))); } return newlyAssignedAtoms.size(); } @@ -601,7 +612,7 @@ private class AssignmentIterator implements Iterator { private void advanceCursorToNextPositiveAssignment() { while (newAssignmentsIterator < trail.size()) { - ThriceTruth truth = getTruth(trail.get(newAssignmentsIterator)); + ThriceTruth truth = getTruth(atomOf(trail.get(newAssignmentsIterator))); if (truth != null && truth.toBoolean()) { return; } @@ -617,7 +628,7 @@ public boolean hasNext() { @Override public Integer next() { - return trail.get(newAssignmentsIterator++); + return atomOf(trail.get(newAssignmentsIterator++)); } } @@ -645,12 +656,12 @@ private class TrailPollable implements Pollable { @Override public int peek() { - return trail.get(nextPositionInTrail); + return atomOf(trail.get(nextPositionInTrail)); } @Override public int remove() { - Integer current = peek(); + int current = peek(); nextPositionInTrail++; return current; } @@ -661,6 +672,36 @@ public boolean isEmpty() { } } + public TrailBackwardsWalker getTrailBackwardsWalker() { + return new TrailBackwardsWalker(); + } + + public class TrailBackwardsWalker { + + int trailPos; + + TrailBackwardsWalker() { + trailPos = trail.size(); + } + + public int getNextLowerLiteral() { + return trail.get(--trailPos); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder("["); + for (Integer literalOnTrail : trail) { + sb.append(isPositive(literalOnTrail) ? "+" + atomOf(literalOnTrail) : "-" + atomOf(literalOnTrail)); + sb.append("@"); + sb.append(TrailAssignment.this.getWeakDecisionLevel(atomOf(literalOnTrail))); + sb.append(", "); + } + sb.append("]"); + return sb.toString(); + } + } + private static final class Entry implements Assignment.Entry { private final ThriceTruth value; private final int decisionLevel; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java index 4e31a8d11..e02b8b20a 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java @@ -10,9 +10,11 @@ import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; public final class WatchedNoGood implements NoGoodInterface, Iterable { + private int activity; private final int[] literals; private int alpha; private int head; + private boolean isLbdLessOrEqual2; WatchedNoGood(NoGood noGood, int a, int b, int alpha) { if (noGood.size() < 3) { @@ -26,6 +28,7 @@ public final class WatchedNoGood implements NoGoodInterface, Iterable { } this.alpha = alpha; head = noGood.hasHead() ? 0 : -1; + activity = 0; if (b == 0) { swap(1, a); } else { @@ -149,4 +152,34 @@ public NoGood getNoGood(int impliedLiteral) { // FIXME: this should not be necessary, the GroundConflictNoGoodLearner should be able to work with WatchedNoGood directly. return new NoGood(literals.clone()); } + + @Override + public int[] getReasonLiterals() { + return literals; + } + + public int getActivity() { + return activity; + } + + void decreaseActivity() { + activity >>= 1; + } + + public void bumpActivity() { + activity++; + } + + void setLBD(int lbd) { + isLbdLessOrEqual2 = lbd <= 2; + } + + boolean isLbdLessOrEqual2() { + return isLbdLessOrEqual2; + } + + int[] getLiteralsClone() { + // TODO: this method should be unnecessary and requires refactoring of implication reasons in the assignment. + return literals.clone(); + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index 5857fd271..d67e50d2c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -34,11 +34,12 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.Collection; -import java.util.LinkedHashSet; +import java.util.*; +import java.util.stream.Collectors; +import java.util.stream.IntStream; 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.*; /** * Copyright (c) 2016, the Alpha Team. @@ -77,15 +78,21 @@ public static class ConflictAnalysisResult { public final int backjumpLevel; public final boolean clearLastChoiceAfterBackjump; public final Collection resolutionAtoms; + public final int lbd; private ConflictAnalysisResult() { learnedNoGood = null; backjumpLevel = -1; clearLastChoiceAfterBackjump = false; resolutionAtoms = null; + lbd = -1; } public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, boolean clearLastChoiceAfterBackjump, Collection resolutionAtoms) { + this(learnedNoGood, backjumpLevel, clearLastChoiceAfterBackjump, resolutionAtoms, -1); + } + + public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, boolean clearLastChoiceAfterBackjump, Collection resolutionAtoms, int lbd) { if (backjumpLevel < 0) { throw oops("Backjumping level is smaller than 0"); } @@ -94,6 +101,7 @@ public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, boolean c this.backjumpLevel = backjumpLevel; this.clearLastChoiceAfterBackjump = clearLastChoiceAfterBackjump; this.resolutionAtoms = resolutionAtoms; + this.lbd = lbd; } @Override @@ -101,7 +109,6 @@ public String toString() { if (this == UNSAT) { return "UNSATISFIABLE"; } - return learnedNoGood + "@" + backjumpLevel; } } @@ -110,18 +117,151 @@ public GroundConflictNoGoodLearner(Assignment assignment) { this.assignment = assignment; } - public ConflictAnalysisResult analyzeConflictingNoGood(NoGood violatedNoGood) { + public ConflictAnalysisResult analyzeConflictingNoGoodOld(NoGood violatedNoGood) { LOGGER.trace("Analyzing violated nogood: {}", violatedNoGood); return analyzeConflictingNoGoodRepetition(violatedNoGood, new LinkedHashSet<>()); } + public ConflictAnalysisResult analyzeConflictingNoGood(NoGood violatedNoGood) { + LOGGER.trace("Analyzing violated nogood: {}", violatedNoGood); + return analyzeTrailBased(violatedNoGood.getReasonLiterals()); + } + + public ConflictAnalysisResult analyzeConflictFromAddingNoGood(NoGood violatedNoGood) { + LOGGER.trace("Analyzing conflict caused by adding the (violated) nogood: {}", violatedNoGood); + // Simply compute appropriate backjumping level. + int removingConflict = backjumpLevelRemovingConflict(violatedNoGood); + if (removingConflict < 0) { + return ConflictAnalysisResult.UNSAT; + } + return new ConflictAnalysisResult(null, removingConflict, false, Collections.emptyList(), -1); + } + + private int backjumpLevelRemovingConflict(NoGood violatedNoGood) { + int highestDL = 0; + for (Integer literal : violatedNoGood) { + int literalDL = assignment.getWeakDecisionLevel(atomOf(literal)); //Math.min(assignment.getWeakDecisionLevel(atomOf(literal)), ((TrailAssignment) assignment).getOutOfOrderDecisionLevel(atomOf(literal))); + if (literalDL > highestDL) { + highestDL = literalDL; + } + } + return highestDL - 1; + } + + private String printReasons(Collection reasons) { + StringBuilder sb = new StringBuilder("{"); + for (int reasonLiteral : reasons) { + sb.append(isPositive(reasonLiteral) ? "+" + atomOf(reasonLiteral) : "-" + atomOf(reasonLiteral)); + sb.append("@"); + sb.append(assignment.getWeakDecisionLevel(atomOf(reasonLiteral))); + sb.append(", "); + } + sb.append("}"); + return sb.toString(); + } + + private String printReasons(int[] reasons) { + return printReasons(IntStream.of(reasons != null ? reasons : new int[0]).boxed().collect(Collectors.toList())); + } + + private ConflictAnalysisResult analyzeTrailBased(int[] conflictReason) { + LOGGER.trace("Analyzing trail based."); + if (assignment.getDecisionLevel() == 0) { + return ConflictAnalysisResult.UNSAT; + } + int numLiteralsInConflictLevel = 0; + ArrayList resolutionLiterals = new ArrayList<>(); + ArrayList resolutionAtoms = new ArrayList<>(); + int currentDecisionLevel = assignment.getDecisionLevel(); + HashSet seenAtoms = new HashSet<>(); // NOTE: other solvers use a global array for seen atoms, this might be slightly faster (initial tests with local arrays showed no significant improvement). + HashSet processedAtoms = new HashSet<>(); // Since trail contains 2 entries for MBT->TRUE assigned atoms, explicitly record which seen atoms have ben processed to avoid processing seen atoms twice. + int[] currentConflictReason = conflictReason; + int backjumpLevel = -1; + TrailAssignment.TrailBackwardsWalker trailWalker = ((TrailAssignment)assignment).getTrailBackwardsWalker(); + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Current trail is: {}", trailWalker); + LOGGER.trace("Violated nogood is: {}", printReasons(conflictReason)); + } + int nextAtom = -1; + do { + // Add current conflict reasons; only add those of lower decision levels, since from current one, only the 1UIP literal will be added. + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Atom {} implied by {}, resolving with that nogood", nextAtom, printReasons(currentConflictReason)); + } + for (int literal : currentConflictReason) { + // Seen atoms have already been dealt with. + if (!seenAtoms.contains(atomOf(literal))) { + seenAtoms.add(atomOf(literal)); + int literalDecisionLevel = assignment.getWeakDecisionLevel(atomOf(literal)); + if (literalDecisionLevel == currentDecisionLevel) { + numLiteralsInConflictLevel++; + } else { + resolutionLiterals.add(literal); + if (literalDecisionLevel > backjumpLevel) { + backjumpLevel = literalDecisionLevel; + } + } + resolutionAtoms.add(atomOf(literal)); + } + } + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("LiteralsInConflictLevel now: {}", numLiteralsInConflictLevel); + LOGGER.trace("Seen atoms are {}.", seenAtoms); + LOGGER.trace("Intermediate learned literals: {}", printReasons(resolutionLiterals)); + } + // Find next literal, i.e. first from top of trail that has been seen but is not yet processed. + do { + int nextLiteral = trailWalker.getNextLowerLiteral(); + nextAtom = atomOf(nextLiteral); + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Next literal on trail is: {}", isPositive(nextLiteral) ? "+" + nextAtom : "-" + nextAtom); + } + + } while (!(seenAtoms.contains(nextAtom) && !processedAtoms.contains(nextAtom))); + currentConflictReason = ((TrailAssignment) assignment).getReason(nextAtom); + processedAtoms.add(nextAtom); + } while (numLiteralsInConflictLevel-- > 1); + // Add the 1UIP literal. + resolutionLiterals.add(atomToLiteral(nextAtom, assignment.getTruth(nextAtom).toBoolean())); + + int[] learnedLiterals = new int[resolutionLiterals.size()]; + int i = 0; + for (Integer resolutionLiteral : resolutionLiterals) { + learnedLiterals[i++] = resolutionLiteral; + } + + NoGood learnedNoGood = NoGood.learnt(learnedLiterals); + LOGGER.trace("Learned NoGood is: {}", learnedNoGood); + + int backjumpingDecisionLevel = computeBackjumpingDecisionLevel(learnedNoGood); + if (backjumpingDecisionLevel < 0) { + // Due to out-of-order assigned literals, the learned nogood may be not assigning. + backjumpingDecisionLevel = computeConflictFreeBackjumpingLevel(learnedNoGood); + if (backjumpingDecisionLevel < 0) { + return ConflictAnalysisResult.UNSAT; + } + } + LOGGER.trace("Backjumping decision level: {}", backjumpingDecisionLevel); + return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, false, resolutionAtoms, computeLBD(learnedLiterals)); + } + + private int computeLBD(int[] literals) { + HashSet occurringDecisionLevels = new HashSet<>(); + for (int literal : literals) { + if (!assignment.isAssigned(atomOf(literal))) { + throw oops("Atom is not assigned: " + atomOf(literal)); + } + occurringDecisionLevels.add(assignment.getWeakDecisionLevel(atomOf(literal))); + } + return occurringDecisionLevels.size(); + } + private ConflictAnalysisResult analyzeConflictingNoGoodRepetition(NoGood violatedNoGood, Collection resolutionAtoms) { NoGood currentResolutionNoGood = violatedNoGood.withoutHead(); // Clone violated NoGood and remove potential head. // Find decision level where conflict occurs (i.e., highest decision level of violatedNoGood). int conflictDecisionLevel = -1; for (Integer literal : currentResolutionNoGood) { - Assignment.Entry literalEntry = assignment.get(atomOf(literal)); - int literalDL = literalEntry.getWeakDecisionLevel(); + int literalDL = assignment.getWeakDecisionLevel(atomOf(literal)); if (literalDL > conflictDecisionLevel) { conflictDecisionLevel = literalDL; } @@ -150,7 +290,7 @@ private ConflictAnalysisResult analyzeConflictingNoGoodRepetition(NoGood violate NoGood otherContributingNoGood = atomAssignmentEntry.getImpliedByRespectingLowerMBT(); if (otherContributingNoGood == null) { // Case b), the other assignment is a decision. - return new ConflictAnalysisResult(null, atomAssignmentEntry.getWeakDecisionLevel(), true, resolutionAtoms); + return new ConflictAnalysisResult(null, atomAssignmentEntry.getWeakDecisionLevel(), true, resolutionAtoms, -1); } // Case a) take other implying NoGood into account. int resolutionAtom = atomAssignmentEntry.getAtom(); @@ -168,17 +308,17 @@ private ConflictAnalysisResult analyzeConflictingNoGoodRepetition(NoGood violate if (backjumpingDecisionLevel < 0) { return repeatAnalysisIfNotAssigning(currentResolutionNoGood, resolutionAtoms); } - return new ConflictAnalysisResult(currentResolutionNoGood, backjumpingDecisionLevel, false, resolutionAtoms); + return new ConflictAnalysisResult(currentResolutionNoGood, backjumpingDecisionLevel, false, resolutionAtoms, -1); } else if (firstUIPPriorityQueue.size() < 1) { // This can happen if some NoGood implied a literal at a higher decision level and later the implying literals become (re-)assigned at lower decision levels. // Lowering the decision level may be possible but requires further analysis. // For the moment, just report the learned NoGood. return repeatAnalysisIfNotAssigning(currentResolutionNoGood, resolutionAtoms); //return new ConflictAnalysisResult(currentResolutionNoGood, computeBackjumpingDecisionLevel(currentResolutionNoGood), false, noGoodsResponsible); - } else if (currentResolutionNoGood.size() > 32) { + } else if (currentResolutionNoGood.size() > 320000) { // Break if resolved NoGood becomes too large. // Remove all current-dl elements from the resolution NoGood and add the last choice, then backjump like usual. - return new ConflictAnalysisResult(null, conflictDecisionLevel, true, resolutionAtoms); // Flag unsatisfiable abused here. + return new ConflictAnalysisResult(null, conflictDecisionLevel, true, resolutionAtoms, -1); // Flag unsatisfiable abused here. /*if (getAssignmentEntryRespectingLowerMBT(lastGuessedAtom).getDecisionLevel() <= conflictDecisionLevel) { // If lastGuessedAtom is not unassigned after backjump, use repeatAnalysisIfNotAssigning. return repeatAnalysisIfNotAssigning(replaceAllFromConflictDecisionLevelWithGuess(currentResolutionNoGood, conflictDecisionLevel, lastGuessedAtom), noGoodsResponsible, lastGuessedAtom); @@ -228,7 +368,7 @@ private ConflictAnalysisResult repeatAnalysisIfNotAssigning(NoGood learnedNoGood // This can only be the case if a literal got assigned at a lower decision level, otherwise the learnedNoGood is always assigning. return analyzeConflictingNoGoodRepetition(learnedNoGood, resolutionAtoms); } - return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, false, resolutionAtoms); + return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, false, resolutionAtoms, -1); } /** From 82b94c0e38f7d8b454c03f2378fbdaede249f999 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 9 Sep 2019 20:59:28 +0200 Subject: [PATCH 19/36] Ignore less unit tests, address @AntoniusW's comments from #146 --- .../java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 2 +- .../at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index 71219b07a..6e8b4fdc7 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -82,6 +82,7 @@ public void testInstance4() throws IOException { @Test(timeout = 60000) public void testSimple() throws IOException { + ignoreTestForNaiveSolver(); testHanoiTower("simple"); } @@ -90,7 +91,6 @@ private void testHanoiTower(int instance) throws IOException { } private void testHanoiTower(String instance) throws IOException { - ignoreTestForNaiveSolver(); Program parsedProgram = parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_Alpha.asp"))); parsedProgram.accumulate(parser.parse(CharStreams.fromPath(Paths.get("src", "test", "resources", "HanoiTower_instances", instance + ".asp")))); Solver solver = getInstance(parsedProgram); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index 89023e06e..55d26ebe5 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -79,17 +79,17 @@ public void testLocstrat_400() throws IOException { @Test(timeout = 15000) public void testReach_1() throws IOException { + ignoreTestForNaiveSolver(); test("reach", "reach-1.txt"); } - @Test(timeout = 15000) + @Test(timeout = 10000) @Ignore("disabled to save resources during CI") public void testReach_4() throws IOException { test("reach", "reach-4.txt"); } private void test(String folder, String aspFileName) throws IOException { - ignoreTestForNaiveSolver(); CharStream programInputStream = CharStreams.fromPath( Paths.get("benchmarks", "omiga", "omiga-testcases", folder, aspFileName) ); From 9f64386d7714f71fea87640a4082e323ed125d18 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 9 Sep 2019 21:07:39 +0200 Subject: [PATCH 20/36] List of choices to be replayed: more tolerance, more verbose docs inspired by @AntoniusW's comments in #174 --- .../kr/alpha/config/CommandLineParser.java | 22 +++++++------------ .../tuwien/kr/alpha/config/SystemConfig.java | 2 +- .../alpha/config/CommandLineParserTest.java | 2 +- 3 files changed, 10 insertions(+), 16 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 94e211135..8b398ce40 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,13 @@ */ package at.ac.tuwien.kr.alpha.config; +import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; +import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; +import org.apache.commons.cli.*; +import org.apache.commons.lang3.StringUtils; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + import java.io.ByteArrayOutputStream; import java.io.FileInputStream; import java.io.PrintWriter; @@ -34,19 +41,6 @@ import java.util.Map; import java.util.function.Consumer; -import org.apache.commons.cli.CommandLine; -import org.apache.commons.cli.DefaultParser; -import org.apache.commons.cli.HelpFormatter; -import org.apache.commons.cli.Option; -import org.apache.commons.cli.Options; -import org.apache.commons.cli.ParseException; -import org.apache.commons.lang3.StringUtils; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; -import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; - /** * Parses given argument lists (as passed when Alpha is called from command line) into {@link AlphaConfig}s and {@link InputConfig}s. * @@ -96,7 +90,7 @@ public class CommandLineParser { .desc("strategy for mom's heuristic (CountBinaryWatches or BinaryNoGoodPropagation, default: " + SystemConfig.DEFAULT_MOMS_STRATEGY.name() + ")") .build(); private static final Option OPT_REPLAY_CHOICES = Option.builder("rc").longOpt("replayChoices").hasArg().argName("choices") - .desc("list of choices (signed atom IDs) to be replayed") + .desc("comma-separated list of choices to be replayed (each choice is represented by a signed integer whose absolute value designates an atom ID and whose sign designates a truth value)") .build(); private static final Option OPT_QUIET = Option.builder("q").longOpt("quiet").desc("do not print answer sets (default: " + SystemConfig.DEFAULT_QUIET) .build(); 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 3a3c70708..a15d60570 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 @@ -192,7 +192,7 @@ public void setReplayChoices(List replayChoices) { } public void setReplayChoices(String replayChoices) { - this.replayChoices = Arrays.stream(replayChoices.split(", ")).map(Integer::valueOf).collect(Collectors.toList()); + this.replayChoices = Arrays.stream(replayChoices.split(",")).map(String::trim).map(Integer::valueOf).collect(Collectors.toList()); } } 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 b89888c44..4bb6623b8 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 @@ -97,7 +97,7 @@ public void noInputGiven() throws ParseException { @Test public void replay() throws ParseException { CommandLineParser parser = new CommandLineParser("java -jar Alpha-bundled.jar", (msg) -> { }); - AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-rc", "\"1, 2, 3\""}); + AlphaConfig alphaConfig = parser.parseCommandLine(new String[]{"-str", "aString.", "-rc", "\"1,2, 3\""}); Assert.assertEquals(Arrays.asList(1, 2, 3), alphaConfig.getAlphaConfig().getReplayChoices()); } From 2fd6fcfdd0262c8064df797fe2d922f22dd5036d Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 9 Sep 2019 21:47:48 +0200 Subject: [PATCH 21/36] Ignore non-default heuristics for certain unit tests to save resources during CI (cf. #146) --- .../tuwien/kr/alpha/solver/AbstractSolverTests.java | 11 ++++++++++- .../at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java | 1 + .../tuwien/kr/alpha/solver/OmigaBenchmarksTest.java | 1 + 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java index a5d1007f7..fe82a5b2a 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java @@ -71,13 +71,22 @@ protected static void enableDebugLog() { } /** - * Calling this method in a tests leads to the test being ignored for the naive solver. + * Calling this method in a test leads to the test being ignored for the naive solver. * Note: use this sparingly and only on tests that require too much run time with the naive solver. */ void ignoreTestForNaiveSolver() { org.junit.Assume.assumeFalse(solverName.equals("naive")); } + /** + * Calling this method in a test leads to the test being ignored for non-default domain-independent heuristics. + * Note: use this sparingly and only on tests that require too much run time with non-default heuristics + * (which are not tuned for good performance as well as VSIDS). + */ + void ignoreNonDefaultDomainIndependentHeuristics() { + org.junit.Assume.assumeTrue(heuristic == BranchingHeuristicFactory.Heuristic.VSIDS); + } + private static String[] getProperty(String subKey, String def) { return System.getProperty("test." + subKey, def).split(","); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java index 6e8b4fdc7..3916070c5 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/HanoiTowerTest.java @@ -83,6 +83,7 @@ public void testInstance4() throws IOException { @Test(timeout = 60000) public void testSimple() throws IOException { ignoreTestForNaiveSolver(); + ignoreNonDefaultDomainIndependentHeuristics(); testHanoiTower("simple"); } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java index 55d26ebe5..6f0b1f674 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/OmigaBenchmarksTest.java @@ -80,6 +80,7 @@ public void testLocstrat_400() throws IOException { @Test(timeout = 15000) public void testReach_1() throws IOException { ignoreTestForNaiveSolver(); + ignoreNonDefaultDomainIndependentHeuristics(); test("reach", "reach-1.txt"); } From ca6104d564f0008aa804cd48d36637a0c3f70b06 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 11 Sep 2019 03:07:04 +0200 Subject: [PATCH 22/36] Enable learned NoGood deletion; large refactoring. - Introduce Antecedent interface for solver-internal representation of NoGoods. - Assignment uses Antecedent as type of impliedBy. - Removed no longer necessary methods from Assignment.Entry. - NoGoods may pass as Antecedent. - Refactored use of Assignment.Entry (in AnalyzeUnjustified and DefaultSolver). - BerkMin and DependencyDrivenHeuristic are aware of conflict analysis potentially being empty. - FirstUIPPriorityQueue no longer necessary and removed. - GroundConflictNoGoodLearner cleaned: use Antecedent instead of NoGood, dead code removed, ConflictAnalysisResult.clearLastChoiceAfterBackjump no longer needed and removed, Antecedent activities are now bumped. - Antecedent renamed from ImplicationReasonProvider, cleaned, and extended for activities. - ConflictCause simplified to only store a violated nogood. - DefaultSolver works with Antecedents and expects complete learning. - LearnedNoGoodDeletion runs cleanup based on an arithmetic sequence. - NaiveNoGoodStore adapted for Antecedents and LBD in NoGood addition. - NaiveSolver cleaned. - NoGoodStore provides NoGood addition with LBD set. - NoGoodStoreAlphaRoaming adapted for Antecedents, uses BinaryAntecedent. - TrailAssignment no longer provides propagationLevels, works with Antecedents now. - WatchedNoGood cleaned. - WritableAssignment works with Antecedents. - BerkMinTest and VSIDSTest adapted to changed ConflictAnalysisResult. - Removed FirstUIPPriorityQueueTest. - GroundConflictNoGoodLearnerTest, NaiveNoGoodStoreTest, and NoGoodStoreAlphaRoamingTest work with Antecedents. --- .../ac/tuwien/kr/alpha/common/Assignment.java | 35 +-- .../at/ac/tuwien/kr/alpha/common/NoGood.java | 32 ++- .../kr/alpha/common/NoGoodInterface.java | 6 +- .../structure/AnalyzeUnjustified.java | 4 +- .../ac/tuwien/kr/alpha/solver/Antecedent.java | 45 ++++ .../tuwien/kr/alpha/solver/ConflictCause.java | 28 +-- .../tuwien/kr/alpha/solver/DefaultSolver.java | 42 ++-- .../solver/ImplicationReasonProvider.java | 12 - .../alpha/solver/LearnedNoGoodDeletion.java | 18 +- .../kr/alpha/solver/NaiveNoGoodStore.java | 15 +- .../tuwien/kr/alpha/solver/NaiveSolver.java | 71 ------ .../tuwien/kr/alpha/solver/NoGoodStore.java | 2 + .../alpha/solver/NoGoodStoreAlphaRoaming.java | 60 +++-- .../kr/alpha/solver/TrailAssignment.java | 122 +++------- .../tuwien/kr/alpha/solver/WatchedNoGood.java | 22 +- .../kr/alpha/solver/WritableAssignment.java | 4 +- .../kr/alpha/solver/heuristics/BerkMin.java | 14 +- .../heuristics/DependencyDrivenHeuristic.java | 6 +- .../learning/FirstUIPPriorityQueue.java | 70 ------ .../learning/GroundConflictNoGoodLearner.java | 217 +++--------------- .../kr/alpha/solver/NaiveNoGoodStoreTest.java | 37 +-- .../solver/NoGoodStoreAlphaRoamingTest.java | 41 ++-- .../alpha/solver/heuristics/BerkMinTest.java | 6 +- .../kr/alpha/solver/heuristics/VSIDSTest.java | 4 +- .../learning/FirstUIPPriorityQueueTest.java | 88 ------- .../GroundConflictNoGoodLearnerTest.java | 12 +- 26 files changed, 298 insertions(+), 715 deletions(-) create mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java delete mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java delete mode 100644 src/main/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueue.java delete mode 100644 src/test/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueueTest.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 27390ae89..19287c3bf 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 @@ -27,6 +27,7 @@ */ package at.ac.tuwien.kr.alpha.common; +import at.ac.tuwien.kr.alpha.solver.Antecedent; import at.ac.tuwien.kr.alpha.solver.ThriceTruth; import java.util.Iterator; @@ -68,7 +69,7 @@ default ThriceTruth getTruth(int atom) { * @param atom the atom. * @return the implying NoGood. */ - NoGood getImpliedBy(int atom); + Antecedent getImpliedBy(int atom); /** * Determines if the given {@code noGood} is undefined in the current assignment. @@ -111,40 +112,10 @@ interface Entry { ThriceTruth getTruth(); int getAtom(); int getDecisionLevel(); - NoGood getImpliedBy(); - int getPropagationLevel(); + Antecedent getImpliedBy(); boolean hasPreviousMBT(); int getMBTDecisionLevel(); - int getMBTPropagationLevel(); - NoGood getMBTImpliedBy(); - - default int getPropagationLevelRespectingLowerMBT() { - return hasPreviousMBT() ? getMBTPropagationLevel() : getPropagationLevel(); - } - - default NoGood getImpliedByRespectingLowerMBT() { - if (hasPreviousMBT()) { - return getMBTImpliedBy(); - } - return getImpliedBy(); - } - - /** - * Returns the literal corresponding to this assignment - * @return atomId if this entry is TRUE/MBT and -atomId if entry is FALSE. - */ - default int getLiteral() { - return atomToLiteral(getAtom(), getTruth().toBoolean()); - } - - /** - * Returns the weakly assigned decision level. - * @return the decision level of a previous MBT if it exists, otherwise the decision level of this entry. - */ - default int getWeakDecisionLevel() { - return hasPreviousMBT() ? getMBTDecisionLevel() : getDecisionLevel(); - } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java index cd603eeaa..d77605e89 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java @@ -27,6 +27,8 @@ */ package at.ac.tuwien.kr.alpha.common; +import at.ac.tuwien.kr.alpha.solver.Antecedent; + import java.util.Arrays; import java.util.Iterator; import java.util.List; @@ -137,6 +139,25 @@ public int size() { return literals.length; } + @Override + public Antecedent asAntecedent() { + return new Antecedent() { + + @Override + public int[] getReasonLiterals() { + return NoGood.this.literals; // Beware: returned array must not be modified! + } + + @Override + public void bumpActivity() { + } + + @Override + public void decreaseActivity() { + } + }; + } + public NoGood withoutHead() { return new NoGood(type, literals.clone()); } @@ -262,17 +283,6 @@ public String toString() { return sb.toString(); } - @Override - public NoGood getNoGood(int impliedAtom) { - return this; - } - - @Override - public int[] getReasonLiterals() { - // TODO: this is dangerous and should not be necessary (requires further solver internal changes). - return literals; - } - /** * The possible nogood types */ diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java index 6d4d0957b..3fd253698 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java @@ -1,11 +1,11 @@ package at.ac.tuwien.kr.alpha.common; -import at.ac.tuwien.kr.alpha.solver.ImplicationReasonProvider; +import at.ac.tuwien.kr.alpha.solver.Antecedent; /** * Copyright (c) 2018, the Alpha Team. */ -public interface NoGoodInterface extends ImplicationReasonProvider { +public interface NoGoodInterface { /** * Returns the literal at the given index. @@ -39,4 +39,6 @@ default boolean isUnary() { default boolean isBinary() { return size() == 2; } + + Antecedent asAntecedent(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java index f8cf9be37..8f17cbe11 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/grounder/structure/AnalyzeUnjustified.java @@ -43,8 +43,8 @@ public Set analyze(int atomToJustify, Assignment currentAssignment) { // If atom instanceof RuleAtom and atom is FALSE, then this comes from a violated constraint in the end and the corresponding rule body can be taken as the single rule deriving the RuleAtom. assignedAtoms = new LinkedHashMap<>(); for (int i = 1; i <= atomStore.getMaxAtomId(); i++) { - Assignment.Entry entry = currentAssignment.get(i); - if (entry == null) { + ThriceTruth truth = currentAssignment.getTruth(i); + if (truth == null) { continue; } Atom assignedAtom = atomStore.get(i); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java new file mode 100644 index 000000000..4729ba01d --- /dev/null +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java @@ -0,0 +1,45 @@ +package at.ac.tuwien.kr.alpha.solver; + +import java.util.HashSet; + +/** + * An interface to reasons of implications as used internally by the solver. This is a lightweight NoGood that only + * provides an array of literals (in some order) and has an activity that may change. + * + * Copyright (c) 2018, the Alpha Team. + */ +public interface Antecedent { + + + int[] getReasonLiterals(); + + void bumpActivity(); + + void decreaseActivity(); + + /** + * Tests whether two Antecedent objects have the same reason literals (irrespective of their order). + * Note that both Antecedents are assumed to contain no duplicate literals. + * @param l left Antecedent. + * @param r right Antecedent + * @return true iff both Antecedents contain the same literals. + */ + static boolean antecedentsEquals(Antecedent l, Antecedent r) { + if (l == r) { + return true; + } + if (l != null && r != null && l.getReasonLiterals().length == r.getReasonLiterals().length) { + HashSet lSet = new HashSet<>(); + for (int literal : l.getReasonLiterals()) { + lSet.add(literal); + } + for (int literal : r.getReasonLiterals()) { + if (!lSet.contains(literal)) { + return false; + } + } + return true; + } + return false; + } +} diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java index b6a08966b..a7ca0d000 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java @@ -1,27 +1,18 @@ package at.ac.tuwien.kr.alpha.solver; -import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.common.NoGood; - +/** + * Indicates the presence of a conflict and contains its reason in terms of a violated Antecedent. + * Throughout the solver the absence of a conflict is indicated by ConflictCause = null. + */ public class ConflictCause { - private final NoGood violatedNoGood; - private final Assignment.Entry violatedChoice; + // Note: directly replacing ConflictCause by Antecedent requires another indicator flag of whether a conflict occurred. + private final Antecedent violatedNoGood; - public ConflictCause(NoGood violatedNoGood) { + public ConflictCause(Antecedent violatedNoGood) { this.violatedNoGood = violatedNoGood; - this.violatedChoice = null; - } - - public ConflictCause(Assignment.Entry violatedChoice) { - this.violatedNoGood = null; - this.violatedChoice = violatedChoice; } - public Assignment.Entry getViolatedChoice() { - return violatedChoice; - } - - public NoGood getViolatedNoGood() { + public Antecedent getAntecedent() { return violatedNoGood; } @@ -30,9 +21,6 @@ public String toString() { if (violatedNoGood != null) { return violatedNoGood.toString(); } - if (violatedChoice != null) { - return violatedChoice.toString(); - } return "null"; } 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 66f7da581..f712e119a 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 @@ -122,7 +122,7 @@ protected boolean tryAdvance(Consumer action) { // Backjump instead of backtrackSlow, enumerationNoGood will invert last choice. choiceManager.backjump(backjumpLevel - 1); LOGGER.debug("Adding enumeration nogood: {}", enumerationNoGood); - if (!addAndBackjumpIfNecessary(grounder.register(enumerationNoGood), enumerationNoGood, -1)) { + if (!addAndBackjumpIfNecessary(grounder.register(enumerationNoGood), enumerationNoGood, Integer.MAX_VALUE)) { return false; } } @@ -141,8 +141,10 @@ protected boolean tryAdvance(Consumer action) { } if (conflictCause != null) { // Learn from conflict. - NoGood violatedNoGood = conflictCause.getViolatedNoGood(); LOGGER.debug("Violating assignment is: {}", assignment); + Antecedent conflictAntecedent = conflictCause.getAntecedent(); + NoGood violatedNoGood = new NoGood(conflictAntecedent.getReasonLiterals().clone()); + // TODO: The violatedNoGood should not be necessary here, but this requires major type changes in heuristics. branchingHeuristic.violatedNoGood(violatedNoGood); if (!afterAllAtomsAssigned) { if (!learnBackjumpAddFromConflict(conflictCause)) { @@ -152,7 +154,7 @@ protected boolean tryAdvance(Consumer action) { } else { LOGGER.debug("Assignment is violated after all unassigned atoms have been assigned false."); conflictsAfterClosing++; - if (!treatConflictAfterClosing(violatedNoGood)) { + if (!treatConflictAfterClosing(conflictAntecedent)) { return false; } afterAllAtomsAssigned = false; @@ -198,7 +200,7 @@ protected boolean tryAdvance(Consumer action) { * @param noGood */ private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd) { - while (((NoGoodStoreAlphaRoaming)store).add(noGoodId, noGood, lbd) != null) { + while (store.add(noGoodId, noGood, lbd) != null) { LOGGER.debug("Adding noGood (again) caused conflict, computing real backjumping level now."); int backjumpLevel = learner.computeConflictFreeBackjumpingLevel(noGood); if (backjumpLevel < 0) { @@ -218,7 +220,7 @@ private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd) * @return false iff the analysis result shows that the set of NoGoods is unsatisfiable. */ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) { - GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getViolatedNoGood()); + GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); LOGGER.debug("Analysis result: {}", analysisResult); @@ -229,11 +231,6 @@ private boolean learnBackjumpAddFromConflict(ConflictCause conflictCause) { branchingHeuristic.analyzedConflict(analysisResult); - if (analysisResult.learnedNoGood == null && analysisResult.clearLastChoiceAfterBackjump) { - // TODO: Temporarily abort resolution with backtrackFast instead of learning a too large nogood. - return backtrack(); - } - if (analysisResult.learnedNoGood != null) { choiceManager.backjump(analysisResult.backjumpLevel); @@ -302,7 +299,7 @@ private NoGood noGoodFromJustificationReasons(int atomToJustify, Set re return NoGood.learnt(reasons); } - private boolean treatConflictAfterClosing(NoGood violatedNoGood) { + private boolean treatConflictAfterClosing(Antecedent violatedNoGood) { if (disableJustificationAfterClosing || disableJustifications || !(grounder instanceof ProgramAnalyzingGrounder)) { // Will not learn from violated NoGood, do simple backtrack. LOGGER.debug("NoGood was violated after all unassigned atoms were assigned to false; will not learn from it; skipping."); @@ -316,8 +313,8 @@ private boolean treatConflictAfterClosing(NoGood violatedNoGood) { LOGGER.debug("Justifying atoms in violated nogood."); LinkedHashSet toJustify = new LinkedHashSet<>(); // Find those literals in violatedNoGood that were just assigned false. - for (Integer literal : violatedNoGood) { - if (assignment.getImpliedBy(atomOf(literal)) == TrailAssignment.CLOSING_INDICATOR_NOGOOD) { + for (Integer literal : violatedNoGood.getReasonLiterals()) { + if (assignment.getImpliedBy(atomOf(literal)) == TrailAssignment.CLOSING_INDICATOR_ANTECEDENT) { toJustify.add(literal); } } @@ -351,9 +348,9 @@ private boolean treatConflictAfterClosing(NoGood violatedNoGood) { continue; } int groundAtomId = atomStore.get(groundAtom); - Assignment.Entry entry = assignment.get(groundAtomId); + Antecedent impliedBy = assignment.getImpliedBy(groundAtomId); // Check if atom was assigned to FALSE during the closing. - if (entry.getImpliedBy() == TrailAssignment.CLOSING_INDICATOR_NOGOOD) { + if (impliedBy == TrailAssignment.CLOSING_INDICATOR_ANTECEDENT) { ruleAtomReplacements.add(atomToNegatedLiteral(groundAtomId)); } } @@ -448,7 +445,7 @@ private boolean ingest(Map obtained) { return false; } - final ConflictCause conflictCause = store.add(entry.getKey(), entry.getValue()); + final ConflictCause conflictCause = store.add(entry.getKey(), entry.getValue(), Integer.MAX_VALUE); if (conflictCause == null) { // There is no conflict, all is fine. Just skip conflict treatment and carry on. continue; @@ -465,25 +462,16 @@ private boolean ingest(Map obtained) { private NoGood fixContradiction(Map.Entry noGoodEntry, ConflictCause conflictCause) { LOGGER.debug("Attempting to fix violation of {} caused by {}", noGoodEntry.getValue(), conflictCause); - if (conflictCause.getViolatedChoice() != null) { - choiceManager.backjump(conflictCause.getViolatedChoice().getDecisionLevel()); - choiceManager.backtrackFast(); - return null; - } - - GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictFromAddingNoGood(conflictCause.getViolatedNoGood()); + GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictFromAddingNoGood(conflictCause.getAntecedent()); if (conflictAnalysisResult == UNSAT) { return NoGood.UNSAT; } branchingHeuristic.analyzedConflict(conflictAnalysisResult); - if (conflictAnalysisResult.learnedNoGood != null || conflictAnalysisResult.clearLastChoiceAfterBackjump) { + if (conflictAnalysisResult.learnedNoGood != null) { throw oops("Unexpectedly learned NoGood after addition of new NoGood caused a conflict."); } choiceManager.backjump(conflictAnalysisResult.backjumpLevel); - if (conflictAnalysisResult.clearLastChoiceAfterBackjump) { - choiceManager.backtrackFast(); - } // If NoGood was learned, add it to the store. // Note that the learned NoGood may cause further conflicts, since propagation on lower decision levels is lazy, diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java deleted file mode 100644 index e7a63169b..000000000 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ImplicationReasonProvider.java +++ /dev/null @@ -1,12 +0,0 @@ -package at.ac.tuwien.kr.alpha.solver; - -import at.ac.tuwien.kr.alpha.common.NoGood; - -/** - * Copyright (c) 2018, the Alpha Team. - */ -public interface ImplicationReasonProvider { - NoGood getNoGood(int impliedLiteral); - - int[] getReasonLiterals(); -} 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 765edcc94..657f467d1 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 @@ -1,7 +1,6 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.Assignment; -import at.ac.tuwien.kr.alpha.common.NoGood; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -17,10 +16,14 @@ */ class LearnedNoGoodDeletion { private static final Logger LOGGER = LoggerFactory.getLogger(LearnedNoGoodDeletion.class); + private static final int RESET_SEQUENCE_AFTER = 20; + private static final int RUN_AFTER_AT_LEAST = 2000; + private static final int GROWTH_FACTOR = 100; private final ArrayList learnedNoGoods = new ArrayList<>(); // List of learned NoGoods that can be removed again. Note: should only contain NoGoods of size > 2. private final NoGoodStoreAlphaRoaming store; private final Assignment assignment; private int conflictCounter; + private int cleanupCounter; LearnedNoGoodDeletion(NoGoodStoreAlphaRoaming store, Assignment assignment) { this.store = store; @@ -36,11 +39,16 @@ void increaseConflictCounter() { } boolean needToRunNoGoodDeletion() { - return false; //TODO: disable running of the NoGood deletion for now. Later use something like conflictCounter > 2000; + return conflictCounter > RUN_AFTER_AT_LEAST + (GROWTH_FACTOR * cleanupCounter); } void runNoGoodDeletion() { conflictCounter = 0; + cleanupCounter++; + // Reset the sequence after enough growth cycles. + if (cleanupCounter > RESET_SEQUENCE_AFTER) { + cleanupCounter = 0; + } int deletedNoGoods = 0; int originalSize = learnedNoGoods.size(); if (originalSize == 0) { @@ -78,9 +86,7 @@ private boolean isLocked(WatchedNoGood noGood, Assignment assignment) { if (!assignment.isAssigned(watchedAtom1) || !assignment.isAssigned(watchedAtom2)) { return false; } - NoGood helperNoGood = new NoGood(noGood.getLiteralsClone()); - // TODO: this is inefficient, the equality check should be a simple object comparison. For that, the assignment needs to store WatchedNoGoods. - return helperNoGood.equals(assignment.getImpliedBy(watchedAtom1)) - || helperNoGood.equals(assignment.getImpliedBy(watchedAtom2)); + return noGood == assignment.getImpliedBy(watchedAtom1) + || noGood == assignment.getImpliedBy(watchedAtom2); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java index 5089664b9..5c479b6f0 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveNoGoodStore.java @@ -27,15 +27,20 @@ void clear() { } @Override - public ConflictCause add(int id, NoGood noGood) { + public ConflictCause add(int id, NoGood noGood, int lbd) { if (assignment.violates(noGood)) { - return new ConflictCause(noGood); + return new ConflictCause(noGood.asAntecedent()); } delegate.put(id, noGood); return null; } + @Override + public ConflictCause add(int id, NoGood noGood) { + return add(id, noGood, Integer.MAX_VALUE); + } + @Override public ConflictCause propagate() { hasInferredAssignments = false; @@ -74,7 +79,7 @@ public ConflictCause propagate() { for (NoGood noGood : delegate.values()) { if (assignment.violates(noGood)) { - return new ConflictCause(noGood); + return new ConflictCause(noGood.asAntecedent()); } } @@ -141,7 +146,7 @@ private ConflictCause propagateWeakly(NoGood noGood) { hasInferredAssignments = true; final int literal = noGood.getLiteral(index); - return assignment.assign(atomOf(literal), isNegated(literal) ? MBT : FALSE, noGood); + return assignment.assign(atomOf(literal), isNegated(literal) ? MBT : FALSE, noGood.asAntecedent()); } /** @@ -187,6 +192,6 @@ private ConflictCause propagateStrongly(NoGood noGood) { hasInferredAssignments = true; - return assignment.assign(headAtom, TRUE, noGood); + return assignment.assign(headAtom, TRUE, noGood.asAntecedent()); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveSolver.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveSolver.java index c72b9e4a9..0622064fd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveSolver.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NaiveSolver.java @@ -28,7 +28,6 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.AnswerSet; -import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.grounder.Grounder; @@ -284,76 +283,6 @@ private void updateGrounderAssignments() { } - private static final class Entry implements Assignment.Entry { - private final ThriceTruth value; - private final int atom; - - Entry(int atom, ThriceTruth value) { - this.value = value; - this.atom = atom; - } - - @Override - public ThriceTruth getTruth() { - return value; - } - - @Override - public int getDecisionLevel() { - throw new UnsupportedOperationException(); - } - - @Override - public boolean hasPreviousMBT() { - throw new UnsupportedOperationException(); - } - - @Override - public int getMBTDecisionLevel() { - throw new UnsupportedOperationException(); - } - - @Override - public int getMBTPropagationLevel() { - throw new UnsupportedOperationException(); - } - - @Override - public int getPropagationLevelRespectingLowerMBT() { - throw new UnsupportedOperationException(); - } - - @Override - public int getWeakDecisionLevel() { - throw new UnsupportedOperationException(); - } - - @Override - public NoGood getMBTImpliedBy() { - throw new UnsupportedOperationException(); - } - - @Override - public NoGood getImpliedBy() { - throw new UnsupportedOperationException(); - } - - @Override - public int getAtom() { - return atom; - } - - @Override - public int getPropagationLevel() { - throw new UnsupportedOperationException(); - } - - @Override - public String toString() { - throw new UnsupportedOperationException(); - } - } - private void obtainNoGoodsFromGrounder() { final int oldSize = knownNoGoods.size(); knownNoGoods.putAll(grounder.getNoGoods(null)); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java index 36b06172a..bcf3619d8 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java @@ -15,6 +15,8 @@ public interface NoGoodStore { * @return {@code null} if the noGood was added without conflict, a {@link ConflictCause} describing * the conflict otherwise. */ + ConflictCause add(int id, NoGood noGood, int lbd); + ConflictCause add(int id, NoGood noGood); /** diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index 9fbde4056..d7cad1e9a 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -165,6 +165,7 @@ private void addAlphaWatch(WatchedNoGood wng) { watchesAlpha(literal).add(wng); } + @Override public ConflictCause add(int id, NoGood noGood, int lbd) { LOGGER.trace("Adding {}", noGood); @@ -177,7 +178,6 @@ public ConflictCause add(int id, NoGood noGood, int lbd) { } } - @Override public ConflictCause add(int id, NoGood noGood) { return add(id, noGood, -1); } @@ -321,7 +321,7 @@ private ConflictCause addAndWatch(final NoGood noGood, int lbd) { watch2 = posWeakHighestAssigned; } else { // NoGood is violated. - return new ConflictCause(noGood); + return new ConflictCause(noGood.asAntecedent()); } // Compute alpha watch: @@ -362,7 +362,7 @@ private ConflictCause addAndWatch(final NoGood noGood, int lbd) { return null; } - private ConflictCause addAndWatchBinary(final NoGood noGood) { + private ConflictCause addAndWatchBinary(final NoGood noGood) { // Shorthands for viewing the nogood as { a, b }. final int a = noGood.getLiteral(0); final int b = noGood.getLiteral(1); @@ -383,7 +383,7 @@ private ConflictCause addAndWatchBinary(final NoGood noGood) { // Check for violation. if (isViolatedA && isViolatedB) { - return new ConflictCause(noGood); + return new ConflictCause(noGood.asAntecedent()); } ConflictCause conflictCause = binaryWatches[a].add(noGood); @@ -397,14 +397,14 @@ private ConflictCause addAndWatchBinary(final NoGood noGood) { private ConflictCause assignWeakComplement(final int literalIndex, final NoGoodInterface impliedBy, int decisionLevel) { final int literal = impliedBy.getLiteral(literalIndex); ThriceTruth truth = isNegated(literal) ? MBT : FALSE; - return assignTruth(atomOf(literal), truth, impliedBy, decisionLevel); + return assignTruth(atomOf(literal), truth, impliedBy.asAntecedent(), decisionLevel); } private ConflictCause assignStrongComplement(final NoGoodInterface impliedBy, int decisionLevel) { - return assignTruth(atomOf(impliedBy.getHead()), TRUE, impliedBy, decisionLevel); + return assignTruth(atomOf(impliedBy.getHead()), TRUE, impliedBy.asAntecedent(), decisionLevel); } - private ConflictCause assignTruth(int atom, ThriceTruth truth, ImplicationReasonProvider impliedBy, int decisionLevel) { + private ConflictCause assignTruth(int atom, ThriceTruth truth, Antecedent impliedBy, int decisionLevel) { ConflictCause cause = assignment.assign(atom, truth, impliedBy, decisionLevel); if (cause == null) { didPropagate = true; @@ -638,7 +638,7 @@ public void setChecksEnabled(boolean checksEnabled) { this.checksEnabled = checksEnabled; } - private class BinaryWatchList implements ImplicationReasonProvider { + private class BinaryWatchList { private int[] noGoodsWithoutHead = new int[10]; private int noGoodsWithoutHeadSize; private int[] noGoodsWithHead = new int[10]; @@ -673,7 +673,7 @@ private ConflictCause addHeadedNoGood(NoGood noGood) { ThriceTruth literalTruth = assignment.getTruth(atomOf(forLiteral)); if (literalTruth != null && literalTruth.toBoolean() == isPositive(forLiteral)) { int weakDecisionLevel = assignment.getWeakDecisionLevel(atomOf(forLiteral)); - ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this, weakDecisionLevel); + ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, new BinaryAntecedent(forLiteral, otherLiteral), weakDecisionLevel); if (conflictCause != null) { return conflictCause; } @@ -681,7 +681,7 @@ private ConflictCause addHeadedNoGood(NoGood noGood) { // Assign head (strongly) if the newly added NoGood is unit. int strongDecisionLevel = assignment.getStrongDecisionLevel(atomOf(forLiteral)); if (strongDecisionLevel != -1 && assignment.getTruth(atomOf(forLiteral)).toBoolean() == isPositive(forLiteral)) { - return assignment.assign(atomOf(otherLiteral), TRUE, this, strongDecisionLevel); + return assignment.assign(atomOf(otherLiteral), TRUE, new BinaryAntecedent(forLiteral, otherLiteral), strongDecisionLevel); } return null; } @@ -696,33 +696,23 @@ private ConflictCause addOrdinaryNoGood(NoGood noGood) { ThriceTruth literalTruth = assignment.getTruth(atomOf(forLiteral)); if (literalTruth != null && literalTruth.toBoolean() == isPositive(forLiteral)) { int weakDecisionLevel = assignment.getWeakDecisionLevel(atomOf(forLiteral)); - return assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this, weakDecisionLevel); + return assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, new BinaryAntecedent(otherLiteral, forLiteral), weakDecisionLevel); } return null; } - @Override - public NoGood getNoGood(int impliedAtom) { - return new NoGood(impliedAtom, forLiteral); - } - - @Override - public int[] getReasonLiterals() { - return new int[] {forLiteral}; - } - ConflictCause propagateWeakly() { didPropagate |= noGoodsWithHeadSize > 0 || noGoodsWithoutHeadSize > 0; for (int i = 0; i < noGoodsWithoutHeadSize; i++) { final int otherLiteral = noGoodsWithoutHead[i]; - ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this); + ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, new BinaryAntecedent(otherLiteral, forLiteral)); if (conflictCause != null) { return conflictCause; } } for (int i = 0; i < noGoodsWithHeadSize; i++) { final int otherLiteral = noGoodsWithHead[i]; - ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this); + ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, new BinaryAntecedent(otherLiteral, forLiteral)); if (conflictCause != null) { return conflictCause; } @@ -734,7 +724,7 @@ ConflictCause propagateStrongly() { didPropagate |= noGoodsWithHeadSize > 0; for (int i = 0; i < noGoodsWithHeadSize; i++) { final int headLiteral = noGoodsWithHead[i]; - ConflictCause conflictCause = assignment.assign(atomOf(headLiteral), TRUE, this); + ConflictCause conflictCause = assignment.assign(atomOf(headLiteral), TRUE, new BinaryAntecedent(headLiteral, forLiteral)); if (conflictCause != null) { return conflictCause; } @@ -750,6 +740,28 @@ public int size() { public String toString() { return "BinaryWatchList(" + forLiteral + ")"; } + + private class BinaryAntecedent implements Antecedent { + private final int[] literals = new int[2]; + + BinaryAntecedent(int lit1, int lit2) { + literals[0] = lit1; + literals[1] = lit2; + } + + @Override + public int[] getReasonLiterals() { + return literals; + } + + @Override + public void bumpActivity() { + } + + @Override + public void decreaseActivity() { + } + } } private void clearOrdinaryWatchList(int literal) { 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 af67a82d9..891828362 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 @@ -29,7 +29,6 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.AtomStore; -import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -47,7 +46,23 @@ */ public class TrailAssignment implements WritableAssignment, Checkable { private static final Logger LOGGER = LoggerFactory.getLogger(TrailAssignment.class); - public static final NoGood CLOSING_INDICATOR_NOGOOD = new NoGood(0); + public static final Antecedent CLOSING_INDICATOR_ANTECEDENT = new Antecedent() { + int[] literals = new int[0]; + + @Override + public int[] getReasonLiterals() { + return literals; + } + + @Override + public void bumpActivity() { + } + + @Override + public void decreaseActivity() { + + } + }; private final AtomStore atomStore; private ChoiceManager choiceManagerCallback; @@ -61,10 +76,7 @@ public class TrailAssignment implements WritableAssignment, Checkable { private int[] values; private int[] strongDecisionLevels; - private ImplicationReasonProvider[] impliedBy; - private int[][] impliedByLiterals; - private int[] propagationLevels; - private int currentPropagationLevel; + private Antecedent[] impliedBy; private boolean[] callbackUponChange; private ArrayList outOfOrderLiterals = new ArrayList<>(); private int highestDecisionLevelContainingOutOfOrderLiterals; @@ -84,11 +96,8 @@ public TrailAssignment(AtomStore atomStore, boolean checksEnabled) { this.atomStore = atomStore; this.values = new int[0]; this.strongDecisionLevels = new int[0]; - this.impliedBy = new ImplicationReasonProvider[0]; - this.impliedByLiterals = new int[0][]; // TODO: temporary solution, impliedBy should be unified with impliedByLiterals, for that the ImplicationReasonProvider interface must be reworked. - this.propagationLevels = new int[0]; + this.impliedBy = new Antecedent[0]; this.callbackUponChange = new boolean[0]; - this.trailIndicesOfDecisionLevels = new ArrayList<>(); this.trailIndicesOfDecisionLevels.add(0); nextPositionInTrail = 0; newAssignmentsIterator = 0; @@ -106,9 +115,6 @@ public void clear() { Arrays.fill(values, 0); Arrays.fill(strongDecisionLevels, -1); Arrays.fill(impliedBy, null); - Arrays.fill(impliedByLiterals, null); - currentPropagationLevel = 0; - Arrays.fill(propagationLevels, 0); Arrays.fill(callbackUponChange, false); outOfOrderLiterals = new ArrayList<>(); highestDecisionLevelContainingOutOfOrderLiterals = 0; @@ -230,7 +236,6 @@ private void removeLastDecisionLevel() { int trailCurrentIndex = trail.size(); int trailPrevIndex = trailIndicesOfDecisionLevels.size() < 1 ? 0 : trailIndicesOfDecisionLevels.get(trailIndicesOfDecisionLevels.size() - 1); - currentPropagationLevel = trailCurrentIndex - trailPrevIndex; // Note: due to MBT->TRUE assignments this may be higher than the actual decision level, but never below. } private void replayOutOfOrderLiterals() { @@ -296,12 +301,11 @@ public ConflictCause choose(int atom, ThriceTruth value) { runInternalChecks(); } trailIndicesOfDecisionLevels.add(trail.size()); - currentPropagationLevel = 0; return assign(atom, value, null); } @Override - public ConflictCause assign(int atom, ThriceTruth value, ImplicationReasonProvider impliedBy) { + public ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy) { ConflictCause conflictCause = assignWithTrail(atom, value, impliedBy); if (conflictCause != null) { LOGGER.debug("Assign is conflicting: atom: {}, value: {}, impliedBy: {}.", atom, value, impliedBy); @@ -310,7 +314,7 @@ public ConflictCause assign(int atom, ThriceTruth value, ImplicationReasonProvid } @Override - public ConflictCause assign(int atom, ThriceTruth value, ImplicationReasonProvider impliedBy, int decisionLevel) { + public ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy, int decisionLevel) { if (decisionLevel < getDecisionLevel()) { outOfOrderLiterals.add(new OutOfOrderLiteral(atom, value, decisionLevel, impliedBy)); if (highestDecisionLevelContainingOutOfOrderLiterals < getDecisionLevel()) { @@ -324,7 +328,7 @@ private boolean assignmentsConsistent(ThriceTruth oldTruth, ThriceTruth value) { return oldTruth == null || oldTruth.toBoolean() == value.toBoolean(); } - private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationReasonProvider impliedBy) { + private ConflictCause assignWithTrail(int atom, ThriceTruth value, Antecedent impliedBy) { if (!isAtom(atom)) { throw new IllegalArgumentException("not an atom"); } @@ -334,8 +338,8 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationRe if (LOGGER.isTraceEnabled()) { LOGGER.trace("Recording assignment {}={}@{} impliedBy: {}", atom, value, getDecisionLevel(), impliedBy); if (impliedBy != null) { - for (Integer literal : impliedBy.getNoGood(literalRepresentation(atom, value))) { - LOGGER.trace("NoGood impliedBy literal assignment: {}={}.", atomOf(literal), get(atomOf(literal))); + for (Integer literal : impliedBy.getReasonLiterals()) { + LOGGER.trace("impliedBy literal assignment: {}={}.", atomOf(literal), get(atomOf(literal))); } } } @@ -346,9 +350,6 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationRe trail.add(atomToLiteral(atom, value.toBoolean())); values[atom] = (getDecisionLevel() << 2) | translateTruth(value); this.impliedBy[atom] = impliedBy; - this.impliedByLiterals[atom] = impliedBy != null ? impliedBy.getReasonLiterals() : null; - // TODO: should be linked to a WatchedNoGood here in order to bump its activity upon getReason()! - this.propagationLevels[atom] = ++currentPropagationLevel; // Adjust MBT counter. if (value == MBT) { mbtCount++; @@ -369,8 +370,7 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationRe if (!assignmentsConsistent(currentTruth, value)) { // Assignments are inconsistent, prepare the reason. // Due to the conflict, the impliedBy NoGood is not the recorded one but the one this method is invoked with.stems from this assignment. - int assignedLiteral = literalRepresentation(atom, value); - return new ConflictCause(impliedBy == null ? null : impliedBy.getNoGood(negateLiteral(assignedLiteral))); + return new ConflictCause(impliedBy); } if (value == TRUE && currentTruth != MBT) { throw oops("Assigning TRUE without assigning MBT before."); @@ -392,10 +392,6 @@ private ConflictCause assignWithTrail(int atom, ThriceTruth value, ImplicationRe throw oops("Assignment conditions are not covered."); } - private int literalRepresentation(int atom, ThriceTruth value) { - return atomToLiteral(atom, value.toBoolean()); - } - private ThriceTruth translateTruth(int value) { switch (value & 0x3) { case 0: @@ -442,15 +438,8 @@ public int getStrongDecisionLevel(int atom) { } @Override - public NoGood getImpliedBy(int atom) { - // TODO: this method should be retired/refactored. - int assignedLiteral = atomToLiteral(atom, getTruth(atom).toBoolean()); - // Note that any atom was implied by a literal of opposite truth. - return impliedBy[atom] != null ? impliedBy[atom].getNoGood(negateLiteral(assignedLiteral)) : null; - } - - public int[] getReason(int atom) { - return impliedByLiterals[atom]; + public Antecedent getImpliedBy(int atom) { + return impliedBy[atom]; } @Override @@ -470,9 +459,9 @@ public Entry get(int atom) { return null; } if (strongDecisionLevels[atom] == -1) { - return new Entry(getTruth(atom), atom, getWeakDecisionLevel(atom), propagationLevels[atom], getImpliedBy(atom)); + return new Entry(getTruth(atom), atom, getWeakDecisionLevel(atom), getImpliedBy(atom)); } else { - return new Entry(getTruth(atom), atom, strongDecisionLevels[atom], propagationLevels[atom], getImpliedBy(atom), getWeakDecisionLevel(atom)); + return new Entry(getTruth(atom), atom, strongDecisionLevels[atom], getImpliedBy(atom), getWeakDecisionLevel(atom)); } } @@ -517,7 +506,7 @@ public boolean closeUnassignedAtoms() { boolean didAssign = false; for (int i = 1; i <= atomStore.getMaxAtomId(); i++) { if (!isAssigned(i)) { - assign(i, FALSE, CLOSING_INDICATOR_NOGOOD); + assign(i, FALSE, CLOSING_INDICATOR_ANTECEDENT); didAssign = true; } } @@ -541,8 +530,6 @@ public void growForMaxAtomId() { strongDecisionLevels = Arrays.copyOf(strongDecisionLevels, newCapacity); Arrays.fill(strongDecisionLevels, oldLength, strongDecisionLevels.length, -1); impliedBy = Arrays.copyOf(impliedBy, newCapacity); - impliedByLiterals = Arrays.copyOf(impliedByLiterals, newCapacity); - propagationLevels = Arrays.copyOf(propagationLevels, newCapacity); callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity); } @@ -637,9 +624,9 @@ private static class OutOfOrderLiteral { final int atom; final ThriceTruth value; final int decisionLevel; - final ImplicationReasonProvider impliedBy; + final Antecedent impliedBy; - private OutOfOrderLiteral(int atom, ThriceTruth value, int decisionLevel, ImplicationReasonProvider impliedBy) { + private OutOfOrderLiteral(int atom, ThriceTruth value, int decisionLevel, Antecedent impliedBy) { this.atom = atom; this.decisionLevel = decisionLevel; this.impliedBy = impliedBy; @@ -705,19 +692,17 @@ public String toString() { private static final class Entry implements Assignment.Entry { private final ThriceTruth value; private final int decisionLevel; - private final int propagationLevel; private final int previousDecisionLevel; - private final NoGood impliedBy; + private final Antecedent impliedBy; private final int atom; - Entry(ThriceTruth value, int atom, int decisionLevel, int propagationLevel, NoGood noGood) { - this(value, atom, decisionLevel, propagationLevel, noGood, -1); + Entry(ThriceTruth value, int atom, int decisionLevel, Antecedent noGood) { + this(value, atom, decisionLevel, noGood, -1); } - Entry(ThriceTruth value, int atom, int decisionLevel, int propagationLevel, NoGood impliedBy, int previousDecisionLevel) { + Entry(ThriceTruth value, int atom, int decisionLevel, Antecedent impliedBy, int previousDecisionLevel) { this.value = value; this.decisionLevel = decisionLevel; - this.propagationLevel = propagationLevel; this.impliedBy = impliedBy; this.previousDecisionLevel = previousDecisionLevel; this.atom = atom; @@ -747,20 +732,7 @@ public int getMBTDecisionLevel() { } @Override - public int getMBTPropagationLevel() { - if (previousDecisionLevel != -1) { - return previousDecisionLevel; - } - throw new UnsupportedOperationException(); - } - - @Override - public NoGood getMBTImpliedBy() { - return impliedBy; - } - - @Override - public NoGood getImpliedBy() { + public Antecedent getImpliedBy() { return impliedBy; } @@ -769,24 +741,6 @@ public int getAtom() { return atom; } - @Override - public int getPropagationLevel() { - if (propagationLevel == -1) { - throw new UnsupportedOperationException(); - } else { - return propagationLevel; - } - } - - @Override - public int getPropagationLevelRespectingLowerMBT() { - if (propagationLevel == -1) { - throw new UnsupportedOperationException(); - } else { - return propagationLevel; - } - } - @Override public boolean equals(Object o) { if (this == o) { @@ -808,7 +762,7 @@ public int hashCode() { @Override public String toString() { - return atom + "=" + value.toString() + "(DL" + decisionLevel + ", PL" + propagationLevel + ")" + return atom + "=" + value.toString() + "(DL" + decisionLevel + ")" + (hasPreviousMBT() ? "MBT(DL" + getMBTDecisionLevel() + ", PL-1 )" : ""); } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java index e02b8b20a..ca7b63dab 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java @@ -9,7 +9,7 @@ import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; import static at.ac.tuwien.kr.alpha.common.Literals.isPositive; -public final class WatchedNoGood implements NoGoodInterface, Iterable { +public final class WatchedNoGood implements NoGoodInterface, Antecedent, Iterable { private int activity; private final int[] literals; private int alpha; @@ -108,6 +108,11 @@ public int size() { return literals.length; } + @Override + public Antecedent asAntecedent() { + return this; + } + @Override public Iterator iterator() { return new Iterator() { @@ -147,12 +152,6 @@ public String toString() { return sb.toString(); } - @Override - public NoGood getNoGood(int impliedLiteral) { - // FIXME: this should not be necessary, the GroundConflictNoGoodLearner should be able to work with WatchedNoGood directly. - return new NoGood(literals.clone()); - } - @Override public int[] getReasonLiterals() { return literals; @@ -162,10 +161,12 @@ public int getActivity() { return activity; } - void decreaseActivity() { + @Override + public void decreaseActivity() { activity >>= 1; } + @Override public void bumpActivity() { activity++; } @@ -177,9 +178,4 @@ void setLBD(int lbd) { boolean isLbdLessOrEqual2() { return isLbdLessOrEqual2; } - - int[] getLiteralsClone() { - // TODO: this method should be unnecessary and requires refactoring of implication reasons in the assignment. - return literals.clone(); - } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/WritableAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/WritableAssignment.java index d4ded40ba..806a29957 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/WritableAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/WritableAssignment.java @@ -60,9 +60,9 @@ public interface WritableAssignment extends Assignment { * @param decisionLevel * @return */ - ConflictCause assign(int atom, ThriceTruth value, ImplicationReasonProvider impliedBy, int decisionLevel); + ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy, int decisionLevel); - default ConflictCause assign(int atom, ThriceTruth value, ImplicationReasonProvider impliedBy) { + default ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy) { return assign(atom, value, impliedBy, getDecisionLevel()); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java index c5b20cc09..09ce31ecd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/BerkMin.java @@ -117,12 +117,16 @@ public void violatedNoGood(NoGood violatedNoGood) { @Override public void analyzedConflict(ConflictAnalysisResult analysisResult) { pushToStack(analysisResult.learnedNoGood); - for (int resolutionAtom : analysisResult.resolutionAtoms) { - incrementActivityCounter(atomToLiteral(resolutionAtom, true)); - incrementActivityCounter(atomToLiteral(resolutionAtom, false)); + if (analysisResult.resolutionAtoms != null) { + for (int resolutionAtom : analysisResult.resolutionAtoms) { + incrementActivityCounter(atomToLiteral(resolutionAtom, true)); + incrementActivityCounter(atomToLiteral(resolutionAtom, false)); + } } - for (int literal : analysisResult.learnedNoGood) { - incrementActivityCounter(literal); + if (analysisResult.learnedNoGood != null) { + for (int literal : analysisResult.learnedNoGood) { + incrementActivityCounter(literal); + } } decayAllIfTimeHasCome(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java index 2f8733ed5..24ba73a79 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/DependencyDrivenHeuristic.java @@ -155,8 +155,10 @@ public void analyzedConflict(ConflictAnalysisResult analysisResult) { incrementActivityCounter(atomToLiteral(resolutionAtom, true)); incrementActivityCounter(atomToLiteral(resolutionAtom, false)); } - for (Integer literal : analysisResult.learnedNoGood) { - incrementSignCounter(literal); + if (analysisResult.learnedNoGood != null) { + for (Integer literal : analysisResult.learnedNoGood) { + incrementSignCounter(literal); + } } decayAllIfTimeHasCome(); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueue.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueue.java deleted file mode 100644 index 91ac719a4..000000000 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueue.java +++ /dev/null @@ -1,70 +0,0 @@ -package at.ac.tuwien.kr.alpha.solver.learning; - -import at.ac.tuwien.kr.alpha.common.Assignment; - -import java.util.Comparator; -import java.util.HashSet; -import java.util.PriorityQueue; -import java.util.Set; - -import static at.ac.tuwien.kr.alpha.Util.oops; - -/** - * Copyright (c) 2016, the Alpha Team. - */ -public class FirstUIPPriorityQueue { - private final PriorityQueue delegate; - private final Set alreadyAdded; - private final int decisionLevel; - - private int lastPollPropagationLevel = Integer.MAX_VALUE; - - public FirstUIPPriorityQueue(int decisionLevel) { - this.decisionLevel = decisionLevel; - this.delegate = new PriorityQueue<>(Comparator.comparing(Assignment.Entry::getPropagationLevelRespectingLowerMBT).reversed()); - this.alreadyAdded = new HashSet<>(); - } - - /** - * Adds a new entry to the queue. The entry is sorted into the queue according to its propagationLevel (highest - * propagationLevel first). If the decisionLevel of the entry does not equal the one of the - * FirstUIPPriorityQueue, the entry is ignored. Duplicate entries are ignored. - * @param entry the entry to add. - */ - public void add(Assignment.Entry entry) { - if (entry.getWeakDecisionLevel() != decisionLevel) { - // Ignore assignments from lower decision levels. - return; - } - if (entry.getPropagationLevelRespectingLowerMBT() > lastPollPropagationLevel) { - throw oops("Adding to 1UIP queue an entry with higher propagationLevel than returned by the last poll"); - } - if (alreadyAdded.contains(entry)) { - // Ignore already added assignments. - return; - } - delegate.add(entry); - alreadyAdded.add(entry); - } - - /** - * Retrieves the first element (i.e., the entry with the highest propagationLevel) from the queue and removes it. - * @return null if the queue is empty. - */ - public Assignment.Entry poll() { - Assignment.Entry firstEntry = delegate.poll(); - if (firstEntry == null) { - return null; - } - lastPollPropagationLevel = firstEntry.getPropagationLevelRespectingLowerMBT(); - return firstEntry; - } - - /** - * Returns the size of the queue. - * @return the size of the underlying queue. - */ - public int size() { - return delegate.size(); - } -} \ No newline at end of file diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index d67e50d2c..7e76b6e23 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -29,6 +29,7 @@ import at.ac.tuwien.kr.alpha.common.Assignment; import at.ac.tuwien.kr.alpha.common.NoGood; +import at.ac.tuwien.kr.alpha.solver.Antecedent; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; import org.apache.commons.lang3.NotImplementedException; import org.slf4j.Logger; @@ -42,6 +43,7 @@ import static at.ac.tuwien.kr.alpha.common.Literals.*; /** + * Conflict-driven clause learning on ground clauses. * Copyright (c) 2016, the Alpha Team. */ public class GroundConflictNoGoodLearner { @@ -53,7 +55,8 @@ public int computeConflictFreeBackjumpingLevel(NoGood violatedNoGood) { int highestDecisionLevel = -1; int secondHighestDecisionLevel = -1; int numAtomsInHighestLevel = 0; - for (Integer literal : violatedNoGood) { + int[] reasonLiterals = violatedNoGood.asAntecedent().getReasonLiterals(); + for (int literal : reasonLiterals) { int literalDecisionLevel = assignment.getRealWeakDecisionLevel(atomOf(literal)); if (literalDecisionLevel == highestDecisionLevel) { numAtomsInHighestLevel++; @@ -76,30 +79,27 @@ public static class ConflictAnalysisResult { public final NoGood learnedNoGood; public final int backjumpLevel; - public final boolean clearLastChoiceAfterBackjump; public final Collection resolutionAtoms; public final int lbd; private ConflictAnalysisResult() { learnedNoGood = null; backjumpLevel = -1; - clearLastChoiceAfterBackjump = false; resolutionAtoms = null; lbd = -1; } - public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, boolean clearLastChoiceAfterBackjump, Collection resolutionAtoms) { - this(learnedNoGood, backjumpLevel, clearLastChoiceAfterBackjump, resolutionAtoms, -1); + public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms) { + this(learnedNoGood, backjumpLevel, resolutionAtoms, -1); } - public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, boolean clearLastChoiceAfterBackjump, Collection resolutionAtoms, int lbd) { + public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms, int lbd) { if (backjumpLevel < 0) { throw oops("Backjumping level is smaller than 0"); } this.learnedNoGood = learnedNoGood; this.backjumpLevel = backjumpLevel; - this.clearLastChoiceAfterBackjump = clearLastChoiceAfterBackjump; this.resolutionAtoms = resolutionAtoms; this.lbd = lbd; } @@ -117,29 +117,25 @@ public GroundConflictNoGoodLearner(Assignment assignment) { this.assignment = assignment; } - public ConflictAnalysisResult analyzeConflictingNoGoodOld(NoGood violatedNoGood) { + public ConflictAnalysisResult analyzeConflictingNoGood(Antecedent violatedNoGood) { LOGGER.trace("Analyzing violated nogood: {}", violatedNoGood); - return analyzeConflictingNoGoodRepetition(violatedNoGood, new LinkedHashSet<>()); + return analyzeTrailBased(violatedNoGood); } - public ConflictAnalysisResult analyzeConflictingNoGood(NoGood violatedNoGood) { - LOGGER.trace("Analyzing violated nogood: {}", violatedNoGood); - return analyzeTrailBased(violatedNoGood.getReasonLiterals()); - } - - public ConflictAnalysisResult analyzeConflictFromAddingNoGood(NoGood violatedNoGood) { + public ConflictAnalysisResult analyzeConflictFromAddingNoGood(Antecedent violatedNoGood) { LOGGER.trace("Analyzing conflict caused by adding the (violated) nogood: {}", violatedNoGood); // Simply compute appropriate backjumping level. int removingConflict = backjumpLevelRemovingConflict(violatedNoGood); if (removingConflict < 0) { return ConflictAnalysisResult.UNSAT; } - return new ConflictAnalysisResult(null, removingConflict, false, Collections.emptyList(), -1); + return new ConflictAnalysisResult(null, removingConflict, Collections.emptyList(), -1); } - private int backjumpLevelRemovingConflict(NoGood violatedNoGood) { + private int backjumpLevelRemovingConflict(Antecedent violatedNoGood) { int highestDL = 0; - for (Integer literal : violatedNoGood) { + int[] reasonLiterals = violatedNoGood.getReasonLiterals(); + for (int literal : reasonLiterals) { int literalDL = assignment.getWeakDecisionLevel(atomOf(literal)); //Math.min(assignment.getWeakDecisionLevel(atomOf(literal)), ((TrailAssignment) assignment).getOutOfOrderDecisionLevel(atomOf(literal))); if (literalDL > highestDL) { highestDL = literalDL; @@ -164,7 +160,7 @@ private String printReasons(int[] reasons) { return printReasons(IntStream.of(reasons != null ? reasons : new int[0]).boxed().collect(Collectors.toList())); } - private ConflictAnalysisResult analyzeTrailBased(int[] conflictReason) { + private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { LOGGER.trace("Analyzing trail based."); if (assignment.getDecisionLevel() == 0) { return ConflictAnalysisResult.UNSAT; @@ -175,12 +171,13 @@ private ConflictAnalysisResult analyzeTrailBased(int[] conflictReason) { int currentDecisionLevel = assignment.getDecisionLevel(); HashSet seenAtoms = new HashSet<>(); // NOTE: other solvers use a global array for seen atoms, this might be slightly faster (initial tests with local arrays showed no significant improvement). HashSet processedAtoms = new HashSet<>(); // Since trail contains 2 entries for MBT->TRUE assigned atoms, explicitly record which seen atoms have ben processed to avoid processing seen atoms twice. - int[] currentConflictReason = conflictReason; + int[] currentConflictReason = conflictReason.getReasonLiterals(); int backjumpLevel = -1; + conflictReason.bumpActivity(); TrailAssignment.TrailBackwardsWalker trailWalker = ((TrailAssignment)assignment).getTrailBackwardsWalker(); if (LOGGER.isTraceEnabled()) { LOGGER.trace("Current trail is: {}", trailWalker); - LOGGER.trace("Violated nogood is: {}", printReasons(conflictReason)); + LOGGER.trace("Violated nogood is: {}", printReasons(conflictReason.getReasonLiterals())); } int nextAtom = -1; do { @@ -218,7 +215,11 @@ private ConflictAnalysisResult analyzeTrailBased(int[] conflictReason) { } } while (!(seenAtoms.contains(nextAtom) && !processedAtoms.contains(nextAtom))); - currentConflictReason = ((TrailAssignment) assignment).getReason(nextAtom); + Antecedent impliedBy = assignment.getImpliedBy(nextAtom); + if (impliedBy != null) { + currentConflictReason = impliedBy.getReasonLiterals(); + impliedBy.bumpActivity(); + } processedAtoms.add(nextAtom); } while (numLiteralsInConflictLevel-- > 1); // Add the 1UIP literal. @@ -242,7 +243,7 @@ private ConflictAnalysisResult analyzeTrailBased(int[] conflictReason) { } } LOGGER.trace("Backjumping decision level: {}", backjumpingDecisionLevel); - return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, false, resolutionAtoms, computeLBD(learnedLiterals)); + return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, resolutionAtoms, computeLBD(learnedLiterals)); } private int computeLBD(int[] literals) { @@ -256,170 +257,6 @@ private int computeLBD(int[] literals) { return occurringDecisionLevels.size(); } - private ConflictAnalysisResult analyzeConflictingNoGoodRepetition(NoGood violatedNoGood, Collection resolutionAtoms) { - NoGood currentResolutionNoGood = violatedNoGood.withoutHead(); // Clone violated NoGood and remove potential head. - // Find decision level where conflict occurs (i.e., highest decision level of violatedNoGood). - int conflictDecisionLevel = -1; - for (Integer literal : currentResolutionNoGood) { - int literalDL = assignment.getWeakDecisionLevel(atomOf(literal)); - if (literalDL > conflictDecisionLevel) { - conflictDecisionLevel = literalDL; - } - } - if (conflictDecisionLevel == 0) { - // The given set of NoGoods is unsatisfiable (conflict at decisionLevel 0). - return ConflictAnalysisResult.UNSAT; - } - FirstUIPPriorityQueue firstUIPPriorityQueue = new FirstUIPPriorityQueue(conflictDecisionLevel); - for (Integer literal : currentResolutionNoGood) { - firstUIPPriorityQueue.add(getAssignmentEntryRespectingLowerMBT(literal)); - //sortLiteralToProcessIntoList(sortedLiteralsToProcess, literal, conflictDecisionLevel); - } - // TODO: create ResolutionSequence - if (firstUIPPriorityQueue.size() == 1) { - // There is only one literal to process, i.e., only one literal in the violatedNoGood is from conflict decision level. - // This means that the NoGood already was unit but got violated, because another NoGood propagated earlier or a wrong choice was made. - // The real conflict therefore is caused by either: - // a) two NoGoods propagating the same atom to different truth values in the current decisionLevel, or - // b) a NoGood propagating at a lower decision level to the inverse value of a choice with higher decision level. - // TODO: b) should no longer be possible, since all propagation is on highest decision level now. - // For a) we need to work also with the other NoGood. - // For b) we need to backtrack the wrong choice. - - Assignment.Entry atomAssignmentEntry = firstUIPPriorityQueue.poll(); - NoGood otherContributingNoGood = atomAssignmentEntry.getImpliedByRespectingLowerMBT(); - if (otherContributingNoGood == null) { - // Case b), the other assignment is a decision. - return new ConflictAnalysisResult(null, atomAssignmentEntry.getWeakDecisionLevel(), true, resolutionAtoms, -1); - } - // Case a) take other implying NoGood into account. - int resolutionAtom = atomAssignmentEntry.getAtom(); - resolutionAtoms.add(resolutionAtom); - currentResolutionNoGood = NoGood.learnt(resolveNoGoods(firstUIPPriorityQueue, currentResolutionNoGood, otherContributingNoGood, resolutionAtom, atomAssignmentEntry.getWeakDecisionLevel(), atomAssignmentEntry.getPropagationLevelRespectingLowerMBT())); - - // TODO: create/edit ResolutionSequence - } - - while (true) { - // Check if 1UIP was reached. - if (firstUIPPriorityQueue.size() == 1) { - // Only one remaining literals to process, we reached 1UIP. - int backjumpingDecisionLevel = computeBackjumpingDecisionLevel(currentResolutionNoGood); - if (backjumpingDecisionLevel < 0) { - return repeatAnalysisIfNotAssigning(currentResolutionNoGood, resolutionAtoms); - } - return new ConflictAnalysisResult(currentResolutionNoGood, backjumpingDecisionLevel, false, resolutionAtoms, -1); - } else if (firstUIPPriorityQueue.size() < 1) { - // This can happen if some NoGood implied a literal at a higher decision level and later the implying literals become (re-)assigned at lower decision levels. - // Lowering the decision level may be possible but requires further analysis. - // For the moment, just report the learned NoGood. - return repeatAnalysisIfNotAssigning(currentResolutionNoGood, resolutionAtoms); - //return new ConflictAnalysisResult(currentResolutionNoGood, computeBackjumpingDecisionLevel(currentResolutionNoGood), false, noGoodsResponsible); - } else if (currentResolutionNoGood.size() > 320000) { - // Break if resolved NoGood becomes too large. - // Remove all current-dl elements from the resolution NoGood and add the last choice, then backjump like usual. - return new ConflictAnalysisResult(null, conflictDecisionLevel, true, resolutionAtoms, -1); // Flag unsatisfiable abused here. - /*if (getAssignmentEntryRespectingLowerMBT(lastGuessedAtom).getDecisionLevel() <= conflictDecisionLevel) { - // If lastGuessedAtom is not unassigned after backjump, use repeatAnalysisIfNotAssigning. - return repeatAnalysisIfNotAssigning(replaceAllFromConflictDecisionLevelWithGuess(currentResolutionNoGood, conflictDecisionLevel, lastGuessedAtom), noGoodsResponsible, lastGuessedAtom); - } - return new ConflictAnalysisResult(replaceAllFromConflictDecisionLevelWithGuess(currentResolutionNoGood, conflictDecisionLevel, lastGuessedAtom), conflictDecisionLevel - 1, false, noGoodsResponsible, false, isLearntTooLarge);*/ - } - - // Resolve next NoGood based on current literal - Assignment.Entry currentLiteralAssignment = firstUIPPriorityQueue.poll(); - int decisionLevel = currentLiteralAssignment.getWeakDecisionLevel(); - int propagationLevel = currentLiteralAssignment.getPropagationLevelRespectingLowerMBT(); - // Get NoGood it was implied by. - NoGood impliedByNoGood = currentLiteralAssignment.getImpliedByRespectingLowerMBT(); - if (impliedByNoGood == null) { - // Literal was a decision, keep it in the currentResolutionNoGood by simply skipping. - continue; - } - if (LOGGER.isDebugEnabled()) { - LOGGER.debug("ImpliedBy NoGood is: {}.", impliedByNoGood); - for (Integer literal : impliedByNoGood) { - LOGGER.debug("Literal assignment: {}={}.", atomOf(literal), assignment.get(atomOf(literal))); - } - } - // TODO: add entry in ResolutionSequence. - - int resolutionAtom = currentLiteralAssignment.getAtom(); - resolutionAtoms.add(resolutionAtom); - currentResolutionNoGood = NoGood.learnt(resolveNoGoods(firstUIPPriorityQueue, currentResolutionNoGood, impliedByNoGood, resolutionAtom, decisionLevel, propagationLevel)); - } - } - - /** - * Returns the Assignment.Entry of a literal. If the literal is TRUE but was MBT before, the (previous) MBT entry is returned. - * @param literal - * @return - */ - private Assignment.Entry getAssignmentEntryRespectingLowerMBT(Integer literal) { - Assignment.Entry literalEntry = assignment.get(atomOf(literal)); - // If current assignment is TRUE and previous was MBT, take previous decision level. - return literalEntry; - } - - private ConflictAnalysisResult repeatAnalysisIfNotAssigning(NoGood learnedNoGood, Collection resolutionAtoms) { - int backjumpingDecisionLevel = computeBackjumpingDecisionLevel(learnedNoGood); - if (backjumpingDecisionLevel < 0) { - // The learned NoGood is not yet assigning, repeat the learning on the now-highest decision level. - // This can only be the case if a literal got assigned at a lower decision level, otherwise the learnedNoGood is always assigning. - return analyzeConflictingNoGoodRepetition(learnedNoGood, resolutionAtoms); - } - return new ConflictAnalysisResult(learnedNoGood, backjumpingDecisionLevel, false, resolutionAtoms, -1); - } - - /** - * Resolves two NoGoods and returns the new NoGood as array of literals. - * Literals of the second NoGood are sorted into the firstUIPPriorityQueue list. - * Literals of the first NoGood are assumed to be already in that queue and not added to it. - * @param firstUIPPriorityQueue - * @param firstNoGood - * @param secondNoGood - * @return - */ - private int[] resolveNoGoods(FirstUIPPriorityQueue firstUIPPriorityQueue, NoGood firstNoGood, NoGood secondNoGood, int resolutionAtom, int resolutionLiteralDecisionLevel, int resolutionLiteralPropagationLevel) { - // Resolve implied nogood into current resolution. - int resolvedLiterals[] = new int[secondNoGood.size() + firstNoGood.size() - 2]; - int resolvedCounter = 0; - // Copy over all literals except the resolving ones. - for (int i = 0; i < firstNoGood.size(); i++) { - if (atomOf(firstNoGood.getLiteral(i)) != resolutionAtom) { - resolvedLiterals[resolvedCounter++] = firstNoGood.getLiteral(i); - } - } - // Copy literals from implying nogood except the resolving one and sort additional literals into processing list. - for (int i = 0; i < secondNoGood.size(); i++) { - if (atomOf(secondNoGood.getLiteral(i)) != resolutionAtom) { - resolvedLiterals[resolvedCounter++] = secondNoGood.getLiteral(i); - - // Sort literal also into queue for further processing. - Assignment.Entry newLiteral = getAssignmentEntryRespectingLowerMBT(secondNoGood.getLiteral(i)); - if (assignment instanceof TrailAssignment) { - firstUIPPriorityQueue.add(newLiteral); - continue; - } - // Check for special case where literal was assigned from MBT to TRUE on the same decisionLevel and the propagationLevel of TRUE is higher than the one of the resolutionLiteral. - if (newLiteral.getDecisionLevel() == resolutionLiteralDecisionLevel - && newLiteral.getPropagationLevel() > resolutionLiteralPropagationLevel) { - if (newLiteral.hasPreviousMBT() - && newLiteral.getMBTDecisionLevel() == resolutionLiteralDecisionLevel - && newLiteral.getMBTPropagationLevel() < resolutionLiteralPropagationLevel) { - // Resort to the previous entry (i.e., the one for MBT) and use that one. - firstUIPPriorityQueue.add(newLiteral); - continue; - } - throw oops("Implying literal on current decisionLevel has higher propagationLevel than the implied literal and this was no assignment from MBT to TRUE"); - } - // Add literal to queue for finding 1UIP. - firstUIPPriorityQueue.add(newLiteral); - } - } - return resolvedLiterals; - } - public ResolutionSequence obtainResolutionSequence() { throw new NotImplementedException("Method not yet implemented."); } @@ -445,9 +282,9 @@ private int computeBackjumpingDecisionLevel(NoGood learnedNoGood) { LOGGER.trace("NoGood has only one literal, backjumping to level: {}", singleLiteralBackjumpingLevel); return singleLiteralBackjumpingLevel; } - for (Integer integer : learnedNoGood) { - Assignment.Entry assignmentEntry = assignment.get(atomOf(integer)); - int atomDecisionLevel = assignmentEntry.getWeakDecisionLevel(); + int[] reasonLiterals = learnedNoGood.asAntecedent().getReasonLiterals(); + for (int integer : reasonLiterals) { + int atomDecisionLevel = assignment.getWeakDecisionLevel(atomOf(integer)); if (assignment instanceof TrailAssignment) { atomDecisionLevel = Math.min(atomDecisionLevel, ((TrailAssignment) assignment).getOutOfOrderDecisionLevel(atomOf(integer))); } 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 32c66ce7e..a167aa8c8 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 @@ -8,6 +8,7 @@ import static at.ac.tuwien.kr.alpha.common.NoGood.fact; import static at.ac.tuwien.kr.alpha.common.NoGood.headFirst; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; +import static at.ac.tuwien.kr.alpha.solver.Antecedent.antecedentsEquals; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.*; import static org.junit.Assert.*; @@ -338,7 +339,7 @@ public void conflictingFact() { assignment.assign(1, FALSE); ConflictCause conflictCause = store.add(1, noGood); assertNotNull(conflictCause); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -348,7 +349,7 @@ public void conflictingBinary() { assignment.assign(1, TRUE); assignment.assign(2, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -359,7 +360,7 @@ public void conflictingNary() { assignment.assign(2, TRUE); assignment.assign(3, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -372,7 +373,7 @@ public void propagateViolatedConstraint() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -395,7 +396,7 @@ public void propagateViolatedConstraintHeadless() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -408,7 +409,7 @@ public void propagateViolatedConstraintHeadlessMbt() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -440,7 +441,7 @@ public void naryNoGoodViolatedDuringAdditionAllTrue() { assertNull(assignment.assign(3, TRUE)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -452,7 +453,7 @@ public void naryNoGoodViolatedDuringAdditionAllMbt() { assertNull(assignment.assign(3, MBT)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -472,7 +473,7 @@ public void binaryNoGoodViolatedDuringAdditionAllTrue() { assertNull(assignment.assign(2, TRUE)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -483,7 +484,7 @@ public void binaryNoGoodViolatedDuringAdditionAllMbt() { assertNull(assignment.assign(2, MBT)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -495,7 +496,7 @@ public void addedViolatedBinaryNoGoodPropagatesAfterBacktracking() { assignment.backtrack(); assertNull(store.add(3, noGood)); store.propagate(); - assertTrue(FALSE.equals(assignment.getTruth(195))); + assertEquals(FALSE, assignment.getTruth(195)); } @Test @@ -508,7 +509,7 @@ public void addedViolatedNaryNoGoodPropagatesAfterBacktracking() { assignment.backtrack(); assertNull(store.add(3, noGood)); store.propagate(); - assertTrue(FALSE.equals(assignment.getTruth(36))); + assertEquals(FALSE, assignment.getTruth(36)); } @Test @@ -517,7 +518,7 @@ public void binaryNoGoodPropagatesTrueFromFalse() { assertNull(store.add(5, noGood)); assertNull(assignment.choose(12, FALSE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @Test @@ -526,7 +527,7 @@ public void binaryNoGoodPropagatesTrueFromTrue() { assertNull(store.add(5, noGood)); assertNull(assignment.choose(12, TRUE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @@ -536,7 +537,7 @@ public void addedBinaryNoGoodPropagatesTrueFromFalse() { NoGood noGood = headFirst(fromOldLiterals(-11, -12)); assertNull(assignment.choose(12, FALSE)); assertNull(store.add(5, noGood)); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @Test @@ -545,7 +546,7 @@ public void addedBinaryNoGoodPropagatesTrueFromTrue() { assertNull(assignment.choose(12, TRUE)); assertNull(store.add(5, noGood)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @Test @@ -556,7 +557,7 @@ public void naryNoGoodPropagatesTrueFromFalse() { store.propagate(); assertNull(assignment.assign(3, FALSE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(1))); + assertEquals(TRUE, assignment.getTruth(1)); } @Test @@ -567,7 +568,7 @@ public void naryNoGoodPropagatesTrueFromTrue() { store.propagate(); assertNull(assignment.assign(2, TRUE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(1))); + assertEquals(TRUE, assignment.getTruth(1)); } @Test 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 da5101cac..730033978 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 @@ -8,6 +8,7 @@ import static at.ac.tuwien.kr.alpha.common.NoGood.fact; import static at.ac.tuwien.kr.alpha.common.NoGood.headFirst; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; +import static at.ac.tuwien.kr.alpha.solver.Antecedent.antecedentsEquals; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.*; import static org.junit.Assert.*; @@ -336,7 +337,7 @@ public void conflictingFact() { assignment.assign(1, FALSE); ConflictCause conflictCause = store.add(1, noGood); assertNotNull(conflictCause); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -345,7 +346,7 @@ public void conflictingBinary() { assignment.assign(1, TRUE); assignment.assign(2, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -355,7 +356,7 @@ public void conflictingNary() { assignment.assign(2, TRUE); assignment.assign(3, TRUE); ConflictCause conflictCause = store.add(1, noGood); - assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -368,7 +369,7 @@ public void propagateViolatedConstraint() { ConflictCause conflictCause = store.propagate(); assertNotNull(conflictCause); assertFalse(store.didPropagate()); - //assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -390,7 +391,7 @@ public void propagateViolatedConstraintHeadless() { ConflictCause conflictCause = store.propagate(); assertFalse(store.didPropagate()); assertNotNull(conflictCause); - //assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -403,7 +404,7 @@ public void propagateViolatedConstraintHeadlessMbt() { ConflictCause conflictCause = store.propagate(); assertFalse(store.didPropagate()); assertNotNull(conflictCause); - //assertEquals(noGood, conflictCause.getViolatedNoGood()); + assertTrue(antecedentsEquals(noGood.asAntecedent(), conflictCause.getAntecedent())); } @Test @@ -434,7 +435,7 @@ public void naryNoGoodViolatedDuringAdditionAllTrue() { assertNull(assignment.assign(3, TRUE)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -445,7 +446,7 @@ public void naryNoGoodViolatedDuringAdditionAllMbt() { assertNull(assignment.assign(3, MBT)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -464,7 +465,7 @@ public void binaryNoGoodViolatedDuringAdditionAllTrue() { assertNull(assignment.assign(2, TRUE)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -474,7 +475,7 @@ public void binaryNoGoodViolatedDuringAdditionAllMbt() { assertNull(assignment.assign(2, MBT)); ConflictCause conflictCause = store.add(11, noGood); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); } @Test @@ -486,7 +487,7 @@ public void addedViolatedBinaryNoGoodPropagatesAfterBacktracking() { assignment.backtrack(); assertNull(store.add(3, noGood)); store.propagate(); - assertTrue(FALSE.equals(assignment.getTruth(195))); + assertEquals(FALSE, assignment.getTruth(195)); } @Test @@ -499,7 +500,7 @@ public void addedViolatedNaryNoGoodPropagatesAfterBacktracking() { assignment.backtrack(); assertNull(store.add(3, noGood)); store.propagate(); - assertTrue(FALSE.equals(assignment.getTruth(36))); + assertEquals(FALSE, assignment.getTruth(36)); } @Test @@ -508,7 +509,7 @@ public void binaryNoGoodPropagatesTrueFromFalse() { assertNull(store.add(5, noGood)); assertNull(assignment.choose(12, FALSE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @Test @@ -517,7 +518,7 @@ public void binaryNoGoodPropagatesTrueFromTrue() { assertNull(store.add(5, noGood)); assertNull(assignment.choose(12, TRUE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @@ -526,7 +527,7 @@ public void addedBinaryNoGoodPropagatesTrueFromFalse() { NoGood noGood = headFirst(fromOldLiterals(-11, -12)); assertNull(assignment.choose(12, FALSE)); assertNull(store.add(5, noGood)); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @Test @@ -535,7 +536,7 @@ public void addedBinaryNoGoodPropagatesTrueFromTrue() { assertNull(assignment.choose(12, TRUE)); assertNull(store.add(5, noGood)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(11))); + assertEquals(TRUE, assignment.getTruth(11)); } @Test @@ -546,7 +547,7 @@ public void naryNoGoodPropagatesTrueFromFalse() { store.propagate(); assertNull(assignment.assign(3, FALSE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(1))); + assertEquals(TRUE, assignment.getTruth(1)); } @Test @@ -557,7 +558,7 @@ public void naryNoGoodPropagatesTrueFromTrue() { store.propagate(); assertNull(assignment.assign(2, TRUE)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(1))); + assertEquals(TRUE, assignment.getTruth(1)); } @Ignore // TrailAssignment no longer propagates at lower decision level. @@ -569,9 +570,9 @@ public void propagationAtLowerDecisionLevel() { assertNull(assignment.choose(4, TRUE)); assertNull(store.add(10, noGood)); store.propagate(); - assertTrue(TRUE.equals(assignment.getTruth(1))); + assertEquals(TRUE, assignment.getTruth(1)); Assignment.Entry entry = assignment.get(1); - assertTrue(TRUE.equals(entry.getTruth())); + assertEquals(TRUE, entry.getTruth()); assertEquals(2, entry.getDecisionLevel()); } 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 b0bf78c84..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 @@ -182,12 +182,12 @@ public void learnNoGood() { int backjumpLevel = 1; boolean clearLastChoiceAfterBackjump = true; Collection resolutionAtoms = Collections.emptySet(); - berkmin.analyzedConflict(new ConflictAnalysisResult(learnedNoGood, backjumpLevel, clearLastChoiceAfterBackjump, - resolutionAtoms)); + berkmin.analyzedConflict(new ConflictAnalysisResult(learnedNoGood, backjumpLevel, + resolutionAtoms)); assertEquals(learnedNoGood, berkmin.getCurrentTopClause()); } private static ConflictAnalysisResult pseudo(NoGood noGood) { - return new ConflictAnalysisResult(noGood, 0, false, Collections.emptySet()); + return new ConflictAnalysisResult(noGood, 0, Collections.emptySet()); } } 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 e63f3c280..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 @@ -93,7 +93,7 @@ public void testConflict() { NoGood learnedNoGood = new NoGood(lit2, lit3); Collection resolutionAtoms = Arrays.asList(1); - ConflictAnalysisResult analysisResult = new ConflictAnalysisResult(learnedNoGood, 1, true, resolutionAtoms); + ConflictAnalysisResult analysisResult = new ConflictAnalysisResult(learnedNoGood, 1, resolutionAtoms); vsids.analyzedConflict(analysisResult); assertEquals(vsids.getActivity(lit1), vsids.getActivity(lit2), DOUBLE_COMPARISON_EPSILON); assertEquals(vsids.getActivity(lit2), vsids.getActivity(lit3), DOUBLE_COMPARISON_EPSILON); @@ -122,7 +122,7 @@ public void testTwoConflicts() { NoGood learnedNoGood = new NoGood(lit1Neg, lit4); Collection resolutionAtoms = Arrays.asList(2); - ConflictAnalysisResult analysisResult = new ConflictAnalysisResult(learnedNoGood, 1, true, resolutionAtoms); + ConflictAnalysisResult analysisResult = new ConflictAnalysisResult(learnedNoGood, 1, resolutionAtoms); vsids.analyzedConflict(analysisResult); assertEquals(activity1 + VSIDS.DEFAULT_DECAY_FACTOR, vsids.getActivity(lit1), DOUBLE_COMPARISON_EPSILON); assertEquals(activity2 + VSIDS.DEFAULT_DECAY_FACTOR, vsids.getActivity(lit2), DOUBLE_COMPARISON_EPSILON); diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueueTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueueTest.java deleted file mode 100644 index 4970e3cb7..000000000 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/learning/FirstUIPPriorityQueueTest.java +++ /dev/null @@ -1,88 +0,0 @@ -package at.ac.tuwien.kr.alpha.solver.learning; - -import at.ac.tuwien.kr.alpha.common.Assignment; -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.ThriceTruth; -import at.ac.tuwien.kr.alpha.solver.TrailAssignment; -import at.ac.tuwien.kr.alpha.solver.WritableAssignment; -import org.junit.Before; -import org.junit.Test; - -import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertTrue; - -/** - * Copyright (c) 2016, the Alpha Team. - */ -public class FirstUIPPriorityQueueTest { - private final AtomStore atomStore; - private final WritableAssignment assignment; - - public FirstUIPPriorityQueueTest() { - atomStore = new AtomStoreImpl(); - assignment = new TrailAssignment(atomStore); - } - - @Before - public void setUp() { - assignment.clear(); - AtomStoreTest.fillAtomStore(atomStore, 4); - assignment.growForMaxAtomId(); - } - - @Test - public void nonlinearEntries() { - assignment.choose(1, ThriceTruth.MBT); - assignment.assign(2, ThriceTruth.TRUE); - assignment.assign(3, ThriceTruth.FALSE); - assignment.assign(4, ThriceTruth.MBT); - - Assignment.Entry entry1 = assignment.get(1); - Assignment.Entry entry2 = assignment.get(2); - Assignment.Entry entry3 = assignment.get(3); - Assignment.Entry entry4 = assignment.get(4); - assertTrue(entry1.getDecisionLevel() == entry2.getDecisionLevel() && entry2.getDecisionLevel() == entry3.getDecisionLevel() && entry3.getDecisionLevel() == entry4.getDecisionLevel()); - assertTrue(entry1.getPropagationLevel() < entry2.getPropagationLevel()); - assertTrue(entry2.getPropagationLevel() < entry3.getPropagationLevel()); - assertTrue(entry3.getPropagationLevel() < entry4.getPropagationLevel()); - - FirstUIPPriorityQueue firstUIPPriorityQueue = new FirstUIPPriorityQueue(entry1.getDecisionLevel()); - firstUIPPriorityQueue.add(entry2); - firstUIPPriorityQueue.add(entry4); - firstUIPPriorityQueue.add(entry3); - - assertEquals(3, firstUIPPriorityQueue.size()); - assertEquals(entry4, firstUIPPriorityQueue.poll()); - assertEquals(entry3, firstUIPPriorityQueue.poll()); - assertEquals(entry2, firstUIPPriorityQueue.poll()); - } - - @Test - public void ignoreDuplicates() { - assignment.choose(1, ThriceTruth.MBT); - assignment.assign(2, ThriceTruth.TRUE); - assignment.assign(3, ThriceTruth.FALSE); - - Assignment.Entry entry1 = assignment.get(1); - Assignment.Entry entry2 = assignment.get(2); - Assignment.Entry entry3 = assignment.get(3); - - FirstUIPPriorityQueue firstUIPPriorityQueue = new FirstUIPPriorityQueue(entry1.getDecisionLevel()); - firstUIPPriorityQueue.add(entry1); - firstUIPPriorityQueue.add(entry2); - firstUIPPriorityQueue.add(entry2); - firstUIPPriorityQueue.add(entry3); - firstUIPPriorityQueue.add(entry2); - firstUIPPriorityQueue.add(entry3); - firstUIPPriorityQueue.add(entry2); - - assertEquals(3, firstUIPPriorityQueue.size()); - assertEquals(entry3, firstUIPPriorityQueue.poll()); - assertEquals(entry2, firstUIPPriorityQueue.poll()); - assertEquals(entry1, firstUIPPriorityQueue.poll()); - assertEquals(null, firstUIPPriorityQueue.poll()); - } - -} \ No newline at end of file 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 997596da4..22584eaa7 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 @@ -9,6 +9,7 @@ import org.junit.Test; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; +import static at.ac.tuwien.kr.alpha.solver.Antecedent.antecedentsEquals; import static org.junit.Assert.*; /** @@ -56,15 +57,14 @@ public void smallConflictNonTrivial1UIP() { assertTrue(store.didPropagate()); assertNotNull(conflictCause); - NoGood violatedNoGood = conflictCause.getViolatedNoGood(); + Antecedent violatedNoGood = conflictCause.getAntecedent(); assertNotNull(violatedNoGood); - assertTrue(violatedNoGood.equals(n5) || violatedNoGood.equals(n7)); - GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(violatedNoGood); + assertTrue(antecedentsEquals(violatedNoGood, n5.asAntecedent()) || antecedentsEquals(violatedNoGood, n7.asAntecedent())); + GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); NoGood learnedNoGood = analysisResult.learnedNoGood; assertEquals(new NoGood(fromOldLiterals(1, -8)), learnedNoGood); int backjumpingDecisionLevel = analysisResult.backjumpLevel; assertEquals(backjumpingDecisionLevel, 2); - assertFalse(analysisResult.clearLastChoiceAfterBackjump); } @Ignore // TrailAssignment no longer propagates at lower decision level. @@ -81,8 +81,8 @@ public void subCurrentDLPropagationWithChoiceCauseOfConflict() { assertEquals(1, assignment.get(2).getDecisionLevel()); ConflictCause conflictCause = store.add(11, n2); assertNotNull(conflictCause); - assertNotNull(conflictCause.getViolatedNoGood()); - GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGood(conflictCause.getViolatedNoGood()); + assertNotNull(conflictCause.getAntecedent()); + GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent()); assertNull(conflictAnalysisResult.learnedNoGood); assertEquals(2, conflictAnalysisResult.backjumpLevel); From a2ca19af14dbc245de41f01a8dd078bd085f3074 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 16 Sep 2019 19:03:17 +0200 Subject: [PATCH 23/36] Refactor solver constructor to accept large config object to stop growing of the constructor's signature --- .../java/at/ac/tuwien/kr/alpha/Alpha.java | 45 ++++++------------- .../tuwien/kr/alpha/solver/DefaultSolver.java | 5 ++- .../tuwien/kr/alpha/solver/SolverFactory.java | 22 +++++++-- .../kr/alpha/solver/AbstractSolverTests.java | 16 +++++-- 4 files changed, 47 insertions(+), 41 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java index fffc4bd57..66a251645 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java @@ -27,24 +27,7 @@ */ package at.ac.tuwien.kr.alpha; -import java.io.IOException; -import java.nio.charset.CodingErrorAction; -import java.nio.file.Files; -import java.nio.file.Paths; -import java.util.List; -import java.util.Map; -import java.util.Random; -import java.util.stream.Stream; - -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.CharStreams; -import org.apache.commons.lang3.StringUtils; - -import at.ac.tuwien.kr.alpha.common.AnswerSet; -import at.ac.tuwien.kr.alpha.common.AtomStore; -import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; -import at.ac.tuwien.kr.alpha.common.Predicate; -import at.ac.tuwien.kr.alpha.common.Program; +import at.ac.tuwien.kr.alpha.common.*; import at.ac.tuwien.kr.alpha.common.fixedinterpretations.PredicateInterpretation; import at.ac.tuwien.kr.alpha.config.InputConfig; import at.ac.tuwien.kr.alpha.config.SystemConfig; @@ -53,8 +36,17 @@ import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.Solver; import at.ac.tuwien.kr.alpha.solver.SolverFactory; -import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration; -import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfigurationBuilder; +import org.antlr.v4.runtime.CharStream; +import org.antlr.v4.runtime.CharStreams; +import org.apache.commons.lang3.StringUtils; + +import java.io.IOException; +import java.nio.charset.CodingErrorAction; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.List; +import java.util.Map; +import java.util.stream.Stream; public class Alpha { @@ -109,22 +101,11 @@ public Program readProgramString(String aspString, Map filter) { String grounderName = this.config.getGrounderName(); - String solverName = this.config.getSolverName(); - String nogoodStoreName = this.config.getNogoodStoreName(); - long seed = this.config.getSeed(); boolean doDebugChecks = this.config.isDebugInternalChecks(); - boolean disableJustificationSearch = this.config.isDisableJustificationSearch(); - - HeuristicsConfigurationBuilder heuristicsConfigurationBuilder = HeuristicsConfiguration.builder(); - heuristicsConfigurationBuilder.setHeuristic(this.config.getBranchingHeuristic()); - heuristicsConfigurationBuilder.setMomsStrategy(this.config.getMomsStrategy()); - AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, doDebugChecks); - Solver solver = SolverFactory.getInstance(solverName, nogoodStoreName, atomStore, grounder, new Random(seed), heuristicsConfigurationBuilder.build(), - doDebugChecks, disableJustificationSearch); - return solver; + return SolverFactory.getInstance(this.config, atomStore, grounder); } public Solver prepareSolverFor(Program program) { 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 f712e119a..212945aff 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 @@ -33,6 +33,7 @@ import at.ac.tuwien.kr.alpha.common.atoms.ComparisonAtom; import at.ac.tuwien.kr.alpha.common.atoms.Literal; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.config.SystemConfig; import at.ac.tuwien.kr.alpha.grounder.Grounder; import at.ac.tuwien.kr.alpha.grounder.NonGroundRule; import at.ac.tuwien.kr.alpha.grounder.ProgramAnalyzingGrounder; @@ -76,7 +77,7 @@ public class DefaultSolver extends AbstractSolver implements SolverMaintainingSt private final PerformanceLog performanceLog; - public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks, boolean disableJustifications) { + public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, WritableAssignment assignment, Random random, SystemConfig config, HeuristicsConfiguration heuristicsConfiguration) { super(atomStore, grounder); this.assignment = assignment; @@ -86,7 +87,7 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.branchingHeuristic = ChainedBranchingHeuristics.chainOf( BranchingHeuristicFactory.getInstance(heuristicsConfiguration, grounder, assignment, choiceManager, random), new NaiveHeuristic(choiceManager)); - this.disableJustifications = disableJustifications; + this.disableJustifications = config.isDisableJustificationSearch(); this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000); } 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 0b1ae49b5..195dee66e 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 @@ -28,18 +28,25 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.common.AtomStore; +import at.ac.tuwien.kr.alpha.config.SystemConfig; 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 java.util.Random; public final class SolverFactory { - public static Solver getInstance(String name, String storeName, AtomStore atomStore, Grounder grounder, Random random, HeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks, boolean disableJustifications) { + public static Solver getInstance(SystemConfig config, AtomStore atomStore, Grounder grounder) { + final String solverName = config.getSolverName(); + final String nogoodStoreName = config.getNogoodStoreName(); + final Random random = new Random(config.getSeed()); + final boolean debugInternalChecks = config.isDebugInternalChecks(); + final HeuristicsConfiguration heuristicsConfiguration = buildHeuristicsConfiguration(config); final WritableAssignment assignment = new TrailAssignment(atomStore, debugInternalChecks); NoGoodStore store; - switch (storeName.toLowerCase()) { + switch (nogoodStoreName.toLowerCase()) { case "naive": store = new NaiveNoGoodStore(assignment); break; @@ -50,12 +57,19 @@ public static Solver getInstance(String name, String storeName, AtomStore atomSt throw new IllegalArgumentException("Unknown store requested."); } - switch (name.toLowerCase()) { + switch (solverName.toLowerCase()) { case "naive" : return new NaiveSolver(atomStore, grounder); case "default": - return new DefaultSolver(atomStore, grounder, store, assignment, random, heuristicsConfiguration, debugInternalChecks, disableJustifications); + return new DefaultSolver(atomStore, grounder, store, assignment, random, config, heuristicsConfiguration); } throw new IllegalArgumentException("Unknown solver requested."); } + + private static HeuristicsConfiguration buildHeuristicsConfiguration(SystemConfig config) { + HeuristicsConfigurationBuilder heuristicsConfigurationBuilder = HeuristicsConfiguration.builder(); + heuristicsConfigurationBuilder.setHeuristic(config.getBranchingHeuristic()); + heuristicsConfigurationBuilder.setMomsStrategy(config.getMomsStrategy()); + return heuristicsConfigurationBuilder.build(); + } } diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java index a5d1007f7..6ef9d4834 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java @@ -32,11 +32,11 @@ import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.AtomStoreImpl; import at.ac.tuwien.kr.alpha.common.Program; +import at.ac.tuwien.kr.alpha.config.SystemConfig; import at.ac.tuwien.kr.alpha.grounder.Grounder; import at.ac.tuwien.kr.alpha.grounder.GrounderFactory; import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory; -import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration; import ch.qos.logback.classic.Level; import ch.qos.logback.classic.Logger; import org.antlr.v4.runtime.CharStream; @@ -149,8 +149,18 @@ public static Collection parameters() { public boolean checks; protected Solver getInstance(AtomStore atomStore, Grounder grounder) { - HeuristicsConfiguration heuristicsConfiguration = HeuristicsConfiguration.builder().setHeuristic(heuristic).build(); - return SolverFactory.getInstance(solverName, storeName, atomStore, grounder, new Random(seed), heuristicsConfiguration, checks, false); + return SolverFactory.getInstance(buildSystemConfig(), atomStore, grounder); + } + + private SystemConfig buildSystemConfig() { + SystemConfig config = new SystemConfig(); + config.setSolverName(solverName); + config.setNogoodStoreName(storeName); + config.setSeed(seed); + config.setBranchingHeuristic(heuristic); + config.setDebugInternalChecks(checks); + config.setDisableJustificationSearch(false); + return config; } protected Solver getInstance(Program program) { From 52ffaa77a6524523ace735acb17b98c787231b01 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 16 Sep 2019 19:49:02 +0200 Subject: [PATCH 24/36] Add option to disable nogood deletion --- .../kr/alpha/config/CommandLineParser.java | 30 +++++++++++-------- .../tuwien/kr/alpha/config/SystemConfig.java | 10 +++++++ .../tuwien/kr/alpha/solver/DefaultSolver.java | 4 ++- 3 files changed, 30 insertions(+), 14 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 5d9941baf..e339ec787 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,13 @@ */ package at.ac.tuwien.kr.alpha.config; +import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; +import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; +import org.apache.commons.cli.*; +import org.apache.commons.lang3.StringUtils; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + import java.io.ByteArrayOutputStream; import java.io.FileInputStream; import java.io.PrintWriter; @@ -34,19 +41,6 @@ import java.util.Map; import java.util.function.Consumer; -import org.apache.commons.cli.CommandLine; -import org.apache.commons.cli.DefaultParser; -import org.apache.commons.cli.HelpFormatter; -import org.apache.commons.cli.Option; -import org.apache.commons.cli.Options; -import org.apache.commons.cli.ParseException; -import org.apache.commons.lang3.StringUtils; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import at.ac.tuwien.kr.alpha.solver.BinaryNoGoodPropagationEstimation; -import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory.Heuristic; - /** * Parses given argument lists (as passed when Alpha is called from command line) into {@link AlphaConfig}s and {@link InputConfig}s. * @@ -106,6 +100,10 @@ public class CommandLineParser { private static final Option OPT_NORMALIZATION_GRID = Option.builder("ng").longOpt("normalizationCountingGrid") .desc("use counting grid normalization instead of sorting circuit for #count (default: " + SystemConfig.DEFAULT_USE_NORMALIZATION_GRID + ")") .build(); + private static final Option OPT_NO_NOGOOD_DELETION = Option.builder("dnd").longOpt("disableNoGoodDeletion") + .desc("disable the deletion of (learned, little active) nogoods (default: " + + SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION + ")") + .build(); private static final Options CLI_OPTS = new Options(); @@ -134,6 +132,7 @@ public class CommandLineParser { CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_STATS); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_JUSTIFICATION); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NORMALIZATION_GRID); + CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_NO_NOGOOD_DELETION); } /* @@ -175,6 +174,7 @@ public CommandLineParser(String cmdLineSyntax, Consumer abortAction) { this.globalOptionHandlers.put(CommandLineParser.OPT_STATS.getOpt(), this::handleStats); this.globalOptionHandlers.put(CommandLineParser.OPT_NO_JUSTIFICATION.getOpt(), this::handleNoJustification); this.globalOptionHandlers.put(CommandLineParser.OPT_NORMALIZATION_GRID.getOpt(), this::handleNormalizationGrid); + this.globalOptionHandlers.put(CommandLineParser.OPT_NO_NOGOOD_DELETION.getOpt(), this::handleNoNoGoodDeletion); this.inputOptionHandlers.put(CommandLineParser.OPT_NUM_ANSWER_SETS.getOpt(), this::handleNumAnswerSets); this.inputOptionHandlers.put(CommandLineParser.OPT_INPUT.getOpt(), this::handleInput); @@ -341,4 +341,8 @@ private void handleNormalizationGrid(Option opt, SystemConfig cfg) { cfg.setUseNormalizationGrid(true); } + private void handleNoNoGoodDeletion(Option opt, SystemConfig cfg) { + cfg.setDisableNoGoodDeletion(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 be2d46d39..b804e7d0a 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 @@ -49,6 +49,7 @@ public class SystemConfig { public static final boolean DEFAULT_DEBUG_INTERNAL_CHECKS = false; public static final boolean DEFAULT_USE_NORMALIZATION_GRID = false; public static final boolean DEFAULT_SORT_ANSWER_SETS = false; + public static final boolean DEFAULT_DISABLE_NOGOOD_DELETION = false; private String grounderName = SystemConfig.DEFAULT_GROUNDER_NAME; private String solverName = SystemConfig.DEFAULT_SOLVER_NAME; @@ -63,6 +64,7 @@ public class SystemConfig { private boolean disableJustificationSearch = SystemConfig.DEFAULT_DISABLE_JUSTIFICATION_SEARCH; private boolean useNormalizationGrid = SystemConfig.DEFAULT_USE_NORMALIZATION_GRID; private boolean sortAnswerSets = SystemConfig.DEFAULT_SORT_ANSWER_SETS; + private boolean disableNoGoodDeletion = SystemConfig.DEFAULT_DISABLE_NOGOOD_DELETION; public String getGrounderName() { return this.grounderName; @@ -176,4 +178,12 @@ public void setSortAnswerSets(boolean sortAnswerSets) { this.sortAnswerSets = sortAnswerSets; } + public boolean isDisableNoGoodDeletion() { + return this.disableNoGoodDeletion; + } + + public void setDisableNoGoodDeletion(boolean disableNoGoodDeletion) { + this.disableNoGoodDeletion = disableNoGoodDeletion; + } + } 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 212945aff..3efb4fc30 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 @@ -74,6 +74,7 @@ public class DefaultSolver extends AbstractSolver implements SolverMaintainingSt private int conflictsAfterClosing; private final boolean disableJustifications; private boolean disableJustificationAfterClosing = true; // Keep disabled for now, case not fully worked out yet. + private final boolean disableNoGoodDeletion; private final PerformanceLog performanceLog; @@ -88,6 +89,7 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, BranchingHeuristicFactory.getInstance(heuristicsConfiguration, grounder, assignment, choiceManager, random), new NaiveHeuristic(choiceManager)); this.disableJustifications = config.isDisableJustificationSearch(); + this.disableNoGoodDeletion = config.isDisableNoGoodDeletion(); this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000); } @@ -136,7 +138,7 @@ protected boolean tryAdvance(Consumer action) { ConflictCause conflictCause = store.propagate(); didChange |= store.didPropagate(); LOGGER.trace("Assignment after propagation is: {}", assignment); - if (conflictCause == null) { + if (!disableNoGoodDeletion && conflictCause == null) { // Run learned NoGood deletion strategy. store.cleanupLearnedNoGoods(); } From 3926b67f0182b6cb9dc829524cc4e48d0c8ca4aa Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 16 Sep 2019 23:55:51 +0200 Subject: [PATCH 25/36] Apply suggestions from code review Co-Authored-By: Richard Taupe --- src/main/java/at/ac/tuwien/kr/alpha/common/Assignment.java | 2 +- src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java | 4 ++-- .../java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java | 7 ++----- .../ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletion.java | 2 +- .../ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java | 4 ++-- 5 files changed, 8 insertions(+), 11 deletions(-) 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 19287c3bf..373f9dea5 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 @@ -67,7 +67,7 @@ default ThriceTruth getTruth(int atom) { /** * Returns the NoGood that implied the atom. * @param atom the atom. - * @return the implying NoGood. + * @return the implying Antecedent. */ Antecedent getImpliedBy(int atom); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java index 4729ba01d..9d0b9cd23 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java @@ -3,10 +3,10 @@ import java.util.HashSet; /** - * An interface to reasons of implications as used internally by the solver. This is a lightweight NoGood that only + * An interface to reasons of implications as used internally by the solver. This is a lightweight {@link at.ac.tuwien.kr.alpha.common.NoGood} that only * provides an array of literals (in some order) and has an activity that may change. * - * Copyright (c) 2018, the Alpha Team. + * Copyright (c) 2019, the Alpha Team. */ public interface Antecedent { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java index a7ca0d000..ac9df1aef 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java @@ -2,7 +2,7 @@ /** * Indicates the presence of a conflict and contains its reason in terms of a violated Antecedent. - * Throughout the solver the absence of a conflict is indicated by ConflictCause = null. + * Throughout the solver the absence of a conflict is indicated by {@code ConflictCause = null}. */ public class ConflictCause { // Note: directly replacing ConflictCause by Antecedent requires another indicator flag of whether a conflict occurred. @@ -18,10 +18,7 @@ public Antecedent getAntecedent() { @Override public String toString() { - if (violatedNoGood != null) { - return violatedNoGood.toString(); - } - return "null"; + return String.valueOf(violatedNoGood); } } 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 657f467d1..829f866ee 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 @@ -59,7 +59,7 @@ void runNoGoodDeletion() { for (WatchedNoGood learnedNoGood : learnedNoGoods) { activitySum += learnedNoGood.getActivity(); } - double avgActivity = activitySum / originalSize; + double avgActivity = (double) activitySum / originalSize; double scoreThreshold = avgActivity * 1.5; for (Iterator iterator = learnedNoGoods.iterator(); iterator.hasNext();) { WatchedNoGood learnedNoGood = iterator.next(); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index d7cad1e9a..6824b0452 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -58,7 +58,7 @@ public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropaga private static final int UNASSIGNED = Integer.MAX_VALUE; private final WritableAssignment assignment; - private LearnedNoGoodDeletion learnedNoGoodDeletion; + private final LearnedNoGoodDeletion learnedNoGoodDeletion; @SuppressWarnings("unchecked") private ArrayList[] watches = new ArrayList[0]; @SuppressWarnings("unchecked") @@ -957,4 +957,4 @@ private boolean watchInvariant(boolean atomSatisfies, int atomDecisionLevel, int return false; } } -} \ No newline at end of file +} From 3ec113503a0227f9c45dcf4450a0d62c1987888e Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 17 Sep 2019 01:17:36 +0200 Subject: [PATCH 26/36] Addressing comments from review. --- .../ac/tuwien/kr/alpha/common/Assignment.java | 8 +++-- .../ac/tuwien/kr/alpha/solver/Antecedent.java | 28 ---------------- .../tuwien/kr/alpha/solver/ConflictCause.java | 6 ++-- .../tuwien/kr/alpha/solver/DefaultSolver.java | 8 +++-- .../tuwien/kr/alpha/solver/NoGoodStore.java | 18 +++++++++-- .../kr/alpha/solver/TrailAssignment.java | 7 ++-- .../learning/GroundConflictNoGoodLearner.java | 23 +++++++------ .../kr/alpha/solver/AntecedentTest.java | 32 +++++++++++++++++++ .../kr/alpha/solver/NaiveNoGoodStoreTest.java | 2 +- .../solver/NoGoodStoreAlphaRoamingTest.java | 2 +- .../GroundConflictNoGoodLearnerTest.java | 2 +- 11 files changed, 82 insertions(+), 54 deletions(-) create mode 100644 src/test/java/at/ac/tuwien/kr/alpha/solver/AntecedentTest.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 373f9dea5..638696fce 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 @@ -87,11 +87,15 @@ default boolean isUndefined(NoGood noGood) { } /** - * Returns an iterator over all new assignments. New assignments are only returned once. - * @return an iterator over all new assignments to TRUE or MBT. + * Returns an iterator over all newly assigned atoms. New assignments are only returned once. + * @return an iterator over all atoms newly assigned to TRUE or MBT. */ Iterator getNewPositiveAssignmentsIterator(); + /** + * Returns the new assignments to process. + * @return a Pollable that yields the atoms that were newly assigned. + */ Pollable getAssignmentsToProcess(); /** diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java index 9d0b9cd23..c841ecc0e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/Antecedent.java @@ -1,7 +1,5 @@ package at.ac.tuwien.kr.alpha.solver; -import java.util.HashSet; - /** * An interface to reasons of implications as used internally by the solver. This is a lightweight {@link at.ac.tuwien.kr.alpha.common.NoGood} that only * provides an array of literals (in some order) and has an activity that may change. @@ -10,36 +8,10 @@ */ public interface Antecedent { - int[] getReasonLiterals(); void bumpActivity(); void decreaseActivity(); - /** - * Tests whether two Antecedent objects have the same reason literals (irrespective of their order). - * Note that both Antecedents are assumed to contain no duplicate literals. - * @param l left Antecedent. - * @param r right Antecedent - * @return true iff both Antecedents contain the same literals. - */ - static boolean antecedentsEquals(Antecedent l, Antecedent r) { - if (l == r) { - return true; - } - if (l != null && r != null && l.getReasonLiterals().length == r.getReasonLiterals().length) { - HashSet lSet = new HashSet<>(); - for (int literal : l.getReasonLiterals()) { - lSet.add(literal); - } - for (int literal : r.getReasonLiterals()) { - if (!lSet.contains(literal)) { - return false; - } - } - return true; - } - return false; - } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java index ac9df1aef..b9b72ca58 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ConflictCause.java @@ -5,7 +5,10 @@ * Throughout the solver the absence of a conflict is indicated by {@code ConflictCause = null}. */ public class ConflictCause { - // Note: directly replacing ConflictCause by Antecedent requires another indicator flag of whether a conflict occurred. + // Note: Storing the Antecedent is necessary in order to distinguish the cases of no conflict occurring + // {@code ConflictCause==null} from the case where a choice (with no Antecedent, i.e., + // {@code violatedNoGood==null}) is the cause of the conflict. + // Resolving ConflictCause by Antecedent would require an indicator flag to distinguish these cases. private final Antecedent violatedNoGood; public ConflictCause(Antecedent violatedNoGood) { @@ -18,7 +21,6 @@ public Antecedent getAntecedent() { @Override public String toString() { - return String.valueOf(violatedNoGood); } } 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 3efb4fc30..2a683bf50 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 @@ -50,6 +50,7 @@ import static at.ac.tuwien.kr.alpha.Util.oops; import static at.ac.tuwien.kr.alpha.common.Literals.*; +import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.MBT; import static at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristic.DEFAULT_CHOICE_LITERAL; import static at.ac.tuwien.kr.alpha.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult.UNSAT; @@ -199,8 +200,9 @@ protected boolean tryAdvance(Consumer action) { /** * Adds a noGood to the store and in case of out-of-order literals causing another conflict, triggers further backjumping. - * @param noGoodId - * @param noGood + * @param noGoodId the unique identifier of the NoGood to add. + * @param noGood the NoGood to add. + * @param lbd the LBD (literal blocks distance) value of the NoGood. */ private boolean addAndBackjumpIfNecessary(int noGoodId, NoGood noGood, int lbd) { while (store.add(noGoodId, noGood, lbd) != null) { @@ -479,7 +481,7 @@ private NoGood fixContradiction(Map.Entry noGoodEntry, Conflict // If NoGood was learned, add it to the store. // Note that the learned NoGood may cause further conflicts, since propagation on lower decision levels is lazy, // hence backtracking once might not be enough to remove the real conflict cause. - if (!addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue(), -1)) { + if (!addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue(), LBD_NO_VALUE)) { return NoGood.UNSAT; } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java index bcf3619d8..3b3b184cd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStore.java @@ -3,20 +3,30 @@ import at.ac.tuwien.kr.alpha.common.NoGood; /** - * An interface defining the use of a nogood store. + * An interface defining the use of a NoGood store. * - * Copyright (c) 2016, the Alpha Team. + * Copyright (c) 2016-2019, the Alpha Team. */ public interface NoGoodStore { + int LBD_NO_VALUE = -1; + /** * Adds a nogood with the given id. * @param id the unique identifier of the nogood. * @param noGood the nogood to add. + * @param lbd the literals block distance. * @return {@code null} if the noGood was added without conflict, a {@link ConflictCause} describing * the conflict otherwise. */ ConflictCause add(int id, NoGood noGood, int lbd); + /** + * Adds a NoGood with no LBD value set. + * @param id the unique identifier of the NoGood. + * @param noGood the NoGood to add. + * @return {@code null} if the noGood was added without conflict, a {@link ConflictCause} describing +* * the conflict otherwise. + */ ConflictCause add(int id, NoGood noGood); /** @@ -38,5 +48,9 @@ public interface NoGoodStore { void growForMaxAtomId(int maxAtomId); + /** + * Tests whether a cleanup of the learned NoGoods database is appropriate and exectutes the cleaning if + * necessary. + */ void cleanupLearnedNoGoods(); } 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 891828362..9c4640d01 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 @@ -42,7 +42,10 @@ import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.*; /** - * An implementation of Assignment using a trail and arrays as underlying structures for storing assignments. + * An implementation of Assignment using a trail (of literals) and arrays as underlying structures for storing + * assignments. + * + * Copyright (c) 2018-2019, the Alpha Team. */ public class TrailAssignment implements WritableAssignment, Checkable { private static final Logger LOGGER = LoggerFactory.getLogger(TrailAssignment.class); @@ -763,7 +766,7 @@ public int hashCode() { @Override public String toString() { return atom + "=" + value.toString() + "(DL" + decisionLevel + ")" - + (hasPreviousMBT() ? "MBT(DL" + getMBTDecisionLevel() + ", PL-1 )" : ""); + + (hasPreviousMBT() ? "MBT(DL" + getMBTDecisionLevel() + ")" : ""); } } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index 7e76b6e23..9f48b13b7 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -31,20 +31,23 @@ import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.Antecedent; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; -import org.apache.commons.lang3.NotImplementedException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.*; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; import java.util.stream.Collectors; import java.util.stream.IntStream; import static at.ac.tuwien.kr.alpha.Util.oops; import static at.ac.tuwien.kr.alpha.common.Literals.*; +import static at.ac.tuwien.kr.alpha.solver.NoGoodStore.LBD_NO_VALUE; /** - * Conflict-driven clause learning on ground clauses. - * Copyright (c) 2016, the Alpha Team. + * Conflict-driven learning on ground clauses. + * Copyright (c) 2016-2019, the Alpha Team. */ public class GroundConflictNoGoodLearner { private static final Logger LOGGER = LoggerFactory.getLogger(GroundConflictNoGoodLearner.class); @@ -86,11 +89,11 @@ private ConflictAnalysisResult() { learnedNoGood = null; backjumpLevel = -1; resolutionAtoms = null; - lbd = -1; + lbd = LBD_NO_VALUE; } public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms) { - this(learnedNoGood, backjumpLevel, resolutionAtoms, -1); + this(learnedNoGood, backjumpLevel, resolutionAtoms, LBD_NO_VALUE); } public ConflictAnalysisResult(NoGood learnedNoGood, int backjumpLevel, Collection resolutionAtoms, int lbd) { @@ -129,14 +132,14 @@ public ConflictAnalysisResult analyzeConflictFromAddingNoGood(Antecedent violate if (removingConflict < 0) { return ConflictAnalysisResult.UNSAT; } - return new ConflictAnalysisResult(null, removingConflict, Collections.emptyList(), -1); + return new ConflictAnalysisResult(null, removingConflict, Collections.emptyList(), LBD_NO_VALUE); } private int backjumpLevelRemovingConflict(Antecedent violatedNoGood) { int highestDL = 0; int[] reasonLiterals = violatedNoGood.getReasonLiterals(); for (int literal : reasonLiterals) { - int literalDL = assignment.getWeakDecisionLevel(atomOf(literal)); //Math.min(assignment.getWeakDecisionLevel(atomOf(literal)), ((TrailAssignment) assignment).getOutOfOrderDecisionLevel(atomOf(literal))); + int literalDL = assignment.getWeakDecisionLevel(atomOf(literal)); if (literalDL > highestDL) { highestDL = literalDL; } @@ -257,10 +260,6 @@ private int computeLBD(int[] literals) { return occurringDecisionLevels.size(); } - public ResolutionSequence obtainResolutionSequence() { - throw new NotImplementedException("Method not yet implemented."); - } - /** * Compute the backjumping decision level, i.e., the decision level on which the learned NoGood is assigning (NoGood is unit and propagates). * This usually is the second highest decision level occurring in the learned NoGood, but due to assignments of MBT no such decision level may exist. diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/AntecedentTest.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/AntecedentTest.java new file mode 100644 index 000000000..0dce2db91 --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/AntecedentTest.java @@ -0,0 +1,32 @@ +package at.ac.tuwien.kr.alpha.solver; + +import java.util.HashSet; + +public class AntecedentTest { + + /** + * Tests whether two Antecedent objects have the same reason literals (irrespective of their order). + * Note that both Antecedents are assumed to contain no duplicate literals. + * @param l left Antecedent. + * @param r right Antecedent + * @return true iff both Antecedents contain the same literals. + */ + public static boolean antecedentsEquals(Antecedent l, Antecedent r) { + if (l == r) { + return true; + } + if (l != null && r != null && l.getReasonLiterals().length == r.getReasonLiterals().length) { + HashSet lSet = new HashSet<>(); + for (int literal : l.getReasonLiterals()) { + lSet.add(literal); + } + for (int literal : r.getReasonLiterals()) { + if (!lSet.contains(literal)) { + return false; + } + } + return true; + } + return false; + } +} \ No newline at end of file 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 a167aa8c8..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 @@ -8,7 +8,7 @@ import static at.ac.tuwien.kr.alpha.common.NoGood.fact; import static at.ac.tuwien.kr.alpha.common.NoGood.headFirst; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; -import static at.ac.tuwien.kr.alpha.solver.Antecedent.antecedentsEquals; +import static at.ac.tuwien.kr.alpha.solver.AntecedentTest.antecedentsEquals; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.*; import static org.junit.Assert.*; 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 730033978..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 @@ -8,7 +8,7 @@ import static at.ac.tuwien.kr.alpha.common.NoGood.fact; import static at.ac.tuwien.kr.alpha.common.NoGood.headFirst; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; -import static at.ac.tuwien.kr.alpha.solver.Antecedent.antecedentsEquals; +import static at.ac.tuwien.kr.alpha.solver.AntecedentTest.antecedentsEquals; import static at.ac.tuwien.kr.alpha.solver.ThriceTruth.*; import static org.junit.Assert.*; 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 22584eaa7..ac87dcaac 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 @@ -9,7 +9,7 @@ import org.junit.Test; import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; -import static at.ac.tuwien.kr.alpha.solver.Antecedent.antecedentsEquals; +import static at.ac.tuwien.kr.alpha.solver.AntecedentTest.antecedentsEquals; import static org.junit.Assert.*; /** From 932c7af99c7db283cdce128b9d04737abc72db24 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 17 Sep 2019 01:23:22 +0200 Subject: [PATCH 27/36] Apply suggestions from code review Co-Authored-By: Richard Taupe --- .../learning/GroundConflictNoGoodLearner.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index 9f48b13b7..35d6f22dd 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -147,7 +147,7 @@ private int backjumpLevelRemovingConflict(Antecedent violatedNoGood) { return highestDL - 1; } - private String printReasons(Collection reasons) { + private String reasonsToString(Collection reasons) { StringBuilder sb = new StringBuilder("{"); for (int reasonLiteral : reasons) { sb.append(isPositive(reasonLiteral) ? "+" + atomOf(reasonLiteral) : "-" + atomOf(reasonLiteral)); @@ -159,8 +159,8 @@ private String printReasons(Collection reasons) { return sb.toString(); } - private String printReasons(int[] reasons) { - return printReasons(IntStream.of(reasons != null ? reasons : new int[0]).boxed().collect(Collectors.toList())); + private String reasonsToString(int[] reasons) { + return reasonsToString(IntStream.of(reasons != null ? reasons : new int[0]).boxed().collect(Collectors.toList())); } private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { @@ -169,11 +169,11 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { return ConflictAnalysisResult.UNSAT; } int numLiteralsInConflictLevel = 0; - ArrayList resolutionLiterals = new ArrayList<>(); - ArrayList resolutionAtoms = new ArrayList<>(); + List resolutionLiterals = new ArrayList<>(); + List resolutionAtoms = new ArrayList<>(); int currentDecisionLevel = assignment.getDecisionLevel(); - HashSet seenAtoms = new HashSet<>(); // NOTE: other solvers use a global array for seen atoms, this might be slightly faster (initial tests with local arrays showed no significant improvement). - HashSet processedAtoms = new HashSet<>(); // Since trail contains 2 entries for MBT->TRUE assigned atoms, explicitly record which seen atoms have ben processed to avoid processing seen atoms twice. + Set seenAtoms = new HashSet<>(); // NOTE: other solvers use a global array for seen atoms, this might be slightly faster (initial tests with local arrays showed no significant improvement). + Set processedAtoms = new HashSet<>(); // Since trail contains 2 entries for MBT->TRUE assigned atoms, explicitly record which seen atoms have ben processed to avoid processing seen atoms twice. int[] currentConflictReason = conflictReason.getReasonLiterals(); int backjumpLevel = -1; conflictReason.bumpActivity(); From 7e3609102dd1023cf86651853dcd5cf2f32630af Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 17 Sep 2019 01:29:41 +0200 Subject: [PATCH 28/36] Fix broken build. --- .../solver/learning/GroundConflictNoGoodLearner.java | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index 35d6f22dd..a84b9667b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -34,10 +34,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.ArrayList; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; +import java.util.*; import java.util.stream.Collectors; import java.util.stream.IntStream; @@ -180,13 +177,13 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { TrailAssignment.TrailBackwardsWalker trailWalker = ((TrailAssignment)assignment).getTrailBackwardsWalker(); if (LOGGER.isTraceEnabled()) { LOGGER.trace("Current trail is: {}", trailWalker); - LOGGER.trace("Violated nogood is: {}", printReasons(conflictReason.getReasonLiterals())); + LOGGER.trace("Violated nogood is: {}", reasonsToString(conflictReason.getReasonLiterals())); } int nextAtom = -1; do { // Add current conflict reasons; only add those of lower decision levels, since from current one, only the 1UIP literal will be added. if (LOGGER.isTraceEnabled()) { - LOGGER.trace("Atom {} implied by {}, resolving with that nogood", nextAtom, printReasons(currentConflictReason)); + LOGGER.trace("Atom {} implied by {}, resolving with that nogood", nextAtom, reasonsToString(currentConflictReason)); } for (int literal : currentConflictReason) { // Seen atoms have already been dealt with. @@ -207,7 +204,7 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { if (LOGGER.isTraceEnabled()) { LOGGER.trace("LiteralsInConflictLevel now: {}", numLiteralsInConflictLevel); LOGGER.trace("Seen atoms are {}.", seenAtoms); - LOGGER.trace("Intermediate learned literals: {}", printReasons(resolutionLiterals)); + LOGGER.trace("Intermediate learned literals: {}", reasonsToString(resolutionLiterals)); } // Find next literal, i.e. first from top of trail that has been seen but is not yet processed. do { From 1e39446ae6731494526d7e2c5eb73b0a0d1a8b0d Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Tue, 17 Sep 2019 09:37:27 +0200 Subject: [PATCH 29/36] Fix merge. --- src/main/java/at/ac/tuwien/kr/alpha/Alpha.java | 2 ++ .../at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java index 33f2270ed..0464dab18 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java @@ -36,6 +36,8 @@ import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.Solver; import at.ac.tuwien.kr.alpha.solver.SolverFactory; +import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration; +import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfigurationBuilder; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.apache.commons.lang3.StringUtils; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index 6824b0452..be33e327d 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -70,7 +70,7 @@ public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropaga private boolean didPropagate; private boolean hasBinaryNoGoods; - NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) { + public NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) { this.assignment = assignment; this.checksEnabled = checksEnabled; this.learnedNoGoodDeletion = new LearnedNoGoodDeletion(this, assignment); From fb573fb97576a97e193339644d467e46cc43c966 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Tue, 17 Sep 2019 09:56:08 +0200 Subject: [PATCH 30/36] Fix merge bc193799e260ebe567f7227794d02626cf4425ac --- src/main/java/at/ac/tuwien/kr/alpha/Alpha.java | 8 -------- .../java/at/ac/tuwien/kr/alpha/solver/SolverFactory.java | 1 + 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java index 0464dab18..4dcb2e2a1 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/Alpha.java @@ -36,8 +36,6 @@ import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; import at.ac.tuwien.kr.alpha.solver.Solver; import at.ac.tuwien.kr.alpha.solver.SolverFactory; -import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfiguration; -import at.ac.tuwien.kr.alpha.solver.heuristics.HeuristicsConfigurationBuilder; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.apache.commons.lang3.StringUtils; @@ -104,12 +102,6 @@ public Program readProgramString(String aspString, Map filter) { String grounderName = this.config.getGrounderName(); boolean doDebugChecks = this.config.isDebugInternalChecks(); - boolean disableJustificationSearch = this.config.isDisableJustificationSearch(); - - HeuristicsConfigurationBuilder heuristicsConfigurationBuilder = HeuristicsConfiguration.builder(); - heuristicsConfigurationBuilder.setHeuristic(this.config.getBranchingHeuristic()); - heuristicsConfigurationBuilder.setMomsStrategy(this.config.getMomsStrategy()); - heuristicsConfigurationBuilder.setReplayChoices(this.config.getReplayChoices()); AtomStore atomStore = new AtomStoreImpl(); Grounder grounder = GrounderFactory.getInstance(grounderName, program, atomStore, filter, doDebugChecks); 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 195dee66e..36bbe668d 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 @@ -70,6 +70,7 @@ private static HeuristicsConfiguration buildHeuristicsConfiguration(SystemConfig HeuristicsConfigurationBuilder heuristicsConfigurationBuilder = HeuristicsConfiguration.builder(); heuristicsConfigurationBuilder.setHeuristic(config.getBranchingHeuristic()); heuristicsConfigurationBuilder.setMomsStrategy(config.getMomsStrategy()); + heuristicsConfigurationBuilder.setReplayChoices(config.getReplayChoices()); return heuristicsConfigurationBuilder.build(); } } From 2306c45fdd4d6b3817a33148ce65491f77ed7c2a Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sun, 22 Sep 2019 00:08:17 +0200 Subject: [PATCH 31/36] Fix bug in GroundConflictNoGoodLearner, improve debug helpers/printing. - ReplayHeuristic can use 0 in replay list to signal no more choices. - GroundConflictNoGoodLearner knows AtomStore for trace printing, atoms assigned T at conflict dl but MBT lower are correctly handled. - Improved debug printing in NoGoodStoreAlphaRoaming and WatchedNoGood. - Adapted GroundConflictNoGoodLearnerTest for AtomStore presence. --- .../at/ac/tuwien/kr/alpha/common/Literals.java | 4 ++++ .../ac/tuwien/kr/alpha/solver/DefaultSolver.java | 2 +- .../kr/alpha/solver/NoGoodStoreAlphaRoaming.java | 5 +++++ .../ac/tuwien/kr/alpha/solver/WatchedNoGood.java | 6 ++---- .../alpha/solver/heuristics/ReplayHeuristic.java | 4 ++++ .../learning/GroundConflictNoGoodLearner.java | 15 ++++++++++----- .../learning/GroundConflictNoGoodLearnerTest.java | 5 +++-- 7 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java b/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java index 947c4c384..8c703a54b 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java @@ -76,4 +76,8 @@ public static int atomToNegatedLiteral(int atom) { public static int positiveLiteral(int literal) { return literal & ~0x1; } + + public static String literalToString(int literal) { + return (isPositive(literal) ? "+" : "-") + atomOf(literal); + } } 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 173269881..88ccb386d 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 @@ -85,7 +85,7 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.assignment = assignment; this.store = store; this.choiceManager = new ChoiceManager(assignment, store); - this.learner = new GroundConflictNoGoodLearner(assignment); + this.learner = new GroundConflictNoGoodLearner(assignment, atomStore); this.branchingHeuristic = chainFallbackHeuristic(grounder, assignment, random, heuristicsConfiguration); this.disableJustifications = config.isDisableJustificationSearch(); this.disableNoGoodDeletion = config.isDisableNoGoodDeletion(); diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index be33e327d..1dfa8976e 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -761,6 +761,11 @@ public void bumpActivity() { @Override public void decreaseActivity() { } + + @Override + public String toString() { + return "{" + literalToString(literals[0]) + ", " + literalToString(literals[1]) + "}"; + } } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java index ca7b63dab..74fa5352a 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/WatchedNoGood.java @@ -6,8 +6,7 @@ import java.util.Iterator; 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.isPositive; +import static at.ac.tuwien.kr.alpha.common.Literals.*; public final class WatchedNoGood implements NoGoodInterface, Antecedent, Iterable { private int activity; @@ -139,8 +138,7 @@ public String toString() { int hcount = 0; for (int literal : literals) { - sb.append(isPositive(literal) ? "+" : "-"); - sb.append(atomOf(literal)); + sb.append(literalToString(literal)); sb.append(hasHead() && head == hcount ? "h" : ""); sb.append(" "); hcount++; diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java index 1fd453ce0..6268f900c 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java @@ -70,6 +70,10 @@ public int chooseLiteral() { return DEFAULT_CHOICE_LITERAL; } int replayChoiceSignedAtom = choicesIterator.next(); + if (replayChoiceSignedAtom == 0 ) { + // Use 0 to signal no more choices. + return DEFAULT_CHOICE_LITERAL; + } int replayChoiceAtom = Math.abs(replayChoiceSignedAtom); int replayChoiceLiteral = Literals.atomToLiteral(replayChoiceAtom, replayChoiceSignedAtom > 0); if (!choiceManager.isActiveChoiceAtom(replayChoiceAtom)) { diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java index a84b9667b..1d4b38bb5 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java @@ -28,6 +28,7 @@ package at.ac.tuwien.kr.alpha.solver.learning; import at.ac.tuwien.kr.alpha.common.Assignment; +import at.ac.tuwien.kr.alpha.common.AtomStore; import at.ac.tuwien.kr.alpha.common.NoGood; import at.ac.tuwien.kr.alpha.solver.Antecedent; import at.ac.tuwien.kr.alpha.solver.TrailAssignment; @@ -50,6 +51,7 @@ public class GroundConflictNoGoodLearner { private static final Logger LOGGER = LoggerFactory.getLogger(GroundConflictNoGoodLearner.class); private final Assignment assignment; + private final AtomStore atomStore; public int computeConflictFreeBackjumpingLevel(NoGood violatedNoGood) { int highestDecisionLevel = -1; @@ -113,8 +115,9 @@ public String toString() { } } - public GroundConflictNoGoodLearner(Assignment assignment) { + public GroundConflictNoGoodLearner(Assignment assignment, AtomStore atomStore) { this.assignment = assignment; + this.atomStore = atomStore; } public ConflictAnalysisResult analyzeConflictingNoGood(Antecedent violatedNoGood) { @@ -163,6 +166,7 @@ private String reasonsToString(int[] reasons) { private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { LOGGER.trace("Analyzing trail based."); if (assignment.getDecisionLevel() == 0) { + LOGGER.trace("Conflict on decision level 0."); return ConflictAnalysisResult.UNSAT; } int numLiteralsInConflictLevel = 0; @@ -206,15 +210,14 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { LOGGER.trace("Seen atoms are {}.", seenAtoms); LOGGER.trace("Intermediate learned literals: {}", reasonsToString(resolutionLiterals)); } - // Find next literal, i.e. first from top of trail that has been seen but is not yet processed. + // Find next literal, i.e. first from top of trail that has been seen but is not yet processed, also skip atoms whose TRUE assignment is on current level but their MBT/weak assignment is lower. do { int nextLiteral = trailWalker.getNextLowerLiteral(); nextAtom = atomOf(nextLiteral); if (LOGGER.isTraceEnabled()) { LOGGER.trace("Next literal on trail is: {}", isPositive(nextLiteral) ? "+" + nextAtom : "-" + nextAtom); } - - } while (!(seenAtoms.contains(nextAtom) && !processedAtoms.contains(nextAtom))); + } while (assignment.getWeakDecisionLevel(nextAtom) != currentDecisionLevel || !seenAtoms.contains(nextAtom) || processedAtoms.contains(nextAtom)); Antecedent impliedBy = assignment.getImpliedBy(nextAtom); if (impliedBy != null) { currentConflictReason = impliedBy.getReasonLiterals(); @@ -232,7 +235,9 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) { } NoGood learnedNoGood = NoGood.learnt(learnedLiterals); - LOGGER.trace("Learned NoGood is: {}", learnedNoGood); + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Learned NoGood is: {}", atomStore.noGoodToString(learnedNoGood)); + } int backjumpingDecisionLevel = computeBackjumpingDecisionLevel(learnedNoGood); if (backjumpingDecisionLevel < 0) { 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 ac87dcaac..668d66bc4 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 @@ -19,6 +19,7 @@ public class GroundConflictNoGoodLearnerTest { private final WritableAssignment assignment; private final NoGoodStore store; + AtomStore atomStore; public GroundConflictNoGoodLearnerTest() { AtomStore atomStore = new AtomStoreImpl(); @@ -31,7 +32,7 @@ public GroundConflictNoGoodLearnerTest() { @Test public void smallConflictNonTrivial1UIP() { - GroundConflictNoGoodLearner learner = new GroundConflictNoGoodLearner(assignment); + GroundConflictNoGoodLearner learner = new GroundConflictNoGoodLearner(assignment, atomStore); NoGood n1 = new NoGood(fromOldLiterals(2, -8, 1)); NoGood n2 = new NoGood(fromOldLiterals(-1, -7)); @@ -70,7 +71,7 @@ public void smallConflictNonTrivial1UIP() { @Ignore // TrailAssignment no longer propagates at lower decision level. @Test public void subCurrentDLPropagationWithChoiceCauseOfConflict() { - GroundConflictNoGoodLearner learner = new GroundConflictNoGoodLearner(assignment); + GroundConflictNoGoodLearner learner = new GroundConflictNoGoodLearner(assignment, atomStore); NoGood n1 = new NoGood(fromOldLiterals(1, -2)); NoGood n2 = new NoGood(fromOldLiterals(2, 3)); store.add(10, n1); From 20779725350120f166a5fa7ef26deaf55b89158a Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Sun, 22 Sep 2019 01:30:15 +0200 Subject: [PATCH 32/36] Satisfy checkstyle. --- .../ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java index 6268f900c..cda9f35ac 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/heuristics/ReplayHeuristic.java @@ -70,7 +70,7 @@ public int chooseLiteral() { return DEFAULT_CHOICE_LITERAL; } int replayChoiceSignedAtom = choicesIterator.next(); - if (replayChoiceSignedAtom == 0 ) { + if (replayChoiceSignedAtom == 0) { // Use 0 to signal no more choices. return DEFAULT_CHOICE_LITERAL; } From c9a4ea5dd53e1e0d5e40aaa089795406181bd472 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Mon, 23 Sep 2019 09:13:46 +0200 Subject: [PATCH 33/36] Adding unit tests for LearnedNoGoodDeletion. --- .../alpha/solver/LearnedNoGoodDeletion.java | 24 +++++-- .../alpha/solver/NoGoodStoreAlphaRoaming.java | 5 ++ .../solver/LearnedNoGoodDeletionTest.java | 69 +++++++++++++++++++ 3 files changed, 93 insertions(+), 5 deletions(-) create mode 100644 src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java 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 829f866ee..e3de0cd21 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 @@ -4,8 +4,7 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.ArrayList; -import java.util.Iterator; +import java.util.*; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; @@ -16,9 +15,9 @@ */ class LearnedNoGoodDeletion { private static final Logger LOGGER = LoggerFactory.getLogger(LearnedNoGoodDeletion.class); - private static final int RESET_SEQUENCE_AFTER = 20; - private static final int RUN_AFTER_AT_LEAST = 2000; - private static final int GROWTH_FACTOR = 100; + public static final int RESET_SEQUENCE_AFTER = 20; + public static final int RUN_AFTER_AT_LEAST = 2000; + public static final int GROWTH_FACTOR = 100; private final ArrayList learnedNoGoods = new ArrayList<>(); // List of learned NoGoods that can be removed again. Note: should only contain NoGoods of size > 2. private final NoGoodStoreAlphaRoaming store; private final Assignment assignment; @@ -30,6 +29,21 @@ class LearnedNoGoodDeletion { this.assignment = assignment; } + void reset() { + learnedNoGoods.clear(); + conflictCounter = 0; + cleanupCounter = 0; + } + + /** + * Returns WatchedNoGoods known to {@link LearnedNoGoodDeletion}. + * Note: this is likely just a subset of all learned nogoods. + * @return an unmodifiable list of {@link WatchedNoGood}s. + */ + public List inspectLearnedNoGoods() { + return Collections.unmodifiableList(learnedNoGoods); + } + void recordLearnedNoGood(WatchedNoGood learnedWatchedNoGood) { learnedNoGoods.add(learnedWatchedNoGood); } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java index 1dfa8976e..95e4e0aef 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/NoGoodStoreAlphaRoaming.java @@ -83,12 +83,17 @@ public NoGoodStoreAlphaRoaming(WritableAssignment assignment) { @SuppressWarnings("unchecked") void clear() { assignment.clear(); + learnedNoGoodDeletion.reset(); binaryWatches = new BinaryWatchList[0]; watches = new ArrayList[0]; watchesAlpha = new ArrayList[0]; maxAtomId = 0; } + public LearnedNoGoodDeletion getLearnedNoGoodDeletion() { + return learnedNoGoodDeletion; + } + @Override public void backtrack() { didPropagate = false; 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 new file mode 100644 index 000000000..45e65b76d --- /dev/null +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/LearnedNoGoodDeletionTest.java @@ -0,0 +1,69 @@ +package at.ac.tuwien.kr.alpha.solver; + +import at.ac.tuwien.kr.alpha.common.*; +import org.junit.Before; +import org.junit.Test; + +import java.util.List; + +import static at.ac.tuwien.kr.alpha.common.NoGoodTest.fromOldLiterals; +import static org.junit.Assert.*; + +public class LearnedNoGoodDeletionTest { + + private NoGoodStoreAlphaRoaming store; + private LearnedNoGoodDeletion learnedNoGoodDeletion; + + public LearnedNoGoodDeletionTest() { + AtomStore atomStore = new AtomStoreImpl(); + AtomStoreTest.fillAtomStore(atomStore, 200); + WritableAssignment assignment = new TrailAssignment(atomStore); + assignment.growForMaxAtomId(); + store = new NoGoodStoreAlphaRoaming(assignment); + learnedNoGoodDeletion = store.getLearnedNoGoodDeletion(); + } + + @Before + public void setUp() { + store.clear(); + store.growForMaxAtomId(fromOldLiterals(200)); + assertNull(store.add(1, new NoGood(fromOldLiterals(1, -2)))); + assertNull(store.add(2, new NoGood(fromOldLiterals(2, -3)))); + assertNull(store.add(3, new NoGood(fromOldLiterals(2, -4, -5)))); + assertNull(store.add(4, new NoGood(fromOldLiterals(3, 4, 5)))); + assertNull(store.propagate()); + } + + @Test + public void testDeletionRunningAfterConflicts() { + for (int i = 0; i < LearnedNoGoodDeletion.RUN_AFTER_AT_LEAST; i++) { + learnedNoGoodDeletion.increaseConflictCounter(); + } + assertFalse(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + learnedNoGoodDeletion.increaseConflictCounter(); + assertTrue(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + learnedNoGoodDeletion.runNoGoodDeletion(); + assertFalse(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + } + + @Test + public void testDeletionRemovingWatches() { + for (int i = 0; i < LearnedNoGoodDeletion.RUN_AFTER_AT_LEAST; i++) { + learnedNoGoodDeletion.increaseConflictCounter(); + } + assertFalse(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + learnedNoGoodDeletion.increaseConflictCounter(); + assertTrue(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + assertNull(store.add(4, NoGood.learnt(fromOldLiterals(10, 11, 12)), 3)); + assertNull(store.add(5, NoGood.learnt(fromOldLiterals(10, -13, -14)), 4)); + List watchedNoGoods = learnedNoGoodDeletion.inspectLearnedNoGoods(); + assertTrue(watchedNoGoods.size() >= 2); + WatchedNoGood watchedNoGood = watchedNoGoods.get(0); + for (int i = 0; i < 10; i++) { + watchedNoGood.bumpActivity(); + } + learnedNoGoodDeletion.runNoGoodDeletion(); + watchedNoGoods = learnedNoGoodDeletion.inspectLearnedNoGoods(); + assertTrue(watchedNoGoods.size() < 2); + } +} \ No newline at end of file From 832137b8d0849dc80e1fa713f97659d0ed792c9f Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 25 Sep 2019 16:10:02 +0200 Subject: [PATCH 34/36] Fix member/local variable mixup. --- .../solver/learning/GroundConflictNoGoodLearnerTest.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 668d66bc4..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 @@ -13,16 +13,16 @@ import static org.junit.Assert.*; /** - * Copyright (c) 2016, the Alpha Team. + * Copyright (c) 2016-2019, the Alpha Team. */ public class GroundConflictNoGoodLearnerTest { private final WritableAssignment assignment; private final NoGoodStore store; - AtomStore atomStore; + private AtomStore atomStore; public GroundConflictNoGoodLearnerTest() { - AtomStore atomStore = new AtomStoreImpl(); + atomStore = new AtomStoreImpl(); AtomStoreTest.fillAtomStore(atomStore, 20); this.assignment = new TrailAssignment(atomStore); this.assignment.growForMaxAtomId(); From de00b53b965685b1e0fe484539e8de8ce1f20c20 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Fri, 27 Sep 2019 10:10:49 +0200 Subject: [PATCH 35/36] Include number of deleted nogoods in stats. --- .../tuwien/kr/alpha/solver/DefaultSolver.java | 8 ++++ .../alpha/solver/LearnedNoGoodDeletion.java | 12 ++++- .../solver/SolverMaintainingStatistics.java | 9 ++-- .../solver/LearnedNoGoodDeletionTest.java | 47 ++++++++++++++++++- .../alpha/solver/SolverStatisticsTests.java | 12 ++--- 5 files changed, 77 insertions(+), 11 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 88ccb386d..2ee2b11d4 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 @@ -546,6 +546,14 @@ public int getNumberOfConflictsAfterClosing() { return conflictsAfterClosing; } + @Override + public int getNumberOfDeletedNoGoods() { + if (!(store instanceof NoGoodStoreAlphaRoaming)) { + return 0; + } + return ((NoGoodStoreAlphaRoaming)store).getLearnedNoGoodDeletion().getNumberOfDeletedNoGoods(); + } + private void logStats() { if (LOGGER.isDebugEnabled()) { LOGGER.debug(getStatisticsString()); 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 e3de0cd21..a17264654 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 @@ -4,7 +4,10 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Iterator; +import java.util.List; import static at.ac.tuwien.kr.alpha.common.Literals.atomOf; @@ -23,6 +26,7 @@ class LearnedNoGoodDeletion { private final Assignment assignment; private int conflictCounter; private int cleanupCounter; + private int numberOfDeletedNoGoods; LearnedNoGoodDeletion(NoGoodStoreAlphaRoaming store, Assignment assignment) { this.store = store; @@ -33,6 +37,7 @@ void reset() { learnedNoGoods.clear(); conflictCounter = 0; cleanupCounter = 0; + numberOfDeletedNoGoods = 0; } /** @@ -92,6 +97,7 @@ void runNoGoodDeletion() { } } LOGGER.debug("Removed {} NoGoods from store.", deletedNoGoods); + this.numberOfDeletedNoGoods += deletedNoGoods; } private boolean isLocked(WatchedNoGood noGood, Assignment assignment) { @@ -103,4 +109,8 @@ private boolean isLocked(WatchedNoGood noGood, Assignment assignment) { return noGood == assignment.getImpliedBy(watchedAtom1) || noGood == assignment.getImpliedBy(watchedAtom2); } + + public int getNumberOfDeletedNoGoods() { + return numberOfDeletedNoGoods; + } } diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java index a6ee41473..861830582 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/SolverMaintainingStatistics.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017-2018 Siemens AG + * Copyright (c) 2017-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -38,6 +38,8 @@ public interface SolverMaintainingStatistics { int getNumberOfBackjumps(); int getNumberOfBacktracksDueToRemnantMBTs(); + + int getNumberOfDeletedNoGoods(); /** * @return the number of times the solver had to backtrack after closing unassigned atoms @@ -46,11 +48,12 @@ public interface SolverMaintainingStatistics { default String getStatisticsString() { return "g=" + getNumberOfChoices() + ", bt=" + getNumberOfBacktracks() + ", bj=" + getNumberOfBackjumps() + ", bt_within_bj=" - + getNumberOfBacktracksWithinBackjumps() + ", mbt=" + getNumberOfBacktracksDueToRemnantMBTs() + ", cac=" + getNumberOfConflictsAfterClosing(); + + getNumberOfBacktracksWithinBackjumps() + ", mbt=" + getNumberOfBacktracksDueToRemnantMBTs() + ", cac=" + getNumberOfConflictsAfterClosing() + + ", del_ng=" + getNumberOfDeletedNoGoods(); } default String getStatisticsCSV() { - return String.format("%d,%d,%d,%d,%d,%d", getNumberOfChoices(), getNumberOfBacktracks(), getNumberOfBackjumps(), getNumberOfBacktracksWithinBackjumps(), getNumberOfBacktracksDueToRemnantMBTs(), getNumberOfConflictsAfterClosing()); + return String.format("%d,%d,%d,%d,%d,%d,%d", getNumberOfChoices(), getNumberOfBacktracks(), getNumberOfBackjumps(), getNumberOfBacktracksWithinBackjumps(), getNumberOfBacktracksDueToRemnantMBTs(), getNumberOfConflictsAfterClosing(), getNumberOfDeletedNoGoods()); } default void printStatistics(PrintStream out) { 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 45e65b76d..1d9f4cbc5 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 @@ -1,6 +1,36 @@ +/** + * Copyright (c) 2019, 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; -import at.ac.tuwien.kr.alpha.common.*; +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.common.NoGood; import org.junit.Before; import org.junit.Test; @@ -66,4 +96,19 @@ public void testDeletionRemovingWatches() { watchedNoGoods = learnedNoGoodDeletion.inspectLearnedNoGoods(); assertTrue(watchedNoGoods.size() < 2); } + + @Test + public void testDeletionIncreasesDeletionCounter() { + for (int i = 0; i < LearnedNoGoodDeletion.RUN_AFTER_AT_LEAST; i++) { + learnedNoGoodDeletion.increaseConflictCounter(); + } + assertFalse(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + learnedNoGoodDeletion.increaseConflictCounter(); + assertTrue(learnedNoGoodDeletion.needToRunNoGoodDeletion()); + assertNull(store.add(4, NoGood.learnt(fromOldLiterals(10, 11, 12)), 3)); + assertNull(store.add(5, NoGood.learnt(fromOldLiterals(10, -13, -14)), 4)); + assertEquals(0, learnedNoGoodDeletion.getNumberOfDeletedNoGoods()); + learnedNoGoodDeletion.runNoGoodDeletion(); + assertTrue(learnedNoGoodDeletion.getNumberOfDeletedNoGoods() > 0); + } } \ No newline at end of file diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java index 664c7f6e9..a4c7999aa 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverStatisticsTests.java @@ -1,5 +1,5 @@ /** - * Copyright (c) 2017-2018 Siemens AG + * Copyright (c) 2017-2019 Siemens AG * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -37,24 +37,24 @@ public class SolverStatisticsTests extends AbstractSolverTests { @Test public void checkStatsStringZeroChoices() { Solver solver = getInstance("a."); - collectAnswerSetsAndCheckStats(solver, 1, 0, 0, 0, 0, 0, 0); + collectAnswerSetsAndCheckStats(solver, 1, 0, 0, 0, 0, 0, 0, 0); } @Test public void checkStatsStringOneChoice() { Solver solver = getInstance("a :- not b. b :- not a."); - collectAnswerSetsAndCheckStats(solver, 2, 1, 1, 1, 1, 0, 0); + collectAnswerSetsAndCheckStats(solver, 2, 1, 1, 1, 1, 0, 0, 0); } private void collectAnswerSetsAndCheckStats(Solver solver, int expectedNumberOfAnswerSets, int expectedNumberOfGuesses, int expectedTotalNumberOfBacktracks, - int expectedNumberOfBacktracksWithinBackjumps, int expectedNumberOfBackjumps, int expectedNumberOfMBTs, int expectedNumberOfConflictsAfterClosing) { + int expectedNumberOfBacktracksWithinBackjumps, int expectedNumberOfBackjumps, int expectedNumberOfMBTs, int expectedNumberOfConflictsAfterClosing, int expectedNumberOfDeletedNoGoods) { Set answerSets = solver.collectSet(); assertEquals(expectedNumberOfAnswerSets, answerSets.size()); if (solver instanceof SolverMaintainingStatistics) { SolverMaintainingStatistics solverMaintainingStatistics = (SolverMaintainingStatistics) solver; assertEquals( - String.format("g=%d, bt=%d, bj=%d, bt_within_bj=%d, mbt=%d, cac=%d", expectedNumberOfGuesses, expectedTotalNumberOfBacktracks, expectedNumberOfBackjumps, - expectedNumberOfBacktracksWithinBackjumps, expectedNumberOfMBTs, expectedNumberOfConflictsAfterClosing), + String.format("g=%d, bt=%d, bj=%d, bt_within_bj=%d, mbt=%d, cac=%d, del_ng=%d", expectedNumberOfGuesses, expectedTotalNumberOfBacktracks, expectedNumberOfBackjumps, + expectedNumberOfBacktracksWithinBackjumps, expectedNumberOfMBTs, expectedNumberOfConflictsAfterClosing, expectedNumberOfDeletedNoGoods), solverMaintainingStatistics.getStatisticsString()); } } From 1e72a79536e41246fa3fdf2901e5a25af3918788 Mon Sep 17 00:00:00 2001 From: Richard Taupe Date: Mon, 30 Sep 2019 13:33:45 +0200 Subject: [PATCH 36/36] Add reference to ICLP 2019 paper --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index f1dc09b24..0a5028bd1 100644 --- a/README.md +++ b/README.md @@ -81,6 +81,7 @@ run into trouble feel free to file an issue. Peer-reviewed publications part of journals, conferences and workshops: + * [Exploiting Partial Knowledge in Declarative Domain-Specific Heuristics for ASP](https://doi.org/10.4204/EPTCS.306.9) ([supplementary material](https://git-ainf.aau.at/DynaCon/website/tree/master/supplementary_material/2019_ICLP_Domain-Specific_Heuristics)) * [Degrees of Laziness in Grounding: Effects of Lazy-Grounding Strategies on ASP Solving](https://doi.org/10.1007/978-3-030-20528-7_22) ([preprint](https://arxiv.org/abs/1903.12510) | [supplementary material](https://git-ainf.aau.at/DynaCon/website/tree/master/supplementary_material/2019_LPNMR_Degrees_of_Laziness)) * [Exploiting Justifications for Lazy Grounding of Answer Set Programs](https://doi.org/10.24963/ijcai.2018/240) * [Lazy Grounding for Dynamic Configuration: Efficient Large-Scale (Re)Configuration of Cyber-Physical Systems with ASP](https://doi.org/10.1007/s13218-018-0536-x)