00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include <clasp/solve_algorithms.h>
00021 #include <clasp/solver.h>
00022 #include <clasp/enumerator.h>
00023 #include <clasp/minimize_constraint.h>
00024 #include <clasp/util/timer.h>
00025 #include <clasp/util/atomic.h>
00026 namespace Clasp {
00028
00030 struct BasicSolve::State {
00031 typedef BasicSolveEvent EventType;
00032 State(Solver& s, const SolveParams& p);
00033 ValueRep solve(Solver& s, const SolveParams& p, SolveLimits* lim);
00034 uint64 dbGrowNext;
00035 double dbMax;
00036 double dbHigh;
00037 ScheduleStrategy dbRed;
00038 uint32 nRestart;
00039 uint32 nGrow;
00040 uint32 dbRedInit;
00041 uint32 dbPinned;
00042 uint32 rsShuffle;
00043 };
00044
00045 BasicSolve::BasicSolve(Solver& s, SolveLimits* lim) : solver_(&s), params_(&s.searchConfig()), limits_(lim), state_(0) {}
00046 BasicSolve::BasicSolve(Solver& s, const SolveParams& p, SolveLimits* lim)
00047 : solver_(&s)
00048 , params_(&p)
00049 , limits_(lim)
00050 , state_(0) {
00051 }
00052
00053 BasicSolve::~BasicSolve(){ delete state_; }
00054 void BasicSolve::reset(bool reinit) {
00055 if (!state_ || reinit) {
00056 delete state_;
00057 state_ = 0;
00058 }
00059 else {
00060 state_->~State();
00061 new (state_) State(*solver_, *params_);
00062 }
00063 }
00064 void BasicSolve::reset(Solver& s, const SolveParams& p, SolveLimits* lim) {
00065 solver_ = &s;
00066 params_ = &p;
00067 limits_ = lim;
00068 reset(true);
00069 }
00070
00071 ValueRep BasicSolve::solve() {
00072 if (limits_ && limits_->reached()) { return value_free; }
00073 if (!state_ && !params_->randomize(*solver_)){ return value_false; }
00074 if (!state_) { state_ = new State(*solver_, *params_); }
00075 return state_->solve(*solver_, *params_, limits_);
00076 }
00077
00078 bool BasicSolve::satisfiable(const LitVec& path, bool init) {
00079 if (!solver_->clearAssumptions() || !solver_->pushRoot(path)){ return false; }
00080 if (init && !params_->randomize(*solver_)) { return false; }
00081 State temp(*solver_, *params_);
00082 return temp.solve(*solver_, *params_, 0) == value_true;
00083 }
00084
00085 bool BasicSolve::assume(const LitVec& path) {
00086 return solver_->pushRoot(path);
00087 }
00088
00089 BasicSolve::State::State(Solver& s, const SolveParams& p) {
00090 Range32 dbLim= p.reduce.sizeInit(*s.sharedContext());
00091 dbGrowNext = p.reduce.growSched.current();
00092 dbMax = dbLim.lo;
00093 dbHigh = dbLim.hi;
00094 dbRed = p.reduce.cflSched;
00095 nRestart = 0;
00096 nGrow = 0;
00097 dbRedInit = p.reduce.cflInit(*s.sharedContext());
00098 dbPinned = 0;
00099 rsShuffle = p.restart.shuffle;
00100 if (dbLim.lo < s.numLearntConstraints()) {
00101 dbMax = std::min(dbHigh, double(s.numLearntConstraints() + p.reduce.initRange.lo));
00102 }
00103 if (dbRedInit && dbRed.type != ScheduleStrategy::luby_schedule) {
00104 if (dbRedInit < dbRed.base) {
00105 dbRedInit = std::min(dbRed.base, std::max(dbRedInit,(uint32)5000));
00106 dbRed.grow = dbRedInit != dbRed.base ? std::min(dbRed.grow, dbRedInit/2.0f) : dbRed.grow;
00107 dbRed.base = dbRedInit;
00108 }
00109 dbRedInit = 0;
00110 }
00111 if (p.restart.dynamic()) {
00112 s.stats.enableQueue(p.restart.sched.base);
00113 s.stats.queue->resetGlobal();
00114 s.stats.queue->dynamicRestarts((float)p.restart.sched.grow, true);
00115 }
00116 s.stats.lastRestart = s.stats.analyzed;
00117 }
00118
00119 ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* lim) {
00120 assert(!lim || !lim->reached());
00121 if (s.hasConflict() && s.decisionLevel() == s.rootLevel()) {
00122 return value_false;
00123 }
00124 struct ConflictLimits {
00125 uint64 restart;
00126 uint64 reduce;
00127 uint64 grow;
00128 uint64 global;
00129 uint64 min() const { return std::min(std::min(restart, grow), std::min(reduce, global)); }
00130 void update(uint64 x) { restart -= x; reduce -= x; grow -= x; global -= x; }
00131 };
00132 WeightLitVec inDegree;
00133 SearchLimits sLimit;
00134 ScheduleStrategy rs = p.restart.sched;
00135 ScheduleStrategy dbGrow = p.reduce.growSched;
00136 Solver::DBInfo db = {0,0,dbPinned};
00137 ValueRep result = value_free;
00138 ConflictLimits cLimit = {UINT64_MAX, dbRed.current() + dbRedInit, dbGrowNext, lim ? lim->conflicts : UINT64_MAX};
00139 uint64 limRestarts = lim ? lim->restarts : UINT64_MAX;
00140 uint64& rsLimit = p.restart.local() ? sLimit.local : cLimit.restart;
00141 if (!dbGrow.disabled()) { dbGrow.advanceTo(nGrow); }
00142 if (nRestart == UINT32_MAX && p.restart.update() == RestartParams::seq_disable) {
00143 cLimit.restart = UINT64_MAX;
00144 sLimit = SearchLimits();
00145 }
00146 else if (p.restart.dynamic()) {
00147 if (!nRestart) { s.stats.queue->resetQueue(); s.stats.queue->dynamicRestarts((float)p.restart.sched.grow, true); }
00148 sLimit.dynamic = s.stats.queue;
00149 rsLimit = sLimit.dynamic->upForce - std::min(sLimit.dynamic->samples, sLimit.dynamic->upForce - 1);
00150 }
00151 else {
00152 rs.advanceTo(!rs.disabled() ? nRestart : 0);
00153 rsLimit = rs.current();
00154 }
00155 sLimit.setMemLimit(p.reduce.memMax);
00156 for (EventType progress(s, EventType::event_restart, 0, 0); cLimit.global; ) {
00157 uint64 minLimit = cLimit.min(); assert(minLimit);
00158 sLimit.learnts = (uint32)std::min(dbMax + (db.pinned*p.reduce.strategy.noGlue), dbHigh);
00159 sLimit.conflicts= minLimit;
00160 progress.cLimit = std::min(minLimit, sLimit.local);
00161 progress.lLimit = sLimit.learnts;
00162 if (progress.op) { s.sharedContext()->report(progress); progress.op = (uint32)EventType::event_none; }
00163 result = s.search(sLimit, p.randProb);
00164 minLimit -= sLimit.conflicts;
00165 if (result != value_free) {
00166 progress.op = static_cast<uint32>(EventType::event_exit);
00167 if (result == value_true && p.restart.update() != RestartParams::seq_continue) {
00168 if (p.restart.update() == RestartParams::seq_repeat) { nRestart = 0; }
00169 else if (p.restart.update() == RestartParams::seq_disable){ nRestart = UINT32_MAX; }
00170 }
00171 if (!dbGrow.disabled()) { dbGrowNext = std::max(cLimit.grow - minLimit, uint64(1)); }
00172 s.sharedContext()->report(progress);
00173 break;
00174 }
00175 cLimit.update(minLimit);
00176 minLimit = 0;
00177 if (rsLimit == 0 || sLimit.hasDynamicRestart()) {
00178
00179 ++nRestart;
00180 if (p.restart.counterRestart && (nRestart % p.restart.counterRestart) == 0 ) {
00181 inDegree.clear();
00182 s.heuristic()->bump(s, inDegree, p.restart.counterBump / (double)s.inDegree(inDegree));
00183 }
00184 if (sLimit.dynamic) {
00185 minLimit = sLimit.dynamic->samples;
00186 rsLimit = sLimit.dynamic->restart(rs.len ? rs.len : UINT32_MAX, (float)rs.grow);
00187 }
00188 s.restart();
00189 if (rsLimit == 0) { rsLimit = rs.next(); }
00190 if (!minLimit) { minLimit = rs.current(); }
00191 if (p.reduce.strategy.fRestart){ db = s.reduceLearnts(p.reduce.fRestart(), p.reduce.strategy); }
00192 if (nRestart == rsShuffle) { rsShuffle+= p.restart.shuffleNext; s.shuffleOnNextSimplify();}
00193 if (--limRestarts == 0) { break; }
00194 s.stats.lastRestart = s.stats.analyzed;
00195 progress.op = (uint32)EventType::event_restart;
00196 }
00197 if (cLimit.reduce == 0 || s.learntLimit(sLimit)) {
00198
00199 db = s.reduceLearnts(p.reduce.fReduce(), p.reduce.strategy);
00200 cLimit.reduce = dbRedInit + (cLimit.reduce == 0 ? dbRed.next() : dbRed.current());
00201 progress.op = std::max(progress.op, (uint32)EventType::event_deletion);
00202 if (s.learntLimit(sLimit) || db.pinned >= dbMax) {
00203 ReduceStrategy t; t.algo = 2; t.score = 2; t.glue = 0;
00204 db.pinned /= 2;
00205 db.size = s.reduceLearnts(0.5f, t).size;
00206 if (db.size >= sLimit.learnts) { dbMax = std::min(dbMax + std::max(100.0, s.numLearntConstraints()/10.0), dbHigh); }
00207 }
00208 }
00209 if (cLimit.grow == 0 || (dbGrow.defaulted() && progress.op == (uint32)EventType::event_restart)) {
00210
00211 if (cLimit.grow == 0) { cLimit.grow = dbGrow.next(); minLimit = cLimit.grow; ++nGrow; }
00212 if ((s.numLearntConstraints() + minLimit) > dbMax){ dbMax *= p.reduce.fGrow; progress.op = std::max(progress.op, (uint32)EventType::event_grow); }
00213 if (dbMax > dbHigh) { dbMax = dbHigh; cLimit.grow = UINT64_MAX; dbGrow = ScheduleStrategy::none(); }
00214 }
00215 }
00216 dbPinned = db.pinned;
00217 s.stats.lastRestart = s.stats.analyzed - s.stats.lastRestart;
00218 if (lim) {
00219 if (lim->conflicts != UINT64_MAX) { lim->conflicts = cLimit.global; }
00220 if (lim->restarts != UINT64_MAX) { lim->restarts = limRestarts; }
00221 }
00222 return result;
00223 }
00225
00227 SolveAlgorithm::SolveAlgorithm(Enumerator* e, const SolveLimits& lim) : limits_(lim), enum_(e), onModel_(0), enumLimit_(UINT64_MAX) {}
00228 SolveAlgorithm::~SolveAlgorithm() {}
00229
00230 bool SolveAlgorithm::interrupt() {
00231 return doInterrupt();
00232 }
00233 bool SolveAlgorithm::solve(SharedContext& ctx, const LitVec& assume, EventHandler* onModel) {
00234 if (!ctx.frozen() && !ctx.endInit()) { return false; }
00235 if (!limits_.conflicts || interrupted()){ return true; }
00236 struct Scoped {
00237 explicit Scoped(SolveAlgorithm& self, SharedContext& x) : algo(&self), ctx(&x), temp(0), time(0.0) { }
00238 ~Scoped() {
00239 ctx->master()->stats.addCpuTime(ThreadTime::getTime() - time);
00240 if (algo->enum_ == temp) { algo->enum_ = 0; }
00241 algo->onModel_ = 0;
00242 delete temp;
00243 }
00244 bool solve(const LitVec& assume, EventHandler* h) {
00245 ctx->report(message<Event::verbosity_low>(Event::subsystem_solve, "Solving"));
00246 time = ThreadTime::getTime();
00247 if (!algo->enum_) { temp = EnumOptions::nullEnumerator(); algo->setEnumerator(*temp); }
00248 algo->onModel_ = h;
00249 return algo->doSolve(*ctx, assume);
00250 }
00251 SolveAlgorithm* algo;
00252 SharedContext* ctx;
00253 Enumerator* temp;
00254 double time;
00255 };
00256 return Scoped(*this, ctx).solve(assume, onModel);
00257 }
00258 bool SolveAlgorithm::reportModel(Solver& s) const {
00259 for (const Model& m = enum_->lastModel();;) {
00260 bool r1 = !onModel_ || onModel_->onModel(s, m);
00261 bool r2 = s.sharedContext()->report(s, m);
00262 bool res= r1 && r2 && (enumLimit_ > m.num || enum_->tentative());
00263 if (!res || (res = !interrupted()) == false || !enum_->commitSymmetric(s)) { return res; }
00264 }
00265 }
00267
00269 struct SequentialSolve::InterruptHandler : public MessageHandler {
00270 InterruptHandler() : solver(0) { term = 0; }
00271 bool terminated() const { return term != 0; }
00272 bool terminate() { return (term = 1) != 0; }
00273 bool attach(Solver& s) { return !terminated() && (solver = &s)->addPost(this); }
00274 void detach() { if (solver) { solver->removePost(this); solver = 0; } }
00275 bool handleMessages() { return !terminated() || (solver->setStopConflict(), false); }
00276 bool propagateFixpoint(Solver&, PostPropagator*){ return InterruptHandler::handleMessages(); }
00277 Solver* solver;
00278 Clasp::atomic<int> term;
00279 };
00280 SequentialSolve::SequentialSolve(Enumerator* enumerator, const SolveLimits& limit)
00281 : SolveAlgorithm(enumerator, limit)
00282 , term_(0) {
00283 }
00284 SequentialSolve::~SequentialSolve() {
00285 if (term_) { term_->detach(); delete term_; }
00286 }
00287 void SequentialSolve::resetSolve() { if (term_) { term_->term = 0; } }
00288 bool SequentialSolve::doInterrupt() { return term_ && term_->terminate(); }
00289 void SequentialSolve::enableInterrupts() { if (!term_) { term_ = new InterruptHandler(); } }
00290 bool SequentialSolve::interrupted() const{ return term_ && term_->terminated(); }
00291
00292 bool SequentialSolve::doSolve(SharedContext& ctx, const LitVec& gp) {
00293 Solver& s = *ctx.master();
00294 SolveLimits lim = limits();
00295 uint32 root = s.rootLevel();
00296 BasicSolve solve(s, ctx.configuration()->search(0), &lim);
00297 bool stop = term_ && !term_->attach(s);
00298 bool more = !stop && ctx.attach(s) && enumerator().start(s, gp);
00299
00300
00301 for (ValueRep res; more; solve.reset()) {
00302 while ((res = solve.solve()) == value_true && (!enumerator().commitModel(s) || reportModel(s))) {
00303 enumerator().update(s);
00304 }
00305 if (res != value_false) { more = (res == value_free || s.decisionLevel() != root); break; }
00306 else if ((stop=interrupted()) == true) { break; }
00307 else if (enumerator().commitUnsat(s)) { enumerator().update(s); }
00308 else if (enumerator().commitComplete()){ more = false; break; }
00309 else { enumerator().end(s); more = enumerator().start(s, gp); }
00310 }
00311 s.popRootLevel(s.rootLevel() - root);
00312 setLimits(lim);
00313 if (term_) { term_->detach(); }
00314 ctx.detach(s);
00315 return more || stop;
00316 }
00317 }