void Conglomerate::removeVar(const Var var)
{
- solver.setDecisionVar(var, false);
solver.activity[var] = 0.0;
solver.order_heap.update(var);
removedVars[var] = true;
+ if (solver.decision_var[var]) {
+ madeVarNonDecision.push(var);
+ solver.setDecisionVar(var, false);
+ }
found++;
}
solver.learnts.shrink(r-a);
}
-void Conglomerate::doCalcAtFinish()
+void Conglomerate::extendModel(Solver& solver2)
{
#ifdef VERBOSE_DEBUG
cout << "Executing doCalcAtFinish" << endl;
#endif
- vector<Var> toAssign;
- for (XorClause** it = calcAtFinish.getData() + calcAtFinish.size()-1; it != calcAtFinish.getData()-1; it--) {
- toAssign.clear();
- XorClause& c = **it;
+ vec<Lit> ps;
+ for (int i = (int)(calcAtFinish.size())-1; i >= 0; i--) {
+ XorClause& c = *calcAtFinish[i];
assert(c.size() > 2);
- #ifdef VERBOSE_DEBUG
- cout << "doCalcFinish for xor-clause:";
- c.plainPrint();
- #endif
-
- bool final = c.xor_clause_inverted();
- for (int k = 0, size = c.size(); k < size; k++ ) {
- const lbool& val = solver.assigns[c[k].var()];
- if (val == l_Undef)
- toAssign.push_back(c[k].var());
- else
- final ^= val.getBool();
- }
- #ifdef VERBOSE_DEBUG
- if (toAssign.size() == 0) {
- cout << "ERROR: toAssign.size() == 0 !!" << endl;
- for (int k = 0, size = c.size(); k < size; k++ ) {
- cout << "Var: " << c[k].var() + 1 << " Level: " << solver.level[c[k].var()] << endl;
- }
- }
- if (toAssign.size() > 1) {
- cout << "Double assign!" << endl;
- for (uint i = 1; i < toAssign.size(); i++) {
- cout << "-> extra Var " << toAssign[i]+1 << endl;
- }
+ ps.clear();
+ for (Lit *l = c.getData(), *end = c.getDataEnd(); l != end; l++) {
+ ps.push(l->unsign());
}
- #endif
- assert(toAssign.size() > 0);
- for (uint i = 1; i < toAssign.size(); i++) {
- solver.uncheckedEnqueue(Lit(toAssign[i], true), &c);
- }
- solver.uncheckedEnqueue(Lit(toAssign[0], final), &c);
- assert(solver.clauseCleaner->satisfied(c));
+ solver2.addXorClause(ps, c.xor_clause_inverted(), c.getGroup());
+ assert(solver2.ok);
}
}
cout << "Executing addRemovedClauses" << endl;
#endif
- char tmp[100];
- tmp[0] = '\0';
- vec<Lit> ps;
for(uint i = 0; i < calcAtFinish.size(); i++)
{
XorClause& c = *calcAtFinish[i];
c.plainPrint();
#endif
- ps.clear();
- for(uint i2 = 0; i2 != c.size() ; i2++) {
- ps.push(Lit(c[i2].var(), false));
- }
- if (!solver.addXorClause(ps, c.xor_clause_inverted(), c.getGroup(), tmp))
+ for(Lit *l = c.getData(), *end = c.getDataEnd(); l != end ; l++)
+ *l = l->unsign();
+
+ if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup()))
return false;
free(&c);
}
calcAtFinish.clear();
- for (uint i = 0; i < removedVars.size(); i++) {
- if (removedVars[i]) {
- removedVars[i] = false;
- solver.setDecisionVar(i, true);
- #ifdef VERBOSE_DEBUG
- std::cout << "Inserting Var " << i+1 << " back into the order_heap" << std::endl;
- #endif //VERBOSE_DEBUG
- }
+
+ std::fill(removedVars.getData(), removedVars.getDataEnd(), false);
+ for (Var *v = madeVarNonDecision.getData(), *end = madeVarNonDecision.getDataEnd(); v != end; v++) {
+ solver.setDecisionVar(*v, true);
}
+ madeVarNonDecision.clear();
return true;
}
-void Conglomerate::newVar()
-{
- removedVars.resize(removedVars.size()+1, false);
-}
-
}; //NAMESPACE MINISAT
const bool conglomerateXorsFull();
const bool heuleProcessFull();
const bool addRemovedClauses(); ///<Add clauses that have been removed. Used if solve() is called multiple times
- void doCalcAtFinish(); ///<Calculate variables removed during conglomeration
+ void extendModel(Solver& solver2); ///<Calculate variables removed during conglomeration
const vec<XorClause*>& getCalcAtFinish() const;
vec<XorClause*>& getCalcAtFinish();
- const vector<bool>& getRemovedVars() const;
+ const vec<bool>& getRemovedVars() const;
+ const bool needCalcAtFinish() const;
void newVar();
varToXorMap varToXor;
vector<bool> blocked;
vector<bool> toRemove;
- vector<bool> removedVars;
+
+ vec<bool> removedVars;
+ vec<Var> madeVarNonDecision;
vec<XorClause*> calcAtFinish;
uint found;
Solver& solver;
};
-inline const vector<bool>& Conglomerate::getRemovedVars() const
+inline void Conglomerate::newVar()
+{
+ removedVars.push(false);
+}
+
+inline const vec<bool>& Conglomerate::getRemovedVars() const
{
return removedVars;
}
return calcAtFinish;
}
+inline const bool Conglomerate::needCalcAtFinish() const
+{
+ return calcAtFinish.size();
+}
+
}; //NAMESPACE MINISAT
#endif //CONGLOMERATE_H
//Saving Solver state
Heap<Solver::VarOrderLt> backup_order_heap(solver.order_heap);
vector<bool> backup_polarities = solver.polarity;
- vec<double> backup_activity;
- backup_activity.growTo(solver.activity.size());
+ vec<uint32_t> backup_activity(solver.activity.size());
std::copy(solver.activity.getData(), solver.activity.getDataEnd(), backup_activity.getData());
- double backup_var_inc = solver.var_inc;
+ uint32_t backup_var_inc = solver.var_inc;
uint32_t origHeapSize = solver.order_heap.size();
//General Stats
Solver newSolver;
newSolver.mtrand.seed(solver.mtrand.randInt());
newSolver.random_var_freq = solver.random_var_freq;
- newSolver.var_decay = solver.var_decay;
newSolver.verbosity = solver.verbosity;
newSolver.restrictedPickBranch = solver.restrictedPickBranch;
newSolver.greedyUnbound = solver.greedyUnbound;
Solver::Solver() :
// Parameters: (formerly in 'SearchParams')
- var_decay(1 / 0.95), random_var_freq(0.02)
+ random_var_freq(0.02)
, restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1)
// More parameters:
, ok (true)
- , var_inc (1)
+ , var_inc (128)
, curRestart (1)
, nbclausesbeforereduce (NBCLAUSESBEFOREREDUCE)
template<class T>
XorClause* Solver::addXorClauseInt(T& ps, bool xor_clause_inverted, const uint32_t group)
{
+ if (ps.size() > (0x01UL << 18)) {
+ std::cout << "Too long clause!" << std::endl;
+ exit(-1);
+ }
std::sort(ps.getData(), ps.getData()+ps.size());
Lit p;
uint32_t i, j;
Heap<VarOrderLt> backup_order_heap(order_heap);
vector<bool> backup_polarities = polarity;
RestartType backup_restartType= restartType;
- double backup_random_var_freq = random_var_freq;
- vec<double> backup_activity;
- backup_activity.growTo(activity.size());
+ uint32_t backup_random_var_freq = random_var_freq;
+ vec<uint32_t> backup_activity(activity.size());
std::copy(activity.getData(), activity.getDataEnd(), backup_activity.getData());
- double backup_var_inc = var_inc;
+ uint32_t backup_var_inc = var_inc;
if (verbosity >= 2)
std::cout << "c | " << std::setw(24) << " "
//checkSolution();
#endif
- if (subsumer->getNumElimed() > 0) {
+ if (subsumer->getNumElimed() > 0 || conglomerate->needCalcAtFinish()) {
Solver s;
s.doSubsumption = false;
s.performReplace = false;
s.conglomerateXors = false;
s.greedyUnbound = greedyUnbound;
for (Var var = 0; var < nVars(); var++) {
- s.newVar(decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var));
+ s.newVar(decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var) || conglomerate->getRemovedVars()[var]);
+
assert(!(conglomerate->getRemovedVars()[var] && (decision_var[var] || subsumer->getVarElimed()[var] || varReplacer->varHasBeenReplaced(var))));
+
if (value(var) != l_Undef) {
assert(!conglomerate->getRemovedVars()[var]);
vec<Lit> tmp;
}
varReplacer->extendModelImpossible(s);
subsumer->extendModel(s);
+ conglomerate->extendModel(s);
status = s.solve();
- assert(status == l_True);
+ if (status != l_True) {
+ printf("c ERROR! Extension of model failed!\n");
+ assert(status == l_True);
+ exit(-1);
+ }
for (Var var = 0; var < nVars(); var++) {
if (assigns[var] == l_Undef && s.model[var] != l_Undef) uncheckedEnqueue(Lit(var, s.model[var] == l_False));
}
}
- conglomerate->doCalcAtFinish();
- // Extend & copy model:
#ifndef NDEBUG
//checkSolution();
#endif
+ //Copy model:
model.growTo(nVars());
for (Var var = 0; var != nVars(); var++) model[var] = value(var);
#include <cstdio>
#include <string.h>
#include <stdio.h>
-
#ifdef _MSC_VER
#include <msvc/stdint.h>
#else
// Mode of operation:
//
- double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95)
double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02)
int restart_first; // The initial restart limit. (default 100)
double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
// Helper structures:
//
struct VarOrderLt {
- const vec<double>& activity;
+ const vec<uint32_t>& activity;
bool operator () (Var x, Var y) const {
return activity[x] > activity[y];
}
- VarOrderLt(const vec<double>& act) : activity(act) { }
+ VarOrderLt(const vec<uint32_t>& act) : activity(act) { }
};
friend class VarFilter;
vec<Clause*> binaryClauses; // Binary clauses are regularly moved here
vec<XorClause*> xorclauses; // List of problem xor-clauses. Will be freed
vec<Clause*> learnts; // List of learnt clauses.
- vec<double> activity; // A heuristic measurement of the activity of a variable.
- double var_inc; // Amount to bump next variable with.
+ vec<uint32_t> activity; // A heuristic measurement of the activity of a variable.
+ uint32_t var_inc; // Amount to bump next variable 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;
inline void Solver::varDecayActivity()
{
- var_inc *= var_decay;
+ var_inc *= 11;
+ var_inc /= 10;
}
inline void Solver::varBumpActivity(Var v)
{
- if ( (activity[v] += var_inc) > 1e100 ) {
+ if ( (activity[v] += var_inc) > (0x1U) << 24 ) {
//printf("RESCALE!!!!!!\n");
//std::cout << "var_inc: " << var_inc << std::endl;
// Rescale:
for (Var var = 0; var != nVars(); var++) {
- activity[var] *= 1e-95;
+ activity[var] >>= 14;
}
- var_inc *= 1e-100;
+ var_inc >>= 14;
//var_inc = 1;
//std::cout << "var_inc: " << var_inc << std::endl;
cannot_eliminate[c[i2].var()] = true;
}
- const vector<bool>& tmp2 = solver.conglomerate->getRemovedVars();
+ const vec<bool>& tmp2 = solver.conglomerate->getRemovedVars();
for (uint32_t i = 0; i < tmp2.size(); i++) {
if (tmp2[i]) cannot_eliminate[i] = true;
}
CryptoMiniSat
-GIT revision: fb3f0713d5864d50cae28535b577fb74fd65899c
-
+GIT revision: 3c04fa48505107a294986a85131b05a67c479ba1
#endif
Var var = 0;
- const vector<bool>& removedVars = solver.conglomerate->getRemovedVars();
+ const vec<bool>& removedVars = solver.conglomerate->getRemovedVars();
const vec<lbool>& removedVars2 = solver.partHandler->getSavedState();
const vec<char>& removedVars3 = solver.subsumer->getVarElimed();
for (vector<Lit>::const_iterator it = table.begin(); it != table.end(); it++, var++) {
solver.setDecisionVar(var, false);
solver.setDecisionVar(it->var(), true);
- double& activity1 = solver.activity[var];
- double& activity2 = solver.activity[it->var()];
+ uint32_t& activity1 = solver.activity[var];
+ uint32_t& activity2 = solver.activity[it->var()];
if (wasDecisionVar && activity1 > activity2) {
activity2 = activity1;
solver.order_heap.update(it->var());
projects / francis / stp.git / commitdiff