Merge pull request #250 from alpha-asp/fix_239

Fix issue #239
alpha-asp · May 7, 2020 · d5fbdf4 · d5fbdf4
2 parents 220b58b + 6104a49
commit d5fbdf4
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 4 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
@@ -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
@@ -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
@@ -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> answerSet = solver.stream().findFirst();
+		assertTrue(answerSet.isPresent());
+	}
+
 
 	@Test
 	public void dummyGrounder() {