From 599d433a687ba3b2bd80b6e05484c8b5f31a16f1 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 May 2020 04:00:40 +0200 Subject: [PATCH 1/3] Fix bug in computation of backjumping level for violated unary nogoods in GroundConflictNoGoodLearner and related issue with erroneous storage of conflicting out-of-order assignments in TrailAssignment. --- .../kr/alpha/solver/TrailAssignment.java | 5 +++-- .../learning/GroundConflictNoGoodLearner.java | 19 +++++++++++++++++++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/TrailAssignment.java index ee456f154..ac767ff92 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 @@ -317,13 +317,14 @@ public ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy) { @Override public ConflictCause assign(int atom, ThriceTruth value, Antecedent impliedBy, int decisionLevel) { - if (decisionLevel < getDecisionLevel()) { + ConflictCause conflictCause = assign(atom, value, impliedBy); + if (conflictCause == null && decisionLevel < getDecisionLevel()) { outOfOrderLiterals.add(new OutOfOrderLiteral(atom, value, decisionLevel, impliedBy)); if (highestDecisionLevelContainingOutOfOrderLiterals < getDecisionLevel()) { highestDecisionLevelContainingOutOfOrderLiterals = getDecisionLevel(); } } - return assign(atom, value, impliedBy); + return conflictCause; } private boolean assignmentsConsistent(ThriceTruth oldTruth, ThriceTruth value) { 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 00a822541..97f0eccd1 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 @@ -54,7 +54,26 @@ public class GroundConflictNoGoodLearner { private final Assignment assignment; private final AtomStore atomStore; + /** + * Given a conflicting NoGood, computes a conflict-free backjumping level such that the given NoGood is not + * violated. + * + * @param violatedNoGood the conflicting NoGood. + * @return -1 if the violatedNoGood cannot be satisfied, otherwise + * 0 if violatedNoGood is unary, and else + * the highest backjumping level such that the NoGood is no longer violated. + */ public int computeConflictFreeBackjumpingLevel(NoGood violatedNoGood) { + // If violatedNoGood is unary, backjump to decision level 0 if it can be satisfied. + if (violatedNoGood.size() == 1) { + int literal = violatedNoGood.getLiteral(0); + int literalDecisionLevel = assignment.getRealWeakDecisionLevel(atomOf(literal)); + if (literalDecisionLevel > 0) { + return 0; + } else { + return -1; + } + } int highestDecisionLevel = -1; int secondHighestDecisionLevel = -1; int numAtomsInHighestLevel = 0; From 78433905ff349c8a67e61a4a18a1a8a3cb4ad777 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 May 2020 05:20:34 +0200 Subject: [PATCH 2/3] Add unit test. --- .../tuwien/kr/alpha/solver/SolverTests.java | 45 ++++++++++++++++++- 1 file changed, 43 insertions(+), 2 deletions(-) diff --git a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverTests.java b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverTests.java index 81f46d834..82cfd0152 100644 --- a/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverTests.java +++ b/src/test/java/at/ac/tuwien/kr/alpha/solver/SolverTests.java @@ -28,18 +28,36 @@ package at.ac.tuwien.kr.alpha.solver; import at.ac.tuwien.kr.alpha.AnswerSetsParser; -import at.ac.tuwien.kr.alpha.common.*; +import at.ac.tuwien.kr.alpha.common.AnswerSet; +import at.ac.tuwien.kr.alpha.common.AnswerSetBuilder; +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.atoms.Atom; import at.ac.tuwien.kr.alpha.common.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.common.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.config.SystemConfig; import at.ac.tuwien.kr.alpha.grounder.ChoiceGrounder; import at.ac.tuwien.kr.alpha.grounder.DummyGrounder; +import at.ac.tuwien.kr.alpha.grounder.Grounder; +import at.ac.tuwien.kr.alpha.grounder.GrounderFactory; import at.ac.tuwien.kr.alpha.grounder.parser.InlineDirectives; +import at.ac.tuwien.kr.alpha.grounder.parser.ProgramParser; +import at.ac.tuwien.kr.alpha.solver.heuristics.BranchingHeuristicFactory; import junit.framework.TestCase; +import org.antlr.v4.runtime.CharStreams; import org.junit.Test; import java.io.IOException; -import java.util.*; +import java.nio.file.Paths; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.SortedSet; import static java.util.Collections.singleton; import static org.junit.Assert.assertEquals; @@ -723,6 +741,29 @@ public void smallCardinalityAggregate() throws IOException { ); } + @Test + public void testLearnedUnaryNoGoodCausingOutOfOrderLiteralsConflict() throws IOException { + final ProgramParser parser = new ProgramParser(); + 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", "simple.asp")))); + AtomStore atomStore = new AtomStoreImpl(); + Grounder grounder = GrounderFactory.getInstance("naive", parsedProgram, atomStore, true); + SystemConfig config = new SystemConfig(); + config.setSolverName("default"); + config.setNogoodStoreName("alpharoaming"); + config.setSeed(0); + config.setBranchingHeuristic(BranchingHeuristicFactory.Heuristic.valueOf("VSIDS")); + config.setDebugInternalChecks(true); + config.setDisableJustificationSearch(false); + config.setReplayChoices(Arrays.asList(21, 26, 36, 56, 91, 96, 285, 166, 101, 290, 106, 451, 445, 439, 448, + 433, 427, 442, 421, 415, 436, 409, 430, 397, 391, 424, 385, 379, + 418, 373, 412, 406, 394, 388, 382, 245, 232, 208 + )); + Solver solver = SolverFactory.getInstance(config, atomStore, grounder); + Optional answerSet = solver.stream().findFirst(); + assertTrue(answerSet.isPresent()); + } + @Test public void dummyGrounder() { From 6104a491a90b05862246bd72da5167c795b955a0 Mon Sep 17 00:00:00 2001 From: Antonius Weinzierl Date: Wed, 6 May 2020 16:17:10 +0200 Subject: [PATCH 3/3] Update src/main/java/at/ac/tuwien/kr/alpha/solver/learning/GroundConflictNoGoodLearner.java Co-authored-by: Richard Taupe --- .../kr/alpha/solver/learning/GroundConflictNoGoodLearner.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 97f0eccd1..d5b26f9bf 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 @@ -65,7 +65,7 @@ public class GroundConflictNoGoodLearner { */ public int computeConflictFreeBackjumpingLevel(NoGood violatedNoGood) { // If violatedNoGood is unary, backjump to decision level 0 if it can be satisfied. - if (violatedNoGood.size() == 1) { + if (violatedNoGood.isUnary()) { int literal = violatedNoGood.getLiteral(0); int literalDecisionLevel = assignment.getRealWeakDecisionLevel(atomOf(literal)); if (literalDecisionLevel > 0) {