bm->CreateNode(NOT, query));
//solver instantiated here
-#if defined CORE || defined CRYPTOMINISAT
+#if defined CORE || defined CRYPTOMINISAT || defined CRYPTOMINISAT2
MINISAT::Solver NewSolver;
#endif
#if defined CRYPTOMINISAT2
- MINISAT::Solver NewSolver;
if(bm->UserFlags.print_cnf_flag)
{
NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename);
}
- NewSolver.dynamicRestarts = false;
#endif
#ifdef SIMP
}
}
-void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type)
+void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type, const uint limit)
{
#ifdef DEBUG_CLEAN
assert(solver.decisionLevel() == 0);
#endif
- if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num())
+ if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num())
return;
int i,j;
lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
}
-void ClauseCleaner::removeSatisfied(vec<Clause*>& cs, ClauseSetType type)
+void ClauseCleaner::removeSatisfied(vec<Clause*>& cs, ClauseSetType type, const uint limit)
{
#ifdef DEBUG_CLEAN
assert(solver.decisionLevel() == 0);
#endif
- if (lastNumUnitarySat[type] == solver.get_unitary_learnts_num())
+ if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num())
return;
int i,j;
lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
}
-bool ClauseCleaner::cleanClause(Clause& c)
+inline const bool ClauseCleaner::cleanClause(Clause& c)
{
- assert(c.size() >= 2);
- Lit first = c[0];
- Lit second = c[1];
+ Lit origLit1 = c[0];
+ Lit origLit2 = c[1];
+ uint32_t origSize = c.size();
Lit *i, *j, *end;
- uint at = 0;
- for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
- if (solver.value(*i) == l_Undef) {
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ lbool val = solver.value(*i);
+ if (val == l_Undef) {
*j = *i;
j++;
- } else assert(at > 1);
- assert(solver.value(*i) != l_True);
+ }
+ if (val == l_True) {
+ solver.detachModifiedClause(origLit1, origLit2, origSize, &c);
+ return true;
+ }
}
+
if ((c.size() > 2) && (c.size() - (i-j) == 2)) {
- solver.detachModifiedClause(first, second, c.size(), &c);
+ solver.detachModifiedClause(origLit1, origLit2, c.size(), &c);
c.shrink(i-j);
solver.attachClause(c);
} else
c.shrink(i-j);
- assert(c.size() > 1);
-
- return (i-j > 0);
+ return false;
}
-void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type)
+void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type, const uint limit)
{
#ifdef DEBUG_CLEAN
assert(solver.decisionLevel() == 0);
#endif
- if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num())
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
return;
- uint useful = 0;
- for (int s = 0; s < cs.size(); s++)
- useful += cleanClause(*cs[s]);
+ Clause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end;) {
+ if (cleanClause(**s)) {
+ free(*s);
+ s++;
+ } else {
+ *ss++ = *s++;
+ }
+ }
+ cs.shrink(s-ss);
lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
#ifdef VERBOSE_DEBUG
- cout << "cleanClauses(Clause) useful:" << useful << endl;
+ cout << "cleanClauses(Clause) useful ?? Removed: " << s-ss << endl;
#endif
}
-void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type)
+void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type, const uint limit)
{
#ifdef DEBUG_CLEAN
assert(solver.decisionLevel() == 0);
#endif
- if (lastNumUnitaryClean[type] == solver.get_unitary_learnts_num())
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
return;
- uint useful = 0;
XorClause **s, **ss, **end;
for (s = ss = cs.getData(), end = s + cs.size(); s != end;) {
- XorClause& c = **s;
- #ifdef VERBOSE_DEBUG
- std::cout << "Cleaning clause:";
- c.plain_print();
- solver.printClause(c);std::cout << std::endl;
- #endif
-
- Lit *i, *j, *end;
- uint at = 0;
- for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
- const lbool& val = solver.assigns[i->var()];
- if (val.isUndef()) {
- *j = *i;
- j++;
- } else /*assert(at>1),*/ c.invert(val.getBool());
- }
- c.shrink(i-j);
- if (i-j > 0) useful++;
-
- if (c.size() == 2) {
- vec<Lit> ps(2);
- ps[0] = c[0].unsign();
- ps[1] = c[1].unsign();
- solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.group);
- solver.removeClause(c);
+ if (cleanClause(**s)) {
+ (**s).mark(1);
+ solver.freeLater.push(*s);
s++;
- } else
+ } else {
*ss++ = *s++;
-
- #ifdef VERBOSE_DEBUG
- std::cout << "Cleaned clause:";
- c.plain_print();
- solver.printClause(c);std::cout << std::endl;
- #endif
- assert(c.size() > 1);
+ }
}
cs.shrink(s-ss);
lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
#ifdef VERBOSE_DEBUG
- cout << "cleanClauses(XorClause) useful:" << useful << endl;
+ cout << "cleanClauses(XorClause) useful: ?? Removed: " << s-ss << endl;
#endif
}
+inline const bool ClauseCleaner::cleanClause(XorClause& c)
+{
+ Lit *i, *j, *end;
+ Var origVar1 = c[0].var();
+ Var origVar2 = c[1].var();
+ uint32_t origSize = c.size();
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ const lbool& val = solver.assigns[i->var()];
+ if (val.isUndef()) {
+ *j = *i;
+ j++;
+ } else c.invert(val.getBool());
+ }
+ c.shrink(i-j);
+
+ switch (c.size()) {
+ case 0: {
+ solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
+ return true;
+ }
+ case 2: {
+ vec<Lit> ps(2);
+ ps[0] = c[0].unsign();
+ ps[1] = c[1].unsign();
+ solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.group);
+ solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
+ return true;
+ }
+ default:
+ return false;
+ }
+}
+
bool ClauseCleaner::satisfied(const Clause& c) const
{
for (uint i = 0; i < c.size(); i++)
enum ClauseSetType {clauses, xorclauses, learnts, conglomerate};
- void cleanClauses(vec<Clause*>& cs, ClauseSetType type);
- void cleanClauses(vec<XorClause*>& cs, ClauseSetType type);
- void removeSatisfied(vec<Clause*>& cs, ClauseSetType type);
- void removeSatisfied(vec<XorClause*>& cs, ClauseSetType type);
+ void cleanClauses(vec<Clause*>& cs, ClauseSetType type, const uint limit = 0);
+ void cleanClauses(vec<XorClause*>& cs, ClauseSetType type, const uint limit = 0);
+ void removeSatisfied(vec<Clause*>& cs, ClauseSetType type, const uint limit = 0);
+ void removeSatisfied(vec<XorClause*>& cs, ClauseSetType type, const uint limit = 0);
+ void removeAndCleanAll();
bool satisfied(const Clause& c) const;
bool satisfied(const XorClause& c) const;
private:
- bool cleanClause(Clause& c);
+ const bool cleanClause(Clause& c);
+ const bool cleanClause(XorClause& c);
uint lastNumUnitarySat[4];
uint lastNumUnitaryClean[4];
Solver& solver;
};
-};
+inline void ClauseCleaner::removeAndCleanAll()
+{
+ uint limit = (double)solver.order_heap.size() * PERCENTAGEPERFORMREPLACE;
+
+ cleanClauses(solver.clauses, ClauseCleaner::clauses, limit);
+ cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses, limit);
+ cleanClauses(solver.learnts, ClauseCleaner::learnts, limit);
+}
+
+};
#endif //CLAUSECLEANER_H
cout << "Finding conglomerate xors started" << endl;
#endif
- S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
toRemove.clear();
llbool Gaussian::full_init()
{
if (!should_init()) return l_Nothing;
+ reset_stats();
bool do_again_gauss = true;
while (do_again_gauss) {
do_again_gauss = false;
- solver.clauseCleaner->removeSatisfied(solver.xorclauses, ClauseCleaner::xorclauses);
solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
init();
Clause* confl;
//statistics
void print_stats() const;
- void reset_stats();
void print_matrix_stats() const;
const uint get_called() const;
const uint get_useful_prop() const;
bool should_init() const;
bool should_check_gauss(const uint decisionlevel, const uint starts) const;
void disable_if_necessary();
+ void reset_stats();
private:
MTL = mtl
MTRAND = MTRand
-SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp ClauseCleaner.cpp
+SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp ClauseCleaner.cpp RestartTypeChooser.cpp
OBJECTS = $(SOURCES:.cpp=.o)
LIB = libminisat.a
CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
if (S->xorclauses.size() == 0)
return 0;
- S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) {
realMatrixNum++;
} else {
- if (S->verbosity >=1)
+ if (S->verbosity >=1 && numXorInMatrix[a].second >= 20)
cout << "| Unused Matrix ";
}
- if (S->verbosity >=1) {
+ if (S->verbosity >=1 && numXorInMatrix[a].second >= 20) {
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;
--- /dev/null
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "RestartTypeChooser.h"
+#include "Solver.h"
+
+//#define VERBOSE_DEBUG
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+RestartTypeChooser::RestartTypeChooser(const Solver* const _S) :
+ S(_S)
+ , topX(100)
+ , limit(40)
+{
+}
+
+const RestartType RestartTypeChooser::choose()
+{
+ firstVarsOld = firstVars;
+ calcHeap();
+ uint sameIn = 0;
+ if (!firstVarsOld.empty()) {
+ for (uint i = 0; i < 100; i++) {
+ if (std::find(firstVars.begin(), firstVars.end(), firstVarsOld[i]) != firstVars.end())
+ sameIn++;
+ }
+ #ifdef VERBOSE_DEBUG
+ std::cout << " Same vars in first&second first 100: " << sameIn << std::endl;
+ #endif
+ sameIns.push_back(sameIn);
+ } else
+ return static_restart;
+
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Avg same vars in first&second first 100: " << avg() << std::endl;
+ #endif
+
+ if (avg() > (double)limit)
+ return static_restart;
+ else
+ return dynamic_restart;
+}
+
+const double RestartTypeChooser::avg() const
+{
+ double sum = 0.0;
+ for (uint i = 0; i != sameIns.size(); i++)
+ sum += sameIns[i];
+ return (sum/(double)sameIns.size());
+}
+
+void RestartTypeChooser::calcHeap()
+{
+ firstVars.resize(100);
+ #ifdef VERBOSE_DEBUG
+ std::cout << "First vars:" << std::endl;
+ #endif
+ Heap<Solver::VarOrderLt> tmp(S->order_heap);
+ for (uint i = 0; i != 100; i++) {
+ #ifdef VERBOSE_DEBUG
+ std::cout << tmp.removeMin()+1 << ", ";
+ #endif
+ firstVars[i] = tmp.removeMin();
+ }
+ #ifdef VERBOSE_DEBUG
+ std::cout << std::endl;
+ #endif
+}
+
+};
--- /dev/null
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef RESTARTTYPECHOOSER_H
+#define RESTARTTYPECHOOSER_H
+
+#include "SolverTypes.h"
+#include <vector>
+#include <sys/types.h>
+using std::vector;
+
+namespace MINISAT
+{
+
+class Solver;
+
+class RestartTypeChooser
+{
+ public:
+ RestartTypeChooser(const Solver* const S);
+ const RestartType choose();
+
+ private:
+ void calcHeap();
+ const double avg() const;
+
+ const Solver* const S;
+ const uint topX;
+ const uint limit;
+ vector<Var> sameIns;
+
+ vector<Var> firstVars, firstVarsOld;
+};
+
+};
+
+#endif //RESTARTTYPECHOOSER_H
#include "Conglomerate.h"
#include "XorFinder.h"
#include "ClauseCleaner.h"
+#include "RestartTypeChooser.h"
namespace MINISAT
{
, polarity_mode (polarity_user)
, verbosity (0)
, restrictedPickBranch(0)
- , useRealUnknowns (false)
, xorFinder (true)
, performReplace (true)
, greedyUnbound (false)
- , dynamicRestarts (false)
+ , restartType (static_restart)
// Statistics: (formerly in 'SolverStats')
//
for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]);
- for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i];
+ clearGaussMatrixes();
for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]);
delete varReplacer;
delete conglomerate;
p = lit_Undef;
if (!assigns[ps[i].var()].isUndef())
xor_clause_inverted ^= assigns[ps[i].var()].getBool();
- } else if (value(ps[i]) == l_Undef) //just add
+ } else if (assigns[ps[i].var()].isUndef()) //just add
ps[j++] = p = ps[i];
- else xor_clause_inverted ^= (value(ps[i]) == l_True); //modify xor_clause_inverted instead of adding
+ else //modify xor_clause_inverted instead of adding
+ xor_clause_inverted ^= (assigns[ps[i].var()].getBool());
}
ps.shrink(i - j);
return ok = false;
}
case 1: {
- assert(value(ps[0]) == l_Undef);
+ assert(assigns[ps[0].var()].isUndef());
uncheckedEnqueue(ps[0] ^ xor_clause_inverted);
if (dynamic_behaviour_analysis)
logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::add_clause_type, group);
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- if (value(ps[i]) == l_True || ps[i] == ~p)
+ if (value(ps[i]).getBool() || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
#endif
}
-void Solver::setRealUnknown(const uint var)
-{
- if (realUnknowns.size() < var+1)
- realUnknowns.resize(var+1, false);
- realUnknowns[var] = true;
-}
-
void Solver::printLit(const Lit l) const
{
printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
gaussconfig.decision_until = to;
}
+void Solver::clearGaussMatrixes()
+{
+ for (uint i = 0; i < gauss_matrixes.size(); i++)
+ delete gauss_matrixes[i];
+ gauss_matrixes.clear();
+}
+
//=================================================================================================
// Major methods:
const uint my_var = q.var();
if (!seen[my_var] && level[my_var] > 0) {
- if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var]))
- varBumpActivity(my_var);
+ varBumpActivity(my_var);
seen[my_var] = 1;
if (level[my_var] >= decisionLevel()) {
pathC++;
cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel: " << trail.size() << endl;
#endif
- assert(value(p) == l_Undef);
+ assert(assigns[p.var()].isUndef());
const Var v = p.var();
assigns [v] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient
level [v] = decisionLevel();
for(WatchedBin *k = wbin.getData(), *end = k + wbin.size(); k != end; k++) {
Lit imp = k->impliedLit;
lbool val = value(imp);
- if (val == l_False)
- return k->clause;
- if (val == l_Undef) {
+ if (val.isUndef()) {
uncheckedEnqueue(imp, k->clause);
if (dynamic_behaviour_analysis)
logger.propagation(imp, Logger::simple_propagation_type, k->clause->group);
- }
+ } else if (val == l_False)
+ return k->clause;
}
//Next, propagate normal clauses
*j++ = &c;
} else {
// Look for new watch:
- for (uint k = 2; k != c.size(); k++)
+ for (int k = 2; k != c.size(); k++)
if (value(c[k]) != l_False) {
c[1] = c[k];
c[k] = false_lit;
{
// Reached bound on number of conflicts?
- if (dynamicRestarts) {
+ switch (restartType) {
+ case dynamic_restart:
if (nbDecisionLevelHistory.isvalid() &&
((nbDecisionLevelHistory.getavg()*0.7) > (totalSumOfDecisionLevel / conf4Stats))) {
nbDecisionLevelHistory.fastclear();
}
return l_Undef;
}
- } else {
+ break;
+ case static_restart:
if (nof_conflicts >= 0 && conflictC >= nof_conflicts) {
progress_estimate = progressEstimate();
cancelUntil(0);
logger.end(Logger::restarting);
return l_Undef;
}
+ break;
}
// Simplify the set of problem clauses:
learnt_clause.clear();
analyze(confl, learnt_clause, backtrack_level, nbLevels);
conf4Stats++;
- if (dynamicRestarts) {
+ if (restartType == dynamic_restart) {
nbDecisionLevelHistory.push(nbLevels);
totalSumOfDecisionLevel += nbLevels;
}
}
}
-lbool Solver::solve(const vec<Lit>& assumps)
+inline void Solver::chooseRestartType(const lbool& status, RestartTypeChooser& restartTypeChooser)
{
- if (libraryCNFFile)
- fprintf(libraryCNFFile, "c Solver::solve() called\n");
-
- model.clear();
- conflict.clear();
- if (dynamicRestarts) {
- nbDecisionLevelHistory.fastclear();
- nbDecisionLevelHistory.initSize(100);
- totalSumOfDecisionLevel = 0;
+ if (status.isUndef() && starts > 2 && starts < 8) {
+ RestartType tmp = restartTypeChooser.choose();
+ if (starts == 7) {
+ if (tmp == dynamic_restart) {
+ nbDecisionLevelHistory.fastclear();
+ nbDecisionLevelHistory.initSize(100);
+ totalSumOfDecisionLevel = 0;
+ clearGaussMatrixes();
+ if (verbosity >= 1)
+ printf("| Decided on dynamic restart strategy |\n");
+ } else {
+ if (verbosity >= 1)
+ printf("| Decided on static restart strategy |\n");
+ }
+ restartType = tmp;
+ }
+ } else {
+ #ifdef VERBOSE_DEBUG
+ restartTypeChooser.choose();
+ #endif
}
+}
- if (!ok) return l_False;
-
- assumps.copyTo(assumptions);
-
- double nof_conflicts = restart_first;
- lbool status = l_Undef;
-
- if (nClauses() * learntsize_factor < nbclausesbeforereduce) {
- if (nClauses() * learntsize_factor < nbclausesbeforereduce/2)
- nbclausesbeforereduce = nbclausesbeforereduce/4;
- else
- nbclausesbeforereduce = (nClauses() * learntsize_factor)/2;
- }
-
- conglomerate->addRemovedClauses();
-
- if (performReplace) {
+inline void Solver::performStepsBeforeSolve()
+{
+ if (performReplace
+ && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) {
varReplacer->performReplace();
- if (!ok) return l_False;
+ if (!ok) return;
}
-
+
if (xorFinder) {
double time;
if (clauses.size() < 400000) {
time = cpuTime();
- clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses);
- clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses);
uint sumLengths = 0;
XorFinder xorFinder(this, clauses);
uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10);
- if (!ok) return l_False;
+ if (!ok) return;
if (verbosity >=1)
printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
- if (performReplace) {
+ if (performReplace
+ && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) {
varReplacer->performReplace();
- if (!ok) return l_False;
+ if (!ok) return;
}
}
uint foundCong = conglomerate->conglomerateXors();
if (verbosity >=1)
printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong);
- if (!ok) return l_False;
+ if (!ok) return;
uint new_total = 0;
uint new_num_cls = xorclauses.size();
printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total);
}
- if (performReplace) {
+ if (performReplace
+ && ((double)varReplacer->getNewToReplaceVars()/(double)order_heap.size()) > PERCENTAGEPERFORMREPLACE) {
varReplacer->performReplace();
- if (!ok) return l_False;
+ if (!ok) return;
}
}
}
if (verbosity >=1)
printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes);
}
+}
+
+lbool Solver::solve(const vec<Lit>& assumps)
+{
+ if (libraryCNFFile)
+ fprintf(libraryCNFFile, "c Solver::solve() called\n");
+
+ model.clear();
+ conflict.clear();
+ clearGaussMatrixes();
+ restartType = static_restart;
+ conglomerate->addRemovedClauses();
+ starts = 0;
+
+ if (!ok) return l_False;
+
+ assumps.copyTo(assumptions);
+
+ double nof_conflicts = restart_first;
+ lbool status = l_Undef;
+
+ if (nClauses() * learntsize_factor < nbclausesbeforereduce) {
+ if (nClauses() * learntsize_factor < nbclausesbeforereduce/2)
+ nbclausesbeforereduce = nbclausesbeforereduce/4;
+ else
+ nbclausesbeforereduce = (nClauses() * learntsize_factor)/2;
+ }
+
+ performStepsBeforeSolve();
+ if (!ok) return l_False;
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
if (dynamic_behaviour_analysis)
logger.end(Logger::done_adding_clauses);
-
+
+ RestartTypeChooser restartTypeChooser(this);
+
// Search:
while (status == l_Undef && starts < maxRestarts) {
- clauseCleaner->removeSatisfied(clauses, ClauseCleaner::clauses);
- clauseCleaner->removeSatisfied(xorclauses, ClauseCleaner::xorclauses);
- clauseCleaner->removeSatisfied(learnts, ClauseCleaner::learnts);
-
- clauseCleaner->cleanClauses(clauses, ClauseCleaner::clauses);
- clauseCleaner->cleanClauses(xorclauses, ClauseCleaner::xorclauses);
- clauseCleaner->cleanClauses(learnts, ClauseCleaner::learnts);
+ clauseCleaner->removeAndCleanAll();
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nbclausesbeforereduce*curRestart, nLearnts(), (double)learnts_literals/nLearnts());
print_gauss_sum_stats();
}
- for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
- (*gauss)->reset_stats();
if (dynamic_behaviour_analysis)
logger.begin();
status = search((int)nof_conflicts);
nof_conflicts *= restart_inc;
+
+ chooseRestartType(status, restartTypeChooser);
}
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
}
}
+
};
#include "Logger.h"
#include "constants.h"
#include "BoundedQueue.h"
+#include "RestartTypeChooser.h"
#ifdef _MSC_VER
#include <ctime>
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
void setSeed (const uint32_t seed); // Sets the seed to be the given number
- void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown
- void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on)
void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value
void set_gaussian_decision_until(const uint to);
template<class T>
int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false)
int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0)
Var restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all])
- bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true
- vector<bool> realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable
bool xorFinder; // Automatically find xor-clauses and convert them
bool performReplace; // Should var-replacing be performed?
friend class FindUndef;
bool greedyUnbound; //If set, then variables will be greedily unbounded (set to l_Undef)
- bool dynamicRestarts; // If set to true, the restart strategy will be dynamic
+ RestartType restartType; // If set to true, the restart strategy will be dynamic
enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 };
vector<Gaussian*> gauss_matrixes;
GaussianConfig gaussconfig;
void print_gauss_sum_stats() const;
+ void clearGaussMatrixes();
friend class Gaussian;
friend class MatrixFinder;
friend class VarReplacer;
friend class ClauseCleaner;
+ friend class RestartTypeChooser;
Conglomerate* conglomerate;
VarReplacer* varReplacer;
ClauseCleaner* clauseCleaner;
+ void chooseRestartType(const lbool& status, RestartTypeChooser& restartTypeChooser);
+ void performStepsBeforeSolve();
// Debug:
void printLit (const Lit l) const;
if (dynamic_behaviour_analysis)
logger.set_variable_name(var, name);
} // Sets the varible 'var'-s name to 'name' in the logger
-inline void Solver::needRealUnknowns()
-{
- useRealUnknowns = true;
-}
inline const uint Solver::get_unitary_learnts_num() const
{
if (decisionLevel() > 0)
typedef uint32_t Var;
#define var_Undef (0xffffffffU >>1)
+enum RestartType {dynamic_restart, static_restart};
class Lit
{
CryptoMiniSat
-SVN revision: 594
-GIT revision: 4b4477ffe685caf5a034f65063c93c20929440f8
+SVN revision: 614
+GIT revision: 7c6e2b5d2a1d4da60a0d70a3f0745c69f12d8ed2
cout << "Replacer started." << endl;
#endif
- S->clauseCleaner->removeSatisfied(S->clauses, ClauseCleaner::clauses);
- S->clauseCleaner->removeSatisfied(S->learnts, ClauseCleaner::learnts);
- S->clauseCleaner->removeSatisfied(S->xorclauses, ClauseCleaner::xorclauses);
-
S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses);
S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts);
S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
return lastReplacedVars;
}
+const uint VarReplacer::getNewToReplaceVars() const
+{
+ return replacedVars-lastReplacedVars;
+}
+
const vector<Lit>& VarReplacer::getReplaceTable() const
{
return table;
const uint getNumReplacedLits() const;
const uint getNumReplacedVars() const;
const uint getNumLastReplacedVars() const;
+ const uint getNewToReplaceVars() const;
const vector<Var> getReplacingVars() const;
const vector<Lit>& getReplaceTable() const;
const vec<Clause*>& getClauses() const;
#include <iostream>
#include "Solver.h"
#include "VarReplacer.h"
+#include "ClauseCleaner.h"
namespace MINISAT
{
uint XorFinder::doNoPart(uint& sumLengths, const uint minSize, const uint maxSize)
{
+ S->clauseCleaner->cleanClauses(S->clauses, ClauseCleaner::clauses);
+
toRemove.clear();
toRemove.resize(cls.size(), false);
#define RATIOREMOVECLAUSES 2
#define NBCLAUSESBEFOREREDUCE 20000
#define DYNAMICNBLEVEL
-#define CONSTANTREMOVECLAUSE
#define UPDATEVARACTIVITY
-#define BLOCK
+#define PERCENTAGEPERFORMREPLACE 0.03
#define Heap_h
#include "Vec.h"
+#include "string.h"
namespace MINISAT
{
public:
Heap(const Comp& c) : lt(c) { }
+ Heap(const Heap<Comp>& other) : lt(other.lt) {
+ heap.growTo(other.heap.size());
+ memcpy(heap.getData(), other.heap.getData(), sizeof(int)*other.heap.size());
+ indices.growTo(other.indices.size());
+ memcpy(indices.getData(), other.indices.getData(), sizeof(int)*other.indices.size());
+ }
int size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
#endif
#if defined CRYPTOMINISAT2
- //newSolver.set_gaussian_decision_until(50);
+ newSolver.set_gaussian_decision_until(100);
newSolver.performReplace = false;
newSolver.xorFinder = false;
#endif
projects / francis / stp.git / commitdiff