varToXor[a->var()].push_back(make_pair(*it, i));
}
}
+
+ const vector<Lit>& replaceTable = S->toReplace->getReplaceTable();
+ for (uint i = 0; i < replaceTable.size(); i++) {
+ if (replaceTable[i] != Lit(i, false)) {
+ blocked[i] = true;
+ blocked[replaceTable[i].var()] = true;
+ }
+ }
}
-void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vector<Lit>& vars) {
+void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vec<Lit>& vars) {
for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) {
if (a->var() != var) {
- vars.push_back(*a);
+ vars.push(*a);
varToXorMap::iterator finder = varToXor.find(a->var());
if (finder != varToXor.end()) {
vector<pair<XorClause*, uint> >::iterator it =
varToXorMap::iterator it = varToXor.begin();
const vector<pair<XorClause*, uint> >& c = it->second;
const uint& var = it->first;
+
+ //We blocked the var during dealWithNewClause (it was in a 2-long xor-clause)
+ if (blocked[var]) {
+ varToXor.erase(it);
+ continue;
+ }
+
S->setDecisionVar(var, false);
if (c.size() == 0) {
XorClause& x = *(c[0].first);
bool first_inverted = !x.xor_clause_inverted();
- vector<Lit> first_vars;
+ vec<Lit> first_vars;
process_clause(x, c[0].second, var, first_vars);
#ifdef VERBOSE_DEBUG
calcAtFinish.push(&x);
found++;
- vector<Lit> ps;
for (uint i = 1; i < c.size(); i++) {
- ps = first_vars;
+ vec<Lit> ps(first_vars.size());
+ memcpy(ps.getData(), first_vars.getData(), sizeof(Lit)*first_vars.size());
XorClause& x = *c[i].first;
process_clause(x, c[i].second, var, ps);
clearToRemove();
- S->toReplace->performReplace();
- if (S->ok == false) return found;
- S->ok = (S->propagate() == NULL);
+ if (S->ok != false)
+ S->ok = (S->propagate() == NULL);
return found;
}
-bool Conglomerate::dealWithNewClause(vector<Lit>& ps, const bool inverted, const uint old_group)
+bool Conglomerate::dealWithNewClause(vec<Lit>& ps, const bool inverted, const uint old_group)
{
switch(ps.size()) {
case 0: {
free(newX);
#endif
- S->toReplace->replace(ps[0].var(), Lit(ps[1].var(), !inverted));
+ S->toReplace->replace(ps, inverted, old_group);
+ blocked[ps[0].var()] = true;
+ blocked[ps[1].var()] = true;
break;
}
return true;
}
-void Conglomerate::clearDouble(vector<Lit>& ps) const
+void Conglomerate::clearDouble(vec<Lit>& ps) const
{
- std::sort(ps.begin(), ps.end());
+ std::sort(ps.getData(), ps.getData() + ps.size());
Lit p;
uint i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
} else //just add
ps[j++] = p = ps[i];
}
- ps.resize(ps.size()-(i - j));
+ ps.shrink(i - j);
}
void Conglomerate::clearToRemove()
private:
- void process_clause(XorClause& x, const uint num, uint var, vector<Lit>& vars);
+ void process_clause(XorClause& x, const uint num, uint var, vec<Lit>& vars);
void fillVarToXor();
- void clearDouble(vector<Lit>& ps) const;
+ void clearDouble(vec<Lit>& ps) const;
void clearToRemove();
- bool dealWithNewClause(vector<Lit>& ps, const bool inverted, const uint old_group);
+ bool dealWithNewClause(vec<Lit>& ps, const bool inverted, const uint old_group);
typedef map<uint, vector<pair<XorClause*, uint> > > varToXorMap;
varToXorMap varToXor;
&& numXorInMatrix[a].second <= 1000
&& realMatrixNum < 3)
{
- cout << "| Matrix no " << std::setw(4) << realMatrixNum;
+ if (S->verbosity >=1)
+ cout << "| Matrix no " << std::setw(4) << realMatrixNum;
S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, realMatrixNum, xorsInMatrix[i]));
realMatrixNum++;
} else {
- cout << "| Unused Matrix ";
+ if (S->verbosity >=1)
+ cout << "| Unused Matrix ";
+ }
+ if (S->verbosity >=1) {
+ cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size();
+ cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%";
+ cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg;
+ cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl;
}
- cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size();
- cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%";
- cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg;
- cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl;
}
return realMatrixNum;
#include "Conglomerate.h"
#include "XorFinder.h"
+//#define DEBUG_LIB
+
+#ifdef DEBUG_LIB
+#include <sstream>
+FILE* myoutputfile;
+static uint numcalled = 0;
+#endif //DEBUG_LIB
+
namespace MINISAT
{
using namespace MINISAT;
//=================================================================================================
// Constructor/Destructor:
-
Solver::Solver() :
// Parameters: (formerly in 'SearchParams')
var_decay(1 / 0.95), random_var_freq(0.02)
toReplace = new VarReplacer(this);
conglomerate = new Conglomerate(this);
logger.setSolver(this);
+
+ #ifdef DEBUG_LIB
+ std::stringstream ss;
+ ss << "inputfile" << numcalled << ".cnf";
+ myoutputfile = fopen(ss.str().c_str(), "w");
+ #endif
}
gauss_matrixes.clear();
delete toReplace;
delete conglomerate;
+
+ #ifdef DEBUG_LIB
+ fclose(myoutputfile);
+ #endif //DEBUG_LIB
}
//=================================================================================================
bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint group, char* group_name)
{
-
assert(decisionLevel() == 0);
+ #ifdef DEBUG_LIB
+ fprintf(myoutputfile, "x");
+ for (uint i = 0; i < ps.size(); i++) {
+ fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1);
+ }
+ fprintf(myoutputfile, "0\n");
+ #endif //DEBUG_LIB
if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name);
}
case 1: {
assert(value(ps[0]) == l_Undef);
- uncheckedEnqueue( (xor_clause_inverted) ? ~ps[0] : ps[0]);
+ uncheckedEnqueue(ps[0] ^ xor_clause_inverted);
if (dynamic_behaviour_analysis)
logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::add_clause_type, group);
return ok = (propagate() == NULL);
cout << "--> xor is 2-long, replacing var " << ps[0].var()+1 << " with " << (!xor_clause_inverted ? "-" : "") << ps[1].var()+1 << endl;
#endif
- learnt_clause_group = std::max(group+1, learnt_clause_group);
- toReplace->replace(ps[0].var(), Lit(ps[1].var(), !xor_clause_inverted));
+ toReplace->replace(ps, xor_clause_inverted, group);
break;
}
default: {
xorclauses.push(c);
xorclauses_tofree.push(c);
attachClause(*c);
+ toReplace->newClause();
break;
}
}
bool Solver::addClause(vec<Lit>& ps, const uint group, char* group_name)
{
assert(decisionLevel() == 0);
+
+ #ifdef DEBUG_LIB
+ for (int i = 0; i < ps.size(); i++) {
+ fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1);
+ }
+ fprintf(myoutputfile, "0\n");
+ #endif //DEBUG_LIB
if (dynamic_behaviour_analysis)
logger.set_group_name(group, group_name);
return ok = (propagate() == NULL);
} else {
learnt_clause_group = std::max(group+1, learnt_clause_group);
-
Clause* c = Clause_new(ps, group);
clauses.push(c);
attachClause(*c);
+ toReplace->newClause();
}
return true;
if (i-j > 0) useful++;
if (c.size() == 2) {
- vec<Lit> ps;
- ps.push(c[0]);
- ps.push(c[1]);
- addBinaryXorClause(ps, c.xor_clause_inverted(), c.group);
+ vec<Lit> ps(2);
+ ps[0] = c[0];
+ ps[1] = c[1];
+ toReplace->replace(ps, c.xor_clause_inverted(), c.group);
removeClause(c);
s++;
} else
lbool Solver::solve(const vec<Lit>& assumps)
{
+ #ifdef DEBUG_LIB
+ fprintf(myoutputfile, "c Solver::solve() called\n");
+ #endif
+
if (dynamic_behaviour_analysis)
logger.end(Logger::done_adding_clauses);
model.clear();
conflict.clear();
- curRestart = 1;
if (!ok) return l_False;
nbclausesbeforereduce = (nClauses() * learntsize_factor)/2;
}
- toReplace->performReplace();
- if (!ok) return l_False;
+ //toReplace->performReplace();
+ //if (!ok) return l_False;
if (xorFinder) {
double time;
XorFinder xorFinder(this, clauses);
uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10);
- printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
+ if (verbosity >=1)
+ printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
if (!ok) return l_False;
}
removeSatisfied(xorclauses);
cleanClauses(xorclauses);
uint foundCong = conglomerate->conglomerateXors();
- printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong);
+ if (verbosity >=1)
+ printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong);
if (!ok) return l_False;
uint new_total = 0;
for (uint i = 0; i < xorclauses.size(); i++) {
new_total += xorclauses[i]->size();
}
- printf("| Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls);
- printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total);
+ if (verbosity >=1) {
+ printf("| Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls);
+ printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total);
+ }
}
}
+ //toReplace->performReplace();
+ //if (!ok) return l_False;
+
if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) {
removeSatisfied(xorclauses);
cleanClauses(xorclauses);
double time = cpuTime();
MatrixFinder m(this);
const uint numMatrixes = m.findMatrixes();
- printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes);
+ if (verbosity >=1)
+ printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes);
}
-
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
printf("============================[ Search Statistics ]========================================\n");
// Solving:
//
- lbool simplify (); // Removes already satisfied clauses.
lbool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
lbool solve (); // Search without assumptions.
bool okay () const; // FALSE means solver is in a conflicting state
// Main internal methods:
//
+ lbool simplify (); // Removes already satisfied clauses.
//int nbPropagated (int level);
void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
Lit pickBranchLit (int polarity_mode); // Return the next decision variable.
bool satisfied (const XorClause& c) const; // Returns TRUE if the clause is satisfied in the current state
bool satisfied (const Clause& c) const; // Returns TRUE if the clause is satisfied in the current state.
void reverse_binary_clause(Clause& c) const; // Binary clauses --- the first Lit has to be true
- template<class T>
- inline void addBinaryXorClause(T& ps, const bool xor_clause_inverted, const uint group); //Adds Binary XOR clause as two normal clauses
// Misc:
//
c[0] = c[1], c[1] = tmp;
}
}
-template<class T>
-inline void Solver::addBinaryXorClause(T& ps, const bool xor_clause_inverted, const uint group) {
- Clause* c;
- ps[0] = ps[0].unsign();
- ps[1] = ps[1].unsign();
- ps[0] ^= xor_clause_inverted;
-
- c = Clause_new(ps, group, false);
- clauses.push(c);
- attachClause(*c);
-
- ps[0] ^= true;
- ps[1] ^= true;
- c = Clause_new(ps, group, false);
- clauses.push(c);
- attachClause(*c);
-}
inline void Solver::removeClause(Clause& c)
{
detachClause(c);
CryptoMiniSat
-SVN revision: r484
-GIT revision: 36a94d9b25be76b24dd26a413928a3ae559c3983
+SVN revision: r494
+GIT revision: eb7c71aaf2cea3bf064270d227cf7ddf27b852f2
VarReplacer::VarReplacer(Solver *_S) :
replacedLits(0)
, replacedVars(0)
+ , addedNewClause(false)
, S(_S)
{
}
}
#endif
- if (replacedVars == 0) return;
+ if (!addedNewClause || replacedVars == 0) return;
+
+ S->removeSatisfied(S->clauses);
+ S->removeSatisfied(S->xorclauses);
+ S->cleanClauses(S->clauses);
+ S->cleanClauses(S->xorclauses);
+ for (uint i = 0; i < toRemove.size(); i++)
+ S->removeClause(*toRemove[i]);
+ toRemove.clear();
replace_set(S->clauses);
replace_set(S->learnts);
replace_set(S->xorclauses, true);
replace_set(S->conglomerate->getCalcAtFinish(), false);
- printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits);
+ if (S->verbosity >=1)
+ printf("| Replacing %8d vars, replaced %8d lits |\n", replacedVars, replacedLits);
- replacedVars = 0;
replacedLits = 0;
+ addedNewClause = false;
if (S->ok)
S->ok = (S->propagate() == NULL);
c.shrink(i - j);
switch (c.size()) {
- case 0: {
+ case 0:
if (!c.xor_clause_inverted())
S->ok = false;
r++;
break;
- }
- case 1: {
+ case 1:
S->uncheckedEnqueue(Lit(c[0].var(), !c.xor_clause_inverted()));
r++;
break;
- }
- default: {
+ default:
if (c.size() == 2) {
- S->addBinaryXorClause(c, c.xor_clause_inverted(), c.group);
+ vec<Lit> ps(2);
+ ps[0] = c[0];
+ ps[1] = c[1];
+ addBinaryXorClause(ps, c.xor_clause_inverted(), c.group, true);
c.mark(1);
r++;
} else {
}
break;
}
- }
} else {
*a++ = *r++;
}
return replacedVars;
}
+const vector<Lit>& VarReplacer::getReplaceTable() const
+{
+ return table;
+}
+
const vector<Var> VarReplacer::getReplacingVars() const
{
vector<Var> replacingVars;
cout << endl;
#endif
- assert(S->assigns[i] == l_Undef);
assert(S->assigns[it->var()] != l_Undef);
-
- bool val = (S->assigns[it->var()] == l_False);
- S->uncheckedEnqueue(Lit(i, val ^ it->sign()));
+ if (S->assigns[i] == l_Undef) {
+ bool val = (S->assigns[it->var()] == l_False);
+ S->uncheckedEnqueue(Lit(i, val ^ it->sign()));
+ } else {
+ assert(S->assigns[i].getBool() == S->assigns[it->var()].getBool() ^ it->sign());
+ }
}
}
-void VarReplacer::replace(Var var, Lit lit)
+void VarReplacer::replace(vec<Lit>& ps, const bool xor_clause_inverted, const uint group)
{
+ addBinaryXorClause(ps, xor_clause_inverted, group);
+ Var var = ps[0].var();
+ Lit lit = Lit(ps[1].var(), !xor_clause_inverted);
assert(var != lit.var());
//Detect circle
S->setDecisionVar(var, false);
}
+void VarReplacer::addBinaryXorClause(vec<Lit>& ps, const bool xor_clause_inverted, const uint group, const bool internal)
+{
+ Clause* c;
+ ps[0] = ps[0].unsign();
+ ps[1] = ps[1].unsign();
+ ps[0] ^= xor_clause_inverted;
+
+ c = Clause_new(ps, group, false);
+ if (internal)
+ S->clauses.push(c);
+ else
+ toRemove.push(c);
+ S->attachClause(*c);
+
+ ps[0] ^= true;
+ ps[1] ^= true;
+ c = Clause_new(ps, group, false);
+ if (internal)
+ S->clauses.push(c);
+ else
+ toRemove.push(c);
+ S->attachClause(*c);
+}
+
bool VarReplacer::alreadyIn(const Var var, const Lit lit)
{
Lit lit2 = table[var];
{
table.push_back(Lit(table.size(), false));
}
+
+void VarReplacer::newClause()
+{
+ addedNewClause = true;
+}
};
{
public:
VarReplacer(Solver* S);
- void replace(const Var var, Lit lit);
+ void replace(vec<Lit>& ps, const bool xor_clause_inverted, const uint group);
void extendModel() const;
void performReplace();
const uint getNumReplacedLits() const;
const uint getNumReplacedVars() const;
const vector<Var> getReplacingVars() const;
+ const vector<Lit>& getReplaceTable() const;
+ void newClause();
void newVar();
private:
void replace_set(vec<Clause*>& set);
void replace_set(vec<XorClause*>& cs, const bool need_reattach);
bool handleUpdatedClause(Clause& c, const Lit origLit1, const Lit origLit2);
+ void addBinaryXorClause(vec<Lit>& ps, const bool xor_clause_inverted, const uint group, const bool internal = false);
void setAllThatPointsHereTo(const Var var, const Lit lit);
bool alreadyIn(const Var var, const Lit lit);
vector<Lit> table;
map<Var, vector<Var> > reverseTable;
+ vec<Clause*> toRemove;
uint replacedLits;
uint replacedVars;
+ bool addedNewClause;
Solver* S;
};
};
if (found > 0) {
clearToRemove();
- S->toReplace->performReplace();
- if (S->ok == false) return found;
- S->ok = (S->propagate() == NULL);
+ if (S->ok != false)
+ S->ok = (S->propagate() == NULL);
}
return found;
clearToRemove();
- S->toReplace->performReplace();
- if (S->ok == false) return found;
- S->ok = (S->propagate() == NULL);
+ if (S->ok != false)
+ S->ok = (S->propagate() == NULL);
#ifdef VERBOSE_DEBUG
cout << "Overdone work due to partitioning:" << (double)sumNumClauses/(double)cls.size() << "x" << endl;
ClauseTable::iterator begin = table.begin();
ClauseTable::iterator end = table.begin();
- vector<Lit> lits;
+ vec<Lit> lits;
bool impair;
while (getNextXor(begin, end, impair)) {
const Clause& c = *(begin->first);
lits.clear();
for (const Lit *it = &c[0], *cend = it+c.size() ; it != cend; it++) {
- lits.push_back(Lit(it->var(), false));
+ lits.push(Lit(it->var(), false));
}
uint old_group = c.group;
switch(lits.size()) {
case 2: {
- S->toReplace->replace(lits[0].var(), Lit(lits[1].var(), !impair));
+ S->toReplace->replace(lits, impair, old_group);
#ifdef VERBOSE_DEBUG
XorClause* x = XorClause_new(lits, impair, old_group);
projects / francis / stp.git / commitdiff