Issue #81: Unsatisfiable cores with complementary literals.

* Ensure that LogicProgram::extractCore() only unmarks seen literals instead of their variables so that it also correctly handles cores containing complementary literals.
potassco · Jun 24, 2022 · b0b2e0c · b0b2e0c
1 parent 51b73cc
commit b0b2e0c
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 3 deletions.
diff --git a/clasp/logic_program.h b/clasp/logic_program.h
@@ -438,7 +438,7 @@ class LogicProgram : public ProgramBuilder {
 	/*!
 	 * \param solverCore An unsat core found when solving under ProgramBuilder::getAssumptions().
 	 * \param prgLits The given unsat core expressed in terms of program literals.
-	 * \return Whether or not unsatCore was successfully mapped.
+	 * \return Whether unsatCore was successfully mapped.
 	 */
 	bool extractCore(const LitVec& unsatCore, Potassco::LitVec& prgLits) const;
 

diff --git a/clasp/shared_context.h b/clasp/shared_context.h
@@ -796,6 +796,7 @@ class SharedContext {
 	void    setVarEq(Var v, bool b) { set(v, VarInfo::Eq, b); }
 	void    set(Var v, VarInfo::Flag f, bool b) { if (b != varInfo(v).has(f)) varInfo_[v].toggle(f); }
 	void    mark(Literal p)         { assert(validVar(p.var())); varInfo_[p.var()].rep |= (VarInfo::Mark_p + p.sign()); }
+	void    unmark(Literal p)       { assert(validVar(p.var())); varInfo_[p.var()].rep &= ~(VarInfo::Mark_p + p.sign()); }
 	void    unmark(Var v)           { assert(validVar(v)); varInfo_[v].rep &= ~(VarInfo::Mark_p|VarInfo::Mark_n); }
 	//! Eliminates the variable v from the problem.
 	/*!

diff --git a/src/logic_program.cpp b/src/logic_program.cpp
@@ -849,14 +849,14 @@ bool LogicProgram::extractCore(const LitVec& solverCore, Potassco::LitVec& prgLi
 			Literal lit = atom->assumption();
 			if (lit == lit_true() || !ctx()->marked(lit)) continue;
 			prgLits.push_back(atom->literal() == lit ? Potassco::lit(*it) : Potassco::neg(*it));
-			ctx()->unmark(lit.var());
+			ctx()->unmark(lit);
 			--marked;
 		}
 		for (Potassco::LitVec::const_iterator it = assume_.begin(), end = assume_.end(); it != end && marked; ++it) {
 			Literal lit = getLiteral(Potassco::id(*it));
 			if (!ctx()->marked(lit)) continue;
 			prgLits.push_back(*it);
-			ctx()->unmark(lit.var());
+			ctx()->unmark(lit);
 			--marked;
 		}
 	}

diff --git a/tests/facade_test.cpp b/tests/facade_test.cpp
@@ -270,6 +270,25 @@ TEST_CASE("Facade", "[facade]") {
 		CHECK(out[0] == expect);
 	}
 
+	SECTION("testIssue81") {
+		config.solve.numModels = 0;
+		Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
+		lpAdd(asp, "{x}.\n"
+		           "a :- x.\n"
+		           "b :- not x.\n"
+		           "#assume{a,b}.");
+		libclasp.prepare();
+		REQUIRE(libclasp.solve().unsat());
+		const LitVec* core = libclasp.summary().unsatCore();
+		REQUIRE(core);
+		CHECK(core->size() == 2);
+		Potassco::LitVec out;
+		CHECK(asp.extractCore(*core, out));
+		CHECK(out.size() == 2);
+		CHECK(out[0] == 1);
+		CHECK(out[1] == 2);
+	}
+
 	SECTION("testComputeBrave") {
 		config.solve.numModels = 0;
 		config.solve.enumMode = EnumOptions::enum_brave;