uint64_t origProps = solver.propagations;
//If failed var searching is going good, do successively more and more of it
- if (lastTimeFoundTruths > 500 || (double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.05) std::max(numPropsMultiplier*1.7, 5.0);
+ if (lastTimeFoundTruths > 500 || (double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.03) std::max(numPropsMultiplier*1.7, 5.0);
else numPropsMultiplier = 1.0;
numProps = (uint64_t) ((double)numProps * numPropsMultiplier);
propValue.resize(solver.nVars(), 0);
vector<pair<Var, bool> > bothSame;
+ //For calculating how many variables have really been set
+ uint32_t origTrailSize = solver.trail.size();
+
//For 2-long xor (rule 6 of Equivalent literal propagation in the DLL procedure by Chu-Min Li)
set<TwoLongXor> twoLongXors;
uint32_t toReplaceBefore = solver.varReplacer->getNewToReplaceVars();
}
}
- lastTimeFoundTruths = goodBothSame + numFailed;
+ lastTimeFoundTruths = solver.trail.size() - origTrailSize;
solver.var_inc = backup_var_inc;
std::copy(backup_activity.getData(), backup_activity.getDataEnd(), solver.activity.getData());
, ok (true)
, var_inc (128)
+ , cla_inc (1)
, curRestart (1)
, nbclausesbeforereduce (NBCLAUSESBEFOREREDUCE)
, remove_satisfied (true)
, mtrand((unsigned long int)0)
, restartType (static_restart)
+ , lastSelectedRestartType (static_restart)
#ifdef STATS_NEEDED
, logger(verbosity)
, dynamic_behaviour_analysis(false) //do not document the proof as default
| Effect:
| Will undo part of the trail, upto but not beyond the assumption of the current decision level.
|________________________________________________________________________________________________@*/
-Clause* Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, int &nbLevels/*, int &merged*/)
+Clause* Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, int &nbLevels, const bool update)
{
int pathC = 0;
Lit p = lit_Undef;
Clause& c = *confl;
if (p != lit_Undef)
reverse_binary_clause(c);
+
+ if (update && restartType == static_restart && c.learnt())
+ claBumpActivity(c);
for (uint j = (p == lit_Undef) ? 0 : 1; j != c.size(); j++) {
const Lit& q = c[j];
| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
|________________________________________________________________________________________________@*/
-struct reduceDB_lt {
- bool operator () (const Clause* x, const Clause* y) {
- const uint xsize = x->size();
- const uint ysize = y->size();
-
- // First criteria
- if (xsize > 2 && ysize == 2) return 1;
- if (ysize > 2 && xsize == 2) return 0;
-
- // Second criteria
- if (x->activity() > y->activity()) return 1;
- if (x->activity() < y->activity()) return 0;
-
- //return x->oldActivity() < y->oldActivity();
- return xsize > ysize;
- }
-};
+bool reduceDB_ltMiniSat::operator () (const Clause* x, const Clause* y) {
+ const uint xsize = x->size();
+ const uint ysize = y->size();
+
+ // First criteria
+ if (xsize > 2 && ysize == 2) return 1;
+ if (ysize > 2 && xsize == 2) return 0;
+
+ return x->oldActivity() < y->oldActivity();
+}
+
+bool reduceDB_ltGlucose::operator () (const Clause* x, const Clause* y) {
+ const uint xsize = x->size();
+ const uint ysize = y->size();
+
+ // First criteria
+ if (xsize > 2 && ysize == 2) return 1;
+ if (ysize > 2 && xsize == 2) return 0;
+
+ if (x->activity() > y->activity()) return 1;
+ if (x->activity() < y->activity()) return 0;
+ return xsize > ysize;
+}
void Solver::reduceDB()
{
uint32_t i, j;
nbReduceDB++;
- std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
+ if (lastSelectedRestartType == dynamic_restart)
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
+ else
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
#ifdef VERBOSE_DEBUG
std::cout << "Cleaning clauses" << endl;
const vec<Clause*>& Solver::get_sorted_learnts()
{
- std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
+ if (lastSelectedRestartType == dynamic_restart)
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
+ else
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
return learnts;
}
}
fprintf(outfile, "c clauses from learnts\n");
- std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
+
+ if (lastSelectedRestartType == dynamic_restart)
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
+ else
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
for (int i = learnts.size()-1; i >= 0 ; i--) {
if (learnts[i]->size() <= maxSize)
learnts[i]->plainPrint(outfile);
if (decisionLevel() == 0)
return l_False;
learnt_clause.clear();
- Clause* c = analyze(confl, learnt_clause, backtrack_level, nbLevels);
+ Clause* c = analyze(confl, learnt_clause, backtrack_level, nbLevels, update);
if (update) {
avgBranchDepth.push(decisionLevel());
if (restartType == dynamic_restart)
tmp = fixRestartType;
if (tmp == dynamic_restart) {
+ lastSelectedRestartType = dynamic_restart;
nbDecisionLevelHistory.fastclear();
nbDecisionLevelHistory.initSize(100);
if (verbosity >= 2)
printf("c | Decided on dynamic restart strategy |\n");
} else {
+ lastSelectedRestartType = static_restart;
if (verbosity >= 2)
printf("c | Decided on static restart strategy |\n");
{
if (fixRestartType != auto_restart) restartType = fixRestartType;
else restartType = static_restart;
+
if (restartType == dynamic_restart) {
nbDecisionLevelHistory.fastclear();
nbDecisionLevelHistory.initSize(100);
}
+
+ lastSelectedRestartType = restartType;
}
const lbool Solver::simplifyProblem(const uint32_t numConfls, const uint64_t numProps)
//=================================================================================================
// Solver -- the main class:
+struct reduceDB_ltMiniSat
+{
+ bool operator () (const Clause* x, const Clause* y);
+};
+
+struct reduceDB_ltGlucose
+{
+ bool operator () (const Clause* x, const Clause* y);
+};
+
class Solver
{
vec<Clause*> learnts; // List of learnt clauses.
vec<uint32_t> activity; // A heuristic measurement of the activity of a variable.
uint32_t var_inc; // Amount to bump next variable with.
+ double cla_inc; // Amount to bump learnt clause oldActivity with
vec<vec<Watched> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<vec<XorClausePtr> > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses.
vec<vec<WatchedBin> > binwatches;
bqueue<uint> avgBranchDepth; // Avg branch depth
MTRand mtrand; // random number generaton
RestartType restartType; // Used internally to determine which restart strategy to choose
+ RestartType lastSelectedRestartType; //the last selected restart type
friend class Logger;
#ifdef STATS_NEEDED
Logger logger; // dynamic logging, statistics
Clause* propagate (const bool update = true); // Perform unit propagation. Returns possibly conflicting clause.
Clause* propagate_xors (const Lit& p);
void cancelUntil (int level); // Backtrack until a certain level.
- Clause* analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, int &nblevels); // (bt = backtrack)
+ Clause* analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, int &nblevels, const bool update); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
lbool search (int nof_conflicts, int nof_conflicts_fullrestart, const bool update = true); // Search for a given number of conflicts.
// Maintaining Variable/Clause activity:
//
+ void claBumpActivity (Clause& c);
void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
order_heap.decrease(v);
}
+inline void Solver::claBumpActivity (Clause& c)
+{
+ if ( (c.oldActivity() += cla_inc) > 1e20 ) {
+ // Rescale:
+ for (uint32_t i = 0; i < learnts.size(); i++)
+ learnts[i]->oldActivity() *= 1e-17;
+ cla_inc *= 1e-20;
+ }
+}
+
+
inline bool Solver::enqueue (Lit p, Clause* from)
{
return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true);
projects / francis / stp.git / commitdiff