1 //
2 // Copyright (c) 2006-2017 Benjamin Kaufmann
3 //
4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
5 //
6 // Permission is hereby granted, free of charge, to any person obtaining a copy
7 // of this software and associated documentation files (the "Software"), to
8 // deal in the Software without restriction, including without limitation the
9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
10 // sell copies of the Software, and to permit persons to whom the Software is
11 // furnished to do so, subject to the following conditions:
12 //
13 // The above copyright notice and this permission notice shall be included in
14 // all copies or substantial portions of the Software.
15 //
16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
22 // IN THE SOFTWARE.
23 //
24 #include <clasp/model_enumerators.h>
25 #include <clasp/solver.h>
26 #include <clasp/minimize_constraint.h>
27 #include <potassco/basic_types.h>
28 #include <clasp/dependency_graph.h>
29 #include <algorithm>
30 #include <cstdlib>
31 namespace Clasp {
32 class ModelEnumerator::ModelFinder : public EnumerationConstraint {
33 protected:
ModelFinder()34 explicit ModelFinder() : EnumerationConstraint() {}
hasModel() const35 bool hasModel() const { return !solution.empty(); }
36 LitVec solution;
37 };
38 /////////////////////////////////////////////////////////////////////////////////////////
39 // strategy_record
40 /////////////////////////////////////////////////////////////////////////////////////////
41 class ModelEnumerator::RecordFinder : public ModelFinder {
42 public:
RecordFinder()43 RecordFinder() : ModelFinder() { }
clone()44 ConPtr clone() { return new RecordFinder(); }
45 void doCommitModel(Enumerator& ctx, Solver& s);
46 bool doUpdate(Solver& s);
47 void addDecisionNogood(const Solver& s);
48 void addProjectNogood(const ModelEnumerator& ctx, const Solver& s, bool domain);
49 };
50
doUpdate(Solver & s)51 bool ModelEnumerator::RecordFinder::doUpdate(Solver& s) {
52 if (hasModel()) {
53 ConstraintInfo e(Constraint_t::Other);
54 ClauseCreator::Result ret = ClauseCreator::create(s, solution, ClauseCreator::clause_no_add, e);
55 solution.clear();
56 if (ret.local) { add(ret.local);}
57 if (!ret.ok()) { return false; }
58 }
59 return true;
60 }
addDecisionNogood(const Solver & s)61 void ModelEnumerator::RecordFinder::addDecisionNogood(const Solver& s) {
62 for (uint32 x = s.decisionLevel(); x != 0; --x) {
63 Literal d = s.decision(x);
64 if (!s.auxVar(d.var())) { solution.push_back(~d); }
65 else if (d != s.tagLiteral()) {
66 // Todo: set of vars could be reduced to those having the aux var in their reason set.
67 const LitVec& tr = s.trail();
68 const uint32 end = x != s.decisionLevel() ? s.levelStart(x+1) : (uint32)tr.size();
69 for (uint32 n = s.levelStart(x)+1; n != end; ++n) {
70 if (!s.auxVar(tr[n].var())) { solution.push_back(~tr[n]); }
71 }
72 }
73 }
74 }
addProjectNogood(const ModelEnumerator & ctx,const Solver & s,bool domain)75 void ModelEnumerator::RecordFinder::addProjectNogood(const ModelEnumerator& ctx, const Solver& s, bool domain) {
76 for (Var i = 1, end = s.numProblemVars(); i <= end; ++i) {
77 if (ctx.project(i)) {
78 Literal p = Literal(i, s.pref(i).sign());
79 if (!domain || !s.pref(i).has(ValueSet::user_value)) { solution.push_back(~s.trueLit(i)); }
80 else if (p != s.trueLit(i)) { solution.push_back(p); }
81 }
82 }
83 solution.push_back(~s.sharedContext()->stepLiteral());
84 }
doCommitModel(Enumerator & en,Solver & s)85 void ModelEnumerator::RecordFinder::doCommitModel(Enumerator& en, Solver& s) {
86 ModelEnumerator& ctx = static_cast<ModelEnumerator&>(en);
87 assert(solution.empty() && "Update not called!");
88 solution.clear();
89 if (ctx.trivial()) {
90 return;
91 }
92 else if (!ctx.projectionEnabled()) {
93 addDecisionNogood(s);
94 }
95 else {
96 addProjectNogood(ctx, s, ctx.domRec());
97 }
98 if (solution.empty()) { solution.push_back(lit_false()); }
99 if (s.sharedContext()->concurrency() > 1) {
100 // parallel solving active - share solution nogood with other solvers
101 en.commitClause(solution);
102 solution.clear();
103 }
104 }
105 /////////////////////////////////////////////////////////////////////////////////////////
106 // strategy_backtrack
107 /////////////////////////////////////////////////////////////////////////////////////////
108 class ModelEnumerator::BacktrackFinder : public ModelFinder {
109 public:
BacktrackFinder(uint32 projOpts)110 explicit BacktrackFinder(uint32 projOpts) : ModelFinder(), opts(projOpts) {}
111 // EnumerationConstraint interface
clone()112 ConPtr clone() { return new BacktrackFinder(opts); }
113 void doCommitModel(Enumerator& ctx, Solver& s);
114 bool doUpdate(Solver& s);
115 // Constraint interface
116 PropResult propagate(Solver&, Literal, uint32&);
reason(Solver & s,Literal p,LitVec & x)117 void reason(Solver& s, Literal p, LitVec& x){
118 for (uint32 i = 1, end = s.level(p.var()); i <= end; ++i) {
119 x.push_back(s.decision(i));
120 }
121 }
simplify(Solver & s,bool reinit)122 bool simplify(Solver& s, bool reinit) {
123 for (ProjectDB::iterator it = projNogoods.begin(), end = projNogoods.end(); it != end; ++it) {
124 if (it->second && it->second->simplify(s, false)) {
125 s.removeWatch(it->first, this);
126 it->second->destroy(&s, false);
127 it->second = 0;
128 }
129 }
130 while (!projNogoods.empty() && projNogoods.back().second == 0) { projNogoods.pop_back(); }
131 return ModelFinder::simplify(s, reinit);
132 }
destroy(Solver * s,bool detach)133 void destroy(Solver* s, bool detach) {
134 while (!projNogoods.empty()) {
135 NogoodPair x = projNogoods.back();
136 if (x.second) {
137 if (s) { s->removeWatch(x.first, this); }
138 x.second->destroy(s, detach);
139 }
140 projNogoods.pop_back();
141 }
142 ModelFinder::destroy(s, detach);
143 }
144 typedef std::pair<Literal, Constraint*> NogoodPair;
145 typedef PodVector<NogoodPair>::type ProjectDB;
146 ProjectDB projNogoods;
147 uint32 opts;
148 };
149
propagate(Solver & s,Literal,uint32 & pos)150 Constraint::PropResult ModelEnumerator::BacktrackFinder::propagate(Solver& s, Literal, uint32& pos) {
151 assert(pos < projNogoods.size() && projNogoods[pos].second != 0);
152 ClauseHead* c = static_cast<ClauseHead*>(projNogoods[pos].second);
153 if (!c->locked(s)) {
154 c->destroy(&s, true);
155 projNogoods[pos].second = (c = 0);
156 while (!projNogoods.empty() && !projNogoods.back().second) {
157 projNogoods.pop_back();
158 }
159 }
160 return PropResult(true, c != 0);
161 }
doUpdate(Solver & s)162 bool ModelEnumerator::BacktrackFinder::doUpdate(Solver& s) {
163 if (hasModel()) {
164 bool ok = true;
165 uint32 sp = (opts & ModelEnumerator::project_save_progress) != 0 ? Solver::undo_save_phases : 0;
166 s.undoUntil(s.backtrackLevel(), sp|Solver::undo_pop_bt_level);
167 ClauseRep rep = ClauseCreator::prepare(s, solution, 0, Constraint_t::Conflict);
168 if (rep.size == 0 || s.isFalse(rep.lits[0])) { // The decision stack is already ordered.
169 ok = s.backtrack();
170 }
171 else if (rep.size == 1 || s.isFalse(rep.lits[1])) { // The projection nogood is unit. Force the single remaining literal from the current DL.
172 ok = s.force(rep.lits[0], this);
173 }
174 else if (!s.isTrue(rep.lits[0])) { // Shorten the projection nogood by assuming one of its literals to false.
175 uint32 f = static_cast<uint32>(std::stable_partition(rep.lits+2, rep.lits+rep.size, std::not1(std::bind1st(std::mem_fun(&Solver::isFalse), &s))) - rep.lits);
176 Literal x = (opts & ModelEnumerator::project_use_heuristic) != 0 ? s.heuristic()->selectRange(s, rep.lits, rep.lits+f) : rep.lits[0];
177 Constraint* c = Clause::newContractedClause(s, rep, f, true);
178 POTASSCO_REQUIRE(c, "Invalid constraint!");
179 s.assume(~x);
180 // Remember that we must backtrack the current decision
181 // level in order to guarantee a different projected solution.
182 s.setBacktrackLevel(s.decisionLevel(), Solver::undo_pop_proj_level);
183 // Attach nogood to the current decision literal.
184 // Once we backtrack to x, the then obsolete nogood is destroyed
185 // keeping the number of projection nogoods linear in the number of (projection) atoms.
186 s.addWatch(x, this, (uint32)projNogoods.size());
187 projNogoods.push_back(NogoodPair(x, c));
188 ok = true;
189 }
190 solution.clear();
191 return ok;
192 }
193 if (optimize() || s.sharedContext()->concurrency() == 1 || disjointPath()) {
194 return true;
195 }
196 s.setStopConflict();
197 return false;
198 }
199
doCommitModel(Enumerator & ctx,Solver & s)200 void ModelEnumerator::BacktrackFinder::doCommitModel(Enumerator& ctx, Solver& s) {
201 ModelEnumerator& en = static_cast<ModelEnumerator&>(ctx);
202 uint32 dl = s.decisionLevel();
203 solution.assign(1, dl ? ~s.decision(dl) : lit_false());
204 if (en.projectionEnabled()) {
205 // Remember the current projected assignment as a nogood.
206 solution.clear();
207 for (Var i = 1, end = s.numProblemVars(); i <= end; ++i) {
208 if (en.project(i)) {
209 solution.push_back(~s.trueLit(i));
210 }
211 }
212 // Tag solution
213 solution.push_back(~s.sharedContext()->stepLiteral());
214 // Remember initial decisions that are projection vars.
215 for (dl = s.rootLevel(); dl < s.decisionLevel(); ++dl) {
216 if (!en.project(s.decision(dl+1).var())) { break; }
217 }
218 s.setBacktrackLevel(dl, Solver::undo_pop_proj_level);
219 }
220 else {
221 s.setBacktrackLevel(dl);
222 }
223 }
224 /////////////////////////////////////////////////////////////////////////////////////////
225 // class ModelEnumerator
226 /////////////////////////////////////////////////////////////////////////////////////////
ModelEnumerator(Strategy st)227 ModelEnumerator::ModelEnumerator(Strategy st)
228 : Enumerator() {
229 std::memset(&opts_, 0, sizeof(Options));
230 setStrategy(st);
231 trivial_ = false;
232 }
233
createModelEnumerator(const EnumOptions & opts)234 Enumerator* EnumOptions::createModelEnumerator(const EnumOptions& opts) {
235 ModelEnumerator* e = new ModelEnumerator();
236 ModelEnumerator::Strategy s = ModelEnumerator::strategy_auto;
237 if (opts.enumMode && opts.models()) {
238 s = opts.enumMode == enum_bt ? ModelEnumerator::strategy_backtrack : ModelEnumerator::strategy_record;
239 }
240 e->setStrategy(s, opts.project | (opts.enumMode == enum_dom_record ? ModelEnumerator::project_dom_lits : 0));
241 return e;
242 }
243
~ModelEnumerator()244 ModelEnumerator::~ModelEnumerator() {}
245
setStrategy(Strategy st,uint32 projection,char f)246 void ModelEnumerator::setStrategy(Strategy st, uint32 projection, char f) {
247 opts_.algo = st;
248 opts_.proj = projection;
249 filter_ = f;
250 if ((projection & 7u) != 0) {
251 opts_.proj |= uint32(project_enable_simple);
252 }
253 saved_ = opts_;
254 }
255
doInit(SharedContext & ctx,SharedMinimizeData * opt,int numModels)256 EnumerationConstraint* ModelEnumerator::doInit(SharedContext& ctx, SharedMinimizeData* opt, int numModels) {
257 opts_ = saved_;
258 initProjection(ctx);
259 if (ctx.concurrency() > 1 && !ModelEnumerator::supportsParallel()) {
260 opts_.algo = strategy_auto;
261 }
262 bool optOne = opt && opt->mode() == MinimizeMode_t::optimize;
263 bool trivial = (optOne && !domRec()) || std::abs(numModels) == 1;
264 if (optOne && projectionEnabled()) {
265 for (const WeightLiteral* it = minimizer()->lits; !isSentinel(it->first) && trivial; ++it) {
266 trivial = project(it->first.var());
267 }
268 if (!trivial) { ctx.warn("Projection: Optimization may depend on enumeration order."); }
269 }
270 if (opts_.algo == strategy_auto) { opts_.algo = trivial || (projectionEnabled() && ctx.concurrency() > 1) ? strategy_record : strategy_backtrack; }
271 trivial_ = trivial;
272 EnumerationConstraint* c = opts_.algo == strategy_backtrack
273 ? static_cast<ConPtr>(new BacktrackFinder(projectOpts()))
274 : static_cast<ConPtr>(new RecordFinder());
275 if (projectionEnabled()) { setIgnoreSymmetric(true); }
276 return c;
277 }
278
initProjection(SharedContext & ctx)279 void ModelEnumerator::initProjection(SharedContext& ctx) {
280 project_.clear();
281 if (!projectionEnabled()) { return; }
282 const OutputTable& out = ctx.output;
283 if (domRec()) {
284 const SolverParams& p = ctx.configuration()->solver(0);
285 const DomainTable& dom = ctx.heuristic;
286 const Solver& s = *ctx.master();
287 if (p.heuId == Heuristic_t::Domain) {
288 for (uint32 i = 0, end = dom.assume ? sizeVec(*dom.assume) : 0; i != end; ++i) {
289 ctx.mark((*dom.assume)[i]);
290 }
291 DomainTable pref;
292 for (DomainTable::iterator it = dom.begin(), end = dom.end(); it != end; ++it) {
293 if ((it->comp() || it->type() == DomModType::Level) && (s.isTrue(it->cond()) || ctx.marked(it->cond()))) {
294 pref.add(it->var(), it->type(), it->bias(), it->prio(), lit_true());
295 }
296 }
297 pref.simplify();
298 for (DomainTable::iterator it = pref.begin(), end = pref.end(); it != end; ++it) {
299 if (it->bias() > 0) { addProject(ctx, it->var()); }
300 }
301 for (uint32 i = 0, end = dom.assume ? sizeVec(*dom.assume) : 0; i != end; ++i) {
302 ctx.unmark((*dom.assume)[i].var());
303 }
304 if ((p.heuristic.domMod & HeuParams::mod_level) != 0u) {
305 struct AddProject : DomainTable::DefaultAction {
306 AddProject(ModelEnumerator& e, SharedContext& c) : en(&e), ctx(&c) {}
307 void atom(Literal p, HeuParams::DomPref, uint32) { en->addProject(*ctx, p.var()); }
308 ModelEnumerator* en; SharedContext* ctx;
309 } act(*this, ctx);
310 DomainTable::applyDefault(ctx, act, p.heuristic.domPref);
311 }
312 }
313 if (project_.empty()) {
314 ctx.warn("domRec ignored: No domain atoms found.");
315 opts_.proj -= project_dom_lits;
316 initProjection(ctx);
317 return;
318 }
319 else if (ctx.concurrency() > 1) {
320 for (uint32 i = 1, end = ctx.concurrency(); i != end; ++i) {
321 const SolverParams pi = ctx.configuration()->solver(i);
322 if (pi.heuId != p.heuId || pi.heuristic.domMod != p.heuristic.domMod || (pi.heuristic.domPref && pi.heuristic.domPref != p.heuristic.domPref)) {
323 ctx.warn("domRec: Inconsistent domain heuristics, results undefined.");
324 break;
325 }
326 }
327 }
328 }
329 else if (out.projectMode() == ProjectMode_t::Output) {
330 // Mark all relevant output variables.
331 for (OutputTable::pred_iterator it = out.pred_begin(), end = out.pred_end(); it != end; ++it) {
332 if (*it->name != filter_) { addProject(ctx, it->cond.var()); }
333 }
334 for (OutputTable::range_iterator it = out.vars_begin(), end = out.vars_end(); it != end; ++it) {
335 addProject(ctx, *it);
336 }
337 }
338 else {
339 // Mark explicitly requested variables only.
340 for (OutputTable::lit_iterator it = out.proj_begin(), end = out.proj_end(); it != end; ++it) {
341 addProject(ctx, it->var());
342 }
343 }
344 }
345
addProject(SharedContext & ctx,Var v)346 void ModelEnumerator::addProject(SharedContext& ctx, Var v) {
347 const uint32 wIdx = v / 32;
348 const uint32 bIdx = v & 31;
349 if (wIdx >= project_.size()) { project_.resize(wIdx + 1, 0); }
350 store_set_bit(project_[wIdx], bIdx);
351 ctx.setFrozen(v, true);
352 }
project(Var v) const353 bool ModelEnumerator::project(Var v) const {
354 const uint32 wIdx = v / 32;
355 const uint32 bIdx = v & 31;
356 return wIdx < project_.size() && test_bit(project_[wIdx], bIdx);
357 }
358
359 }
360