00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include <clasp/solver_strategies.h>
00021 #include <clasp/solver.h>
00022 #include <clasp/unfounded_check.h>
00023 #include <clasp/heuristics.h>
00024 #include <clasp/lookahead.h>
00025 #include <cmath>
00026 namespace Clasp {
00028
00030 SolverStrategies::SolverStrategies() {
00031 struct X { uint32 z[2]; };
00032 static_assert(sizeof(SolverStrategies) == sizeof(X), "Unsupported Padding");
00033 std::memset(this, 0, sizeof(SolverStrategies));
00034 ccMinAntes = all_antes;
00035 initWatches= 1;
00036 search = use_learning;
00037 loadCfg = 1;
00038 }
00039 void SolverStrategies::prepare() {
00040 if (search == SolverStrategies::no_learning) {
00041 compress = 0;
00042 saveProgress= 0;
00043 reverseArcs = 0;
00044 otfs = 0;
00045 updateLbd = 0;
00046 ccMinAntes = SolverStrategies::no_antes;
00047 bumpVarAct = 0;
00048 }
00049 }
00050 SolverParams::SolverParams() {
00051 struct X { uint32 strat[2]; uint32 self[3]; };
00052 static_assert(sizeof(SolverParams) == sizeof(X), "Unsupported Padding");
00053 std::memset((&seed)+1, 0, sizeof(uint32)*2);
00054 seed = RNG().seed();
00055 heuOther = 3;
00056 heuMoms = 1;
00057 }
00058 uint32 SolverParams::prepare() {
00059 uint32 res = 0;
00060 if (search == SolverStrategies::no_learning && Heuristic_t::isLookback(heuId)) {
00061 heuId = Heuristic_t::heu_none;
00062 res |= 1;
00063 }
00064 if (heuId == Heuristic_t::heu_unit) {
00065 if (lookType == Lookahead::no_lookahead || lookOps != 0) { res |= 2; }
00066 heuParam = lookType == Lookahead::no_lookahead ? Lookahead::atom_lookahead : static_cast<Lookahead::Type>(lookType);
00067 lookType = Lookahead::no_lookahead;
00068 lookOps = 0;
00069 }
00070 SolverStrategies::prepare();
00071 return res;
00072 }
00074
00076 double growR(uint32 idx, double g) { return pow(g, (double)idx); }
00077 double addR(uint32 idx, double a) { return a * idx; }
00078 uint32 lubyR(uint32 idx) {
00079 uint32 i = idx + 1;
00080 while ((i & (i+1)) != 0) {
00081 i -= ((1u << log2(i)) - 1);
00082 }
00083 return (i+1)>>1;
00084 }
00085 ScheduleStrategy::ScheduleStrategy(Type t, uint32 b, double up, uint32 lim)
00086 : base(b), type(t), idx(0), len(lim), grow(0.0) {
00087 if (t == geometric_schedule) { grow = static_cast<float>(std::max(1.0, up)); }
00088 else if (t == arithmetic_schedule) { grow = static_cast<float>(std::max(0.0, up)); }
00089 else if (t == user_schedule) { grow = static_cast<float>(std::max(0.0, up)); }
00090 else if (t == luby_schedule && lim){ len = std::max(uint32(2), (static_cast<uint32>(std::pow(2.0, std::ceil(log(double(lim))/log(2.0)))) - 1)*2); }
00091 }
00092
00093 uint64 ScheduleStrategy::current() const {
00094 enum { t_add = ScheduleStrategy::arithmetic_schedule, t_luby = ScheduleStrategy::luby_schedule };
00095 if (base == 0) return UINT64_MAX;
00096 else if (type == t_add) return static_cast<uint64>(addR(idx, grow) + base);
00097 else if (type == t_luby)return static_cast<uint64>(lubyR(idx)) * base;
00098 uint64 x = static_cast<uint64>(growR(idx, grow) * base);
00099 return x + !x;
00100 }
00101 uint64 ScheduleStrategy::next() {
00102 if (++idx != len) { return current(); }
00103
00104 len = (len + !!idx) << uint32(type == luby_schedule);
00105 idx = 0;
00106 return current();
00107 }
00108 void ScheduleStrategy::advanceTo(uint32 n) {
00109 if (!len || n < len) {
00110 idx = n;
00111 return;
00112 }
00113 if (type != luby_schedule) {
00114 double dLen = len;
00115 uint32 x = uint32(sqrt(dLen * (4.0 * dLen - 4.0) + 8.0 * double(n+1))-2*dLen+1)/2;
00116 idx = n - uint32(x*dLen+double(x-1.0)*x/2.0);
00117 len += x;
00118 return;
00119 }
00120 while (n >= len) {
00121 n -= len++;
00122 len *= 2;
00123 }
00124 idx = n;
00125 }
00127
00129 void RestartParams::disable() {
00130 std::memset(this, 0, sizeof(RestartParams));
00131 sched = ScheduleStrategy::none();
00132 }
00133 uint32 RestartParams::prepare(bool withLookback) {
00134 if (!withLookback || sched.disabled()) {
00135 disable();
00136 }
00137 return 0;
00138 }
00139 uint32 SumQueue::restart(uint32 maxLBD, float limMax) {
00140 ++nRestart;
00141 if (upCfl >= upForce) {
00142 double avg = upCfl / double(nRestart);
00143 double gLbd= globalAvgLbd();
00144 bool sx = samples >= upForce;
00145 upCfl = 0;
00146 nRestart = 0;
00147 if (avg >= 16000.0) { lim += 0.1f; upForce = 16000; }
00148 else if (sx) { lim += 0.05f; upForce = std::max(uint32(16000), upForce-10000); }
00149 else if (avg >= 4000.0) { lim += 0.05f; }
00150 else if (avg >= 1000.0) { upForce += 10000u; }
00151 else if (lim > limMax) { lim -= 0.05f; }
00152 if ((gLbd > maxLBD)==lbd){ dynamicRestarts(limMax, !lbd); }
00153 }
00154 resetQueue();
00155 return upForce;
00156 }
00158
00160 uint32 ReduceParams::getLimit(uint32 base, double f, const Range32& r) {
00161 base = (f != 0.0 ? (uint32)std::min(base*f, double(UINT32_MAX)) : UINT32_MAX);
00162 return r.clamp( base );
00163 }
00164 uint32 ReduceParams::getBase(const SharedContext& ctx) const {
00165 uint32 st = strategy.estimate != ReduceStrategy::est_dynamic || ctx.isExtended() ? strategy.estimate : (uint32)ReduceStrategy::est_num_constraints;
00166 switch(st) {
00167 default:
00168 case ReduceStrategy::est_dynamic : {
00169 uint32 m = std::min(ctx.stats().vars, ctx.stats().numConstraints());
00170 uint32 M = std::max(ctx.stats().vars, ctx.stats().numConstraints());
00171 return M > (m * 10) ? M : m;
00172 }
00173 case ReduceStrategy::est_con_complexity : return ctx.stats().complexity;
00174 case ReduceStrategy::est_num_constraints: return ctx.stats().numConstraints();
00175 case ReduceStrategy::est_num_vars : return ctx.stats().vars;
00176 }
00177 }
00178 void ReduceParams::disable() {
00179 cflSched = ScheduleStrategy::none();
00180 growSched = ScheduleStrategy::none();
00181 strategy.fReduce = 0;
00182 fGrow = 0.0f; fInit = 0.0f; fMax = 0.0f;
00183 initRange = Range<uint32>(UINT32_MAX, UINT32_MAX);
00184 maxRange = UINT32_MAX;
00185 memMax = 0;
00186 }
00187 Range32 ReduceParams::sizeInit(const SharedContext& ctx) const {
00188 if (!growSched.disabled() || growSched.defaulted()) {
00189 uint32 base = getBase(ctx);
00190 uint32 lo = std::min(getLimit(base, fInit, initRange), maxRange);
00191 uint32 hi = getLimit(base, fMax, Range32(lo, maxRange));
00192 return Range32(lo, hi);
00193 }
00194 return Range32(maxRange, maxRange);
00195 }
00196 uint32 ReduceParams::cflInit(const SharedContext& ctx) const {
00197 return cflSched.disabled() ? 0 : getLimit(getBase(ctx), fInit, initRange);
00198 }
00199 uint32 ReduceParams::prepare(bool withLookback) {
00200 if (!withLookback || fReduce() == 0.0f) {
00201 disable();
00202 return 0;
00203 }
00204 if (cflSched.defaulted() && growSched.disabled() && !growSched.defaulted()) {
00205 cflSched = ScheduleStrategy::arith(4000, 600);
00206 }
00207 if (fMax != 0.0f) { fMax = std::max(fMax, fInit); }
00208 return 0;
00209 }
00211
00213 SolveParams::SolveParams()
00214 : randRuns(0u), randConf(0u)
00215 , randProb(0.0f) {
00216 }
00217 uint32 SolveParams::prepare(bool withLookback) {
00218 return restart.prepare(withLookback) | reduce.prepare(withLookback);
00219 }
00220 bool SolveParams::randomize(Solver& s) const {
00221 for (uint32 r = 0, c = randConf; r != randRuns && c; ++r) {
00222 if (s.search(c, UINT32_MAX, false, 1.0) != value_free) { return !s.hasConflict(); }
00223 s.undoUntil(0);
00224 }
00225 return true;
00226 }
00228
00230 Configuration::~Configuration() {}
00231 bool Configuration::addPost(Solver& s) const {
00232 if (s.sharedContext() && s.sharedContext()->sccGraph.get() && !s.getPost(PostPropagator::priority_reserved_ufs)) {
00233 return s.addPost(new DefaultUnfoundedCheck());
00234 }
00235 return true;
00236 }
00237 bool UserConfiguration::addPost(Solver& s) const {
00238 const SolverOpts& x = solver(s.id());
00239 bool ok = true;
00240 if (x.lookType != Lookahead::no_lookahead && x.lookOps == 0 && !s.getPost(PostPropagator::priority_reserved_look)) {
00241 ok = s.addPost(new Lookahead(static_cast<Lookahead::Type>(x.lookType)));
00242 }
00243 return ok && Configuration::addPost(s);
00244 }
00245 BasicSatConfig::BasicSatConfig() {
00246 solver_.push_back(SolverParams());
00247 search_.push_back(SolveParams());
00248 }
00249 void BasicSatConfig::prepare(SharedContext& ctx) {
00250 uint32 warn = 0;
00251 for (uint32 i = 0, end = solver_.size(), mod = search_.size(); i != end; ++i) {
00252 warn |= solver_[i].prepare();
00253 warn |= search_[i%mod].prepare(solver_[i].search != SolverStrategies::no_learning);
00254 }
00255 if ((warn & 1) != 0) { ctx.report(warning(Event::subsystem_facade, "Selected heuristic requires lookback strategy!")); }
00256 if ((warn & 2) != 0) { ctx.report(warning(Event::subsystem_facade, "Heuristic 'Unit' implies lookahead. Using atom.")); }
00257 }
00258 DecisionHeuristic* BasicSatConfig::heuristic(uint32 i) const {
00259 return Heuristic_t::create(BasicSatConfig::solver(i));
00260 }
00261 SolverParams& BasicSatConfig::addSolver(uint32 i) {
00262 if (i >= solver_.size()) { solver_.resize(i+1); solver_[i].id = i;}
00263 return solver_[i];
00264 }
00265 SolveParams& BasicSatConfig::addSearch(uint32 i) {
00266 if (i >= search_.size()) { search_.resize(i+1); }
00267 return search_[i];
00268 }
00269
00270 void BasicSatConfig::reset() {
00271 static_cast<ContextParams&>(*this) = ContextParams();
00272 BasicSatConfig::resize(1, 1);
00273 solver_[0] = SolverParams();
00274 search_[0] = SolveParams();
00275 }
00276 void BasicSatConfig::resize(uint32 solver, uint32 search) {
00277 solver_.resize(solver);
00278 search_.resize(search);
00279 }
00281
00283 DecisionHeuristic* Heuristic_t::create(const SolverParams& str) {
00284 if (str.search != SolverStrategies::use_learning && Heuristic_t::isLookback(str.heuId)) {
00285 throw std::logic_error("Selected heuristic requires lookback!");
00286 }
00287 typedef DecisionHeuristic DH;
00288 uint32 heuParam = str.heuParam;
00289 uint32 id = str.heuId;
00290 DH* heu = 0;
00291 HeuParams params;
00292 params.other(str.heuOther);
00293 params.init(str.heuMoms);
00294 params.score(str.berkOnce);
00295 if (id == heu_default) { id = str.search == SolverStrategies::use_learning ? heu_berkmin : heu_none; }
00296 if (id == heu_berkmin) { heu = new ClaspBerkmin(heuParam, params, str.berkHuang != 0); }
00297 else if (id == heu_vmtf) { heu = new ClaspVmtf(heuParam == 0 ? 8 : heuParam, params); }
00298 else if (id == heu_unit) {
00299 Lookahead::Params p(Lookahead::isType(heuParam) ? static_cast<Lookahead::Type>(heuParam) : Lookahead::atom_lookahead);
00300 heu = new UnitHeuristic(p.nant(str.unitNant!=0));
00301 }
00302 else if (id == heu_none) { heu = new SelectFirst(); }
00303 else if (id == heu_vsids || id == heu_domain) {
00304 double m = heuParam == 0 ? 0.95 : heuParam;
00305 while (m > 1.0) { m /= 10; }
00306 heu = id == heu_vsids ? (DH*)new ClaspVsids(m, params) : (DH*)new DomainHeuristic(m, params);
00307 }
00308 else { throw std::logic_error("Unknown heuristic id!"); }
00309 if (str.lookType != Lookahead::no_lookahead && str.lookOps > 0 && id != heu_unit) {
00310 heu = UnitHeuristic::restricted(Lookahead::Params(static_cast<Lookahead::Type>(str.lookType)).nant(str.unitNant != 0), str.lookOps, heu);
00311 }
00312 return heu;
00313 }
00314
00315 }