Issue #59: Add support for getting final conflict.

* Add SolveHandle::unsatCore(). When a problem is unsat when solving under assumptions, this function returns a subset of the initial assumption literals that together made the problem unsat.
potassco · Apr 10, 2020 · c5391b5 · c5391b5
1 parent 988675e
commit c5391b5
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 13 deletions.
diff --git a/clasp/clasp_facade.h b/clasp/clasp_facade.h
@@ -159,8 +159,9 @@ class ClaspFacade : public ModelHandler {
 	//! A handle to a possibly asynchronously computed SolveResult.
 	class SolveHandle {
 	public:
-		typedef SolveResult  Result;
-		typedef const Model* ModelRef;
+		typedef SolveResult   Result;
+		typedef const Model*  ModelRef;
+		typedef const LitVec* CoreRef;
 		explicit SolveHandle(SolveStrategy*);
 		SolveHandle(const SolveHandle&);
 		~SolveHandle();
@@ -171,6 +172,8 @@ class ClaspFacade : public ModelHandler {
 		 * @{ */
 		//! Waits until a result is ready and returns it.
 		Result   get()              const;
+		//! Returns an unsat core if get() returned unsat under assumptions.
+		CoreRef  unsatCore()        const;
 		//! Waits until a result is ready and returns it if it is a model.
 		/*!
 		 * \note If the corresponding solve operation was not started with

diff --git a/clasp/solve_algorithms.h b/clasp/solve_algorithms.h
@@ -145,6 +145,7 @@ class SolveAlgorithm {
 	const SolveLimits&  limits()     const { return limits_; }
 	virtual bool        interrupted()const = 0;
 	const Model&        model()      const;
+	const LitVec*       unsatCore()  const;
 
 	void setEnumerator(Enumerator& e);
 	void setEnumLimit(uint64 m)          { enumLimit_= m;  }
@@ -229,6 +230,7 @@ class SolveAlgorithm {
 private:
 	typedef SingleOwnerPtr<Enumerator>   EnumPtr;
 	typedef SingleOwnerPtr<const LitVec> PathPtr;
+	typedef SingleOwnerPtr<LitVec>       CorePtr;
 	enum { value_stop = value_false|value_true };
 	bool attach(SharedContext& ctx, ModelHandler* onModel);
 	void detach();
@@ -237,6 +239,7 @@ class SolveAlgorithm {
 	EnumPtr        enum_;
 	ModelHandler*  onModel_;
 	PathPtr        path_;
+	CorePtr        core_;
 	uint64         enumLimit_;
 	double         time_;
 	int            last_;

diff --git a/src/clasp_facade.cpp b/src/clasp_facade.cpp
@@ -236,6 +236,11 @@ struct ClaspFacade::SolveStrategy {
 			? &algo_->model()
 			: 0;
 	}
+	const LitVec* unsatCore() {
+		return result().unsat()
+			? algo_->unsatCore()
+			: 0;
+	}
 	bool next() {
 		return running() && (state_ != state_model || (resume(), true)) && model() != 0;
 	}
@@ -515,17 +520,18 @@ void ClaspFacade::SolveData::prepareEnum(SharedContext& ctx, int64 numM, EnumOpt
 ClaspFacade::SolveHandle::SolveHandle(SolveStrategy* s) : strat_(s->share()) {}
 ClaspFacade::SolveHandle::~SolveHandle() { strat_->release(); }
 ClaspFacade::SolveHandle::SolveHandle(const SolveHandle& o) : strat_(o.strat_->share()) {}
-int  ClaspFacade::SolveHandle::interrupted()     const { return strat_->signal(); }
-bool ClaspFacade::SolveHandle::error()           const { return ready() && strat_->error(); }
-bool ClaspFacade::SolveHandle::ready()           const { return strat_->ready(); }
-bool ClaspFacade::SolveHandle::running()         const { return strat_->running(); }
-void ClaspFacade::SolveHandle::cancel()          const { strat_->interrupt(SolveStrategy::SIGCANCEL); }
-void ClaspFacade::SolveHandle::wait()            const { strat_->wait(-1.0); }
-bool ClaspFacade::SolveHandle::waitFor(double s) const { return strat_->wait(s); }
-void ClaspFacade::SolveHandle::resume()          const { strat_->resume(); }
-SolveResult ClaspFacade::SolveHandle::get()      const { return strat_->result(); }
-const Model* ClaspFacade::SolveHandle::model()   const { return strat_->model(); }
-bool ClaspFacade::SolveHandle::next()            const { return strat_->next(); }
+int  ClaspFacade::SolveHandle::interrupted()        const { return strat_->signal(); }
+bool ClaspFacade::SolveHandle::error()              const { return ready() && strat_->error(); }
+bool ClaspFacade::SolveHandle::ready()              const { return strat_->ready(); }
+bool ClaspFacade::SolveHandle::running()            const { return strat_->running(); }
+void ClaspFacade::SolveHandle::cancel()             const { strat_->interrupt(SolveStrategy::SIGCANCEL); }
+void ClaspFacade::SolveHandle::wait()               const { strat_->wait(-1.0); }
+bool ClaspFacade::SolveHandle::waitFor(double s)    const { return strat_->wait(s); }
+void ClaspFacade::SolveHandle::resume()             const { strat_->resume(); }
+SolveResult ClaspFacade::SolveHandle::get()         const { return strat_->result(); }
+const Model*  ClaspFacade::SolveHandle::model()     const { return strat_->model(); }
+const LitVec* ClaspFacade::SolveHandle::unsatCore() const { return strat_->unsatCore(); }
+bool ClaspFacade::SolveHandle::next()               const { return strat_->next(); }
 /////////////////////////////////////////////////////////////////////////////////////////
 // ClaspFacade::Statistics
 /////////////////////////////////////////////////////////////////////////////////////////

diff --git a/src/solve_algorithms.cpp b/src/solve_algorithms.cpp
@@ -258,6 +258,9 @@ void SolveAlgorithm::setEnumerator(Enumerator& e) {
 const Model& SolveAlgorithm::model() const {
 	return enum_->lastModel();
 }
+const LitVec* SolveAlgorithm::unsatCore() const {
+	return core_.get();
+}
 bool SolveAlgorithm::interrupt() {
 	return doInterrupt();
 }
@@ -273,11 +276,33 @@ bool SolveAlgorithm::attach(SharedContext& ctx, ModelHandler* onModel) {
 	time_    = ThreadTime::getTime();
 	onModel_ = onModel;
 	last_    = value_free;
+	core_.reset(0);
 	if (!enum_.get()) { enum_ = EnumOptions::nullEnumerator(); }
 	return true;
 }
 void SolveAlgorithm::detach() {
 	if (ctx_) {
+		if (enum_->enumerated() == 0 && !path_->empty() && !interrupted()) {
+			uint32  w = ctx_->winner();
+			Solver* s = ctx_->hasSolver(w) ? ctx_->solver(w) : ctx_->solver(0);
+			s->popRootLevel(s->rootLevel());
+			core_ = new LitVec();
+			for (LitVec::const_iterator it = path_->begin(); it != path_->end(); ++it) {
+				if (isSentinel(*it) || s->isTrue(*it) || *it == ctx_->stepLiteral() || !ctx_->varInfo(it->var()).input())
+					continue;
+				core_->push_back(*it);
+				if (!s->pushRoot(*it)) {
+					if (!s->isFalse(*it)) {
+						core_->clear();
+						s->resolveToCore(*core_);
+					}
+					break;
+				}
+			}
+			s->popRootLevel(s->rootLevel());
+			if (core_->empty())
+				core_.reset(0);
+		}
 		ctx_->master()->stats.addCpuTime(ThreadTime::getTime() - time_);
 		onModel_ = 0;
 		ctx_     = 0;