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..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 @@ -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.isUnary()) { + 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; 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() {