diff --git a/src/main/java/at/ac/tuwien/kr/alpha/solver/ArrayAssignment.java b/src/main/java/at/ac/tuwien/kr/alpha/solver/ArrayAssignment.java index 74eb5bf13..eea375cf0 100644 --- a/src/main/java/at/ac/tuwien/kr/alpha/solver/ArrayAssignment.java +++ b/src/main/java/at/ac/tuwien/kr/alpha/solver/ArrayAssignment.java @@ -225,7 +225,7 @@ private ConflictCause assignWithDecisionLevel(int atom, ThriceTruth value, NoGoo // Check consistency. if (!assignmentsConsistent(current, value)) { - ConflictCause conflictCause = null; + ConflictCause conflictCause = new ConflictCause(impliedBy); // Assignments are inconsistent, prepare the reason. NoGood violated = impliedBy; if (decisionLevel < current.getWeakDecisionLevel()) { @@ -233,6 +233,8 @@ private ConflictCause assignWithDecisionLevel(int atom, ThriceTruth value, NoGoo violated = current.getPrevious() == null ? current.getImpliedBy() : current.getPrevious().getImpliedBy(); // take MBT reason if it exists. if (violated == null) { conflictCause = new ConflictCause(current); + } else { + conflictCause = new ConflictCause(violated); } // The lower assignment takes precedence over the current value, overwrite it and adjust mbtCounter. if (current.getTruth() == MBT) { @@ -244,7 +246,6 @@ private ConflictCause assignWithDecisionLevel(int atom, ThriceTruth value, NoGoo } } - conflictCause = new ConflictCause(impliedBy); return conflictCause; } 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 46ee2b2e8..948e8acdb 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 @@ -862,4 +862,30 @@ public void noPositiveCycleSelfFoundingGuess() throws IOException { Set answerSets = solver.collectSet(); assertTrue(answerSets.isEmpty()); } + + @Test + public void conflictFromUnaryNoGood() throws IOException { + String program = + "d(b).\n" + + "sel(X) :- not nsel(X), d(X).\n" + + "nsel(X) :- not sel(X), d(X).\n" + + "t(a) :- sel(b).\n" + + ":- t(X).\n"; + + ParsedProgram parsedProgram = parseVisit(program); + NaiveGrounder grounder = new NaiveGrounder(parsedProgram); + Solver solver = getInstance(grounder); + + Set expected = new HashSet<>(Collections.singletonList( + new BasicAnswerSet.Builder() + .predicate("d") + .instance("b") + .predicate("nsel") + .instance("b") + .build() + )); + + Set answerSets = solver.collectSet(); + assertEquals(expected, answerSets); + } }