+++ /dev/null
-/***********************************************************************************[SolverTypes.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-
-#include "Clause.h"
-
-namespace MINISAT
-{
-
-Clause* Clause_new(const vec<Lit>& ps, const uint group, const bool learnt)
-{
- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));
- Clause* real= new (mem) Clause(ps, group, learnt);
- return real;
-}
-
-Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt)
-{
- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));
- Clause* real= new (mem) Clause(ps, group, learnt);
- return real;
-}
-
-Clause* Clause_new(const PackedRow& row, const vec<lbool>& assigns, const vector<Var>& col_to_var_original, const uint group)
-{
- const uint size = row.popcnt();
- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*size);
- Clause* real= new (mem) Clause(row, size, assigns, col_to_var_original, group);
- return real;
-}
-
-};
16th -31st bit 16bit int size
*/
uint32_t size_etc;
- float act;
+ union { int act; uint32_t abst; } extra;
Lit data[0];
public:
- Clause(const PackedRow& row, const uint size, const vec<lbool>& assigns, const vector<Var>& col_to_var_original, const uint _group) :
- group(_group)
- {
- size_etc = 0;
- setSize(size);
- setLearnt(false);
- row.fill(data, assigns, col_to_var_original);
- }
template<class V>
Clause(const V& ps, const uint _group, const bool learnt) :
setSize(ps.size());
setLearnt(learnt);
for (uint i = 0; i < ps.size(); i++) data[i] = ps[i];
- if (learnt) act = 0;
+ if (learnt) extra.act = 0;
+ else calcAbstraction();
}
// -- use this function instead:
return data[i];
}
- float& activity () {
- return act;
+ void setActivity(int i) {
+ extra.act = i;
+ }
+
+ const int& activity () const {
+ return extra.act;
+ }
+
+ Lit subsumes (const Clause& other) const;
+
+ inline void strengthen(const Lit p)
+ {
+ remove(*this, p);
+ calcAbstraction();
+ }
+
+ void calcAbstraction() {
+ uint32_t abstraction = 0;
+ for (int i = 0; i < size(); i++)
+ abstraction |= 1 << (data[i].var() & 31);
+ extra.abst = abstraction;
}
- Lit* getData () {
+ const Lit* getData () const {
+ return data;
+ }
+ Lit* getData () {
return data;
}
void print() {
}
};
-Clause* Clause_new(const vec<Lit>& ps, const uint group, const bool learnt);
-Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt);
-Clause* Clause_new(const PackedRow& ps, const vec<lbool>& assigns, const vector<Var>& col_to_var_original, const uint group);
+template<class T>
+Clause* Clause_new(const T& ps, const uint group, const bool learnt = false)
+{
+ void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));
+ Clause* real= new (mem) Clause(ps, group, learnt);
+ return real;
+}
+//Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt);
+
+/*_________________________________________________________________________________________________
+|
+| subsumes : (other : const Clause&) -> Lit
+|
+| Description:
+| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
+| by subsumption resolution.
+|
+| Result:
+| lit_Error - No subsumption or simplification
+| lit_Undef - Clause subsumes 'other'
+| p - The literal p can be deleted from 'other'
+|________________________________________________________________________________________________@*/
+inline Lit Clause::subsumes(const Clause& other) const
+{
+ if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
+ return lit_Error;
+
+ Lit ret = lit_Undef;
+ const Lit* c = this->getData();
+ const Lit* d = other.getData();
+
+ for (int i = 0; i < size(); i++) {
+ // search for c[i] or ~c[i]
+ for (int j = 0; j < other.size(); j++)
+ if (c[i] == d[j])
+ goto ok;
+ else if (ret == lit_Undef && c[i] == ~d[j]){
+ ret = c[i];
+ goto ok;
+ }
+
+ // did not find it
+ return lit_Error;
+ ok:;
+ }
+
+ return ret;
+}
+
+
+class WatchedBin {
+ public:
+ WatchedBin(Clause *_clause, Lit _impliedLit) : impliedLit(_impliedLit), clause(_clause) {};
+ Lit impliedLit;
+ Clause *clause;
+};
};
#endif //CLAUSE_H
#endif
S->xorclauses.push(newX);
+ S->xorclauses_tofree.push(newX);
toRemove.push_back(false);
S->attachClause(*newX);
for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) {
using std::cout;
using std::endl;
-uint64_t* PackedRow::tmp_row;
-
ostream& operator << (ostream& os, const vec<Lit>& v)
{
for (int i = 0; i < v.size(); i++) {
return os;
}
-Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _matrix_no) :
+Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _matrix_no, const vector<XorClause*>& _xorclauses) :
solver(_solver)
, config(_config)
, matrix_no(_matrix_no)
+ , xorclauses(_xorclauses)
, messed_matrix_vars_since_reversal(true)
, gauss_last_level(0)
, disabled(false)
, useful_confl(0)
, called(0)
{
- PackedRow::tmp_row = new uint64_t[1000];
}
Gaussian::~Gaussian()
clear_clauses();
}
+inline void Gaussian::set_matrixset_to_cur()
+{
+ uint level = solver.decisionLevel() / config.only_nth_gauss_save;
+ assert(level <= matrix_sets.size());
+
+ if (level == matrix_sets.size())
+ matrix_sets.push_back(cur_matrixset);
+ else
+ matrix_sets[level] = cur_matrixset;
+}
+
void Gaussian::clear_clauses()
{
std::for_each(matrix_clauses_toclear.begin(), matrix_clauses_toclear.end(), std::ptr_fun(free));
llbool Gaussian::full_init()
{
- assert(config.every_nth_gauss > 0);
- assert(config.only_nth_gauss_save >= config.every_nth_gauss);
- assert(config.only_nth_gauss_save % config.every_nth_gauss == 0);
- assert(config.decision_from % config.every_nth_gauss == 0);
- assert(config.decision_from % config.only_nth_gauss_save == 0);
-
if (!should_init()) return l_Nothing;
bool do_again_gauss = true;
return l_Nothing;
}
-void Gaussian::init(void)
+void Gaussian::init()
{
assert(solver.decisionLevel() == 0);
- matrix_sets.clear();
- fill_matrix();
- if (origMat.num_rows == 0) return;
+ fill_matrix(cur_matrixset);
+ if (!cur_matrixset.num_rows || !cur_matrixset.num_cols) {
+ disabled = true;
+ badlevel = 0;
+ return;
+ }
- cur_matrixset = origMat;
-
+ matrix_sets.clear();
+ matrix_sets.push_back(cur_matrixset);
gauss_last_level = solver.trail.size();
messed_matrix_vars_since_reversal = false;
- if (config.decision_from > 0) went_below_decision_from = true;
- else went_below_decision_from = true;
+ badlevel = UINT_MAX;
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")Gaussian init finished." << endl;
#endif
}
-uint Gaussian::select_columnorder(vector<uint16_t>& var_to_col)
+uint Gaussian::select_columnorder(vector<uint16_t>& var_to_col, matrixset& origMat)
{
var_to_col.resize(solver.nVars(), unassigned_col);
- uint largest_used_var = 0;
uint num_xorclauses = 0;
- for (int i = 0; i < solver.xorclauses.size(); i++) {
+ for (int i = 0; i != xorclauses.size(); i++) {
#ifdef DEBUG_GAUSS
- assert(!solver.satisfied(*solver.xorclauses[i]));
+ assert(xorclauses[i]->mark() || !solver.satisfied(*xorclauses[i]));
#endif
- if (solver.xorclauses[i]->getMatrix() == matrix_no) {
+ if (!xorclauses[i]->mark()) {
num_xorclauses++;
- XorClause& c = *solver.xorclauses[i];
+ XorClause& c = *xorclauses[i];
for (uint i2 = 0; i2 < c.size(); i2++) {
assert(solver.assigns[c[i2].var()].isUndef());
- var_to_col[c[i2].var()] = 1;
- largest_used_var = std::max(largest_used_var, c[i2].var());
+ var_to_col[c[i2].var()] = unassigned_col - 1;
}
}
}
+
+ uint largest_used_var = 0;
+ for (uint i = 0; i < var_to_col.size(); i++)
+ if (var_to_col[i] != unassigned_col)
+ largest_used_var = i;
var_to_col.resize(largest_used_var + 1);
+
+ var_is_in.resize(var_to_col.size());
+ var_is_in.setZero();
+ origMat.var_is_set.resize(var_to_col.size());
+ origMat.var_is_set.setZero();
origMat.col_to_var.clear();
for (int i = solver.order_heap.size()-1; i >= 0 ; i--)
#endif
origMat.col_to_var.push_back(v);
- var_to_col[v] = 2;
+ var_to_col[v] = origMat.col_to_var.size()-1;
+ var_is_in.setBit(v);
}
}
//for the ones that were not in the order_heap, but are marked in var_to_col
- for (uint i = 0; i < var_to_col.size(); i++) {
- if (var_to_col[i] == 1)
- origMat.col_to_var.push_back(i);
+ for (uint v = 0; v != var_to_col.size(); v++) {
+ if (var_to_col[v] == unassigned_col - 1) {
+ origMat.col_to_var.push_back(v);
+ var_to_col[v] = origMat.col_to_var.size() -1;
+ var_is_in.setBit(v);
+ }
}
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")col_to_var:";
std::copy(origMat.col_to_var.begin(), origMat.col_to_var.end(), std::ostream_iterator<uint>(cout, ","));
cout << endl;
-
- cout << "(" << matrix_no << ")var_to_col:" << endl;
#endif
- var_is_in.resize(var_to_col.size());
- var_is_in.setZero();
- origMat.var_is_set.resize(var_to_col.size());
- origMat.var_is_set.setZero();
- for (uint i = 0; i < var_to_col.size(); i++) {
- if (var_to_col[i] != unassigned_col) {
- vector<uint>::iterator it = std::find(origMat.col_to_var.begin(), origMat.col_to_var.end(), i);
- assert(it != origMat.col_to_var.end());
- var_to_col[i] = &(*it) - &origMat.col_to_var[0];
- var_is_in.setBit(i);
- #ifdef VERBOSE_DEBUG
- cout << "(" << matrix_no << ")var_to_col[" << i << "]:" << var_to_col[i] << endl;
- #endif
- }
- }
-
return num_xorclauses;
}
-void Gaussian::fill_matrix()
+void Gaussian::fill_matrix(matrixset& origMat)
{
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")Filling matrix" << endl;
#endif
vector<uint16_t> var_to_col;
- origMat.num_rows = select_columnorder(var_to_col);
+ origMat.num_rows = select_columnorder(var_to_col, origMat);
origMat.num_cols = origMat.col_to_var.size();
col_to_var_original = origMat.col_to_var;
changed_rows.resize(origMat.num_rows);
changed_rows.setZero();
- if (origMat.num_rows == 0) return;
origMat.last_one_in_col.resize(origMat.num_cols);
std::fill(origMat.last_one_in_col.begin(), origMat.last_one_in_col.end(), origMat.num_rows);
#endif
uint matrix_row = 0;
- for (int i = 0; i < solver.xorclauses.size(); i++) {
- const XorClause& c = *solver.xorclauses[i];
+ for (int i = 0; i < xorclauses.size(); i++) {
+ const XorClause& c = *xorclauses[i];
- if (c.getMatrix() == matrix_no) {
+ if (!c.mark()) {
origMat.varset[matrix_row].set(c, var_to_col, origMat.num_cols);
origMat.matrix[matrix_row].set(c, var_to_col, origMat.num_cols);
matrix_row++;
#ifdef DEBUG_GAUSS
bool c = false;
- for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.size(); r != end; ++r)
+ for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.getSize(); r != end; ++r)
c |= (*r)[col];
assert(!c);
#endif
#endif
#ifdef DEBUG_GAUSS
- assert(config.every_nth_gauss != 1 || nothing_to_propagate(cur_matrixset));
- assert(check_last_one_in_cols(m));
+ assert(nothing_to_propagate(cur_matrixset));
+ assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m));
#endif
changed_rows.setZero();
uint last = 0;
uint col = 0;
- for (Var *it = &m.col_to_var[0], *end = it + m.num_cols; it != end; col++, it++) {
+ for (const Var *it = &m.col_to_var[0], *end = it + m.num_cols; it != end; col++, it++) {
if (*it != unassigned_var && solver.assigns[*it].isDef()) {
update_matrix_col(m, *it, col);
last++;
last = 0;
}
m.num_cols -= last;
- m.past_the_end_last_one_in_col -= last;
+ m.past_the_end_last_one_in_col = std::min(m.past_the_end_last_one_in_col, (uint16_t)m.num_cols);
#ifdef DEBUG_GAUSS
- check_matrix_against_varset(m.matrix, m.varset);
+ check_matrix_against_varset(m.matrix, m.varset, m);
#endif
#ifdef VERBOSE_DEBUG
Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
{
- if (origMat.num_rows == 0) return nothing;
+ if (solver.decisionLevel() >= badlevel)
+ return nothing;
- if (!messed_matrix_vars_since_reversal) {
+ if (messed_matrix_vars_since_reversal) {
#ifdef VERBOSE_DEBUG
- cout << "(" << matrix_no << ")matrix needs only update" << endl;
+ cout << "(" << matrix_no << ")matrix needs copy before update" << endl;
#endif
- update_matrix_by_col_all(cur_matrixset);
- } else {
- #ifdef VERBOSE_DEBUG
- cout << "(" << matrix_no << ")matrix needs copy&update" << endl;
- #endif
-
- if (went_below_decision_from)
- cur_matrixset = origMat;
- else
- cur_matrixset = matrix_sets[((solver.decisionLevel() - config.decision_from) / config.only_nth_gauss_save)];
-
- update_matrix_by_col_all(cur_matrixset);
+ const uint level = solver.decisionLevel() / config.only_nth_gauss_save;
+ assert(level < matrix_sets.size());
+ cur_matrixset = matrix_sets[level];
}
- if (!cur_matrixset.num_cols || !cur_matrixset.num_cols)
- return nothing;
+ update_matrix_by_col_all(cur_matrixset);
messed_matrix_vars_since_reversal = false;
gauss_last_level = solver.trail.size();
+ badlevel = UINT_MAX;
propagatable_rows.clear();
-
uint conflict_row = UINT_MAX;
uint last_row = eliminate(cur_matrixset, conflict_row);
#ifdef DEBUG_GAUSS
- check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset.varset);
+ check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset.varset, cur_matrixset);
#endif
gaussian_ret ret;
- if (conflict_row != UINT_MAX) {
+ //There is no early abort, so this is unneeded
+ /*if (conflict_row != UINT_MAX) {
uint maxlevel = UINT_MAX;
uint size = UINT_MAX;
uint best_row = UINT_MAX;
analyse_confl(cur_matrixset, conflict_row, maxlevel, size, best_row);
ret = handle_matrix_confl(confl, cur_matrixset, size, maxlevel, best_row);
-
- } else {
+ } else {*/
ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl);
+ //}
+
+ if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) {
+ badlevel = solver.decisionLevel();
+ return nothing;
}
- if (ret == nothing
- && (solver.decisionLevel() == 0 || ((solver.decisionLevel() - config.decision_from) % config.only_nth_gauss_save == 0))
- )
+ if (ret == nothing &&
+ solver.decisionLevel() % config.only_nth_gauss_save == 0)
set_matrixset_to_cur();
#ifdef VERBOSE_DEBUG
#ifdef DEBUG_GAUSS
- assert(check_last_one_in_cols(m));
+ assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m));
#endif
uint i = 0;
if (this_matrix_row != end) {
PackedRow matrix_row_i = m.matrix[i];
PackedRow varset_row_i = m.varset[i];
+ PackedMatrix::iterator this_varset_row = m.varset.begin() + best_row;
//swap rows i and maxi, but do not change the value of i;
if (i != best_row) {
no_exchanged++;
#endif
- if (!matrix_row_i.get_xor_clause_inverted() && matrix_row_i.isZero()) {
- conflict_row = i;
- return 0;
- }
+ //Would early abort, but would not find the best conflict (and would be expensive)
+ //if (!matrix_row_i.get_xor_clause_inverted() && matrix_row_i.isZero()) {
+ // conflict_row = i;
+ // return 0;
+ //}
matrix_row_i.swap(*this_matrix_row);
- varset_row_i.swap(m.varset[best_row]);
+ varset_row_i.swap(*this_varset_row);
}
#ifdef DEBUG_GAUSS
assert(m.matrix[i].popcnt(j) == m.matrix[i].popcnt());
propagatable_rows.push(i);
//Now A[i,j] will contain the old value of A[maxi,j];
- uint i2 = best_row+1;
- for (PackedMatrix::iterator it = this_matrix_row+1, it2 = m.varset.begin() + i2; it != end; ++it, ++it2, i2++) if ((*it)[j]) {
+ ++this_matrix_row;
+ ++this_varset_row;
+ for (; this_matrix_row != end; ++this_matrix_row, ++this_varset_row) if ((*this_matrix_row)[j]) {
//subtract row i from row u;
//Now A[u,j] will be 0, since A[u,j] - A[i,j] = A[u,j] -1 = 0.
#ifdef VERBOSE_DEBUG
number_of_row_additions++;
#endif
- *it ^= matrix_row_i;
- *it2 ^= varset_row_i;
- //Would early abort, but would not find the best conflict:
+ *this_matrix_row ^= matrix_row_i;
+ *this_varset_row ^= varset_row_i;
+ //Would early abort, but would not find the best conflict (and would be expensive)
//if (!it->get_xor_clause_inverted() &&it->isZero()) {
// conflict_row = i2;
// return 0;
#ifdef VERBOSE_DEBUG
cout << "row:" << row << " col:" << col << " m.last_one_in_col[col]-1: " << m.last_one_in_col[col]-1 << endl;
#endif
- assert(m.last_one_in_col[col]-1 == row);
+ assert(m.col_to_var[col] == unassigned_var || std::min(m.last_one_in_col[col]-1, (int)m.num_rows) == row);
continue;
}
row++;
{
assert(best_row != UINT_MAX);
- confl = Clause_new(m.varset[best_row], solver.assigns, col_to_var_original, solver.learnt_clause_group++);
+ m.varset[best_row].fill(tmp_clause, solver.assigns, col_to_var_original);
+ confl = Clause_new(tmp_clause, solver.learnt_clause_group++, false);
Clause& cla = *confl;
if (solver.dynamic_behaviour_analysis)
solver.logger.set_group_name(confl->group, "learnt gauss clause");
cout << endl;
#endif
- Clause& cla = *Clause_new(m.varset[row], solver.assigns, col_to_var_original, solver.learnt_clause_group++);
+ m.varset[row].fill(tmp_clause, solver.assigns, col_to_var_original);
+ Clause& cla = *Clause_new(tmp_clause, solver.learnt_clause_group++, false);
#ifdef VERBOSE_DEBUG
cout << "(" << matrix_no << ")matrix prop clause: ";
solver.printClause(cla);
const bool Gaussian::check_last_one_in_cols(matrixset& m) const
{
for(uint i = 0; i < m.num_cols; i++) {
- const uint last = m.last_one_in_col[i] - 1;
+ const uint last = std::min(m.last_one_in_col[i] - 1, (int)m.num_rows);
uint real_last = 0;
- uint i2;
+ uint i2 = 0;
for (PackedMatrix::iterator it = m.matrix.begin(); it != m.matrix.end(); ++it, i2++) {
if ((*it)[i])
real_last = i2;
}
- if (real_last > last) return false;
+ if (real_last > last)
+ return false;
}
return true;
}
-const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset) const
+const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) const
{
- assert(matrix.size() == varset.size());
+ assert(matrix.getSize() == varset.getSize());
- for (uint i = 0; i < matrix.size(); i++) {
+ for (uint i = 0; i < matrix.getSize(); i++) {
const PackedRow mat_row = matrix[i];
const PackedRow var_row = varset[i];
if (solver.assigns[var] == l_True) {
assert(!mat_row[col]);
+ assert(m.col_to_var[col] == unassigned_var);
+ assert(m.var_is_set[var]);
final = !final;
} else if (solver.assigns[var] == l_False) {
assert(!mat_row[col]);
+ assert(m.col_to_var[col] == unassigned_var);
+ assert(m.var_is_set[var]);
} else if (solver.assigns[var] == l_Undef) {
+ assert(m.col_to_var[col] != unassigned_var);
+ assert(!m.var_is_set[var]);
assert(mat_row[col]);
} else assert(false);
class Gaussian
{
public:
- Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no);
+ Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no, const vector<XorClause*>& xorclauses);
~Gaussian();
llbool full_init();
//Gauss high-level configuration
const GaussianConfig& config;
const uint matrix_no;
+ vector<XorClause*> xorclauses;
enum gaussian_ret {conflict, unit_conflict, propagation, unit_propagation, nothing};
gaussian_ret gaussian(Clause*& confl);
- vector<Var> col_to_var_original;
- BitArray var_is_in;
+ vector<Var> col_to_var_original; //Matches columns to variables
+ BitArray var_is_in; //variable is part of the the matrix. var_is_in's size is _minimal_ so you should check whether var_is_in.getSize() < var before issuing var_is_in[var]
+ uint badlevel;
class matrixset
{
PackedMatrix matrix; // The matrix, updated to reflect variable assignements
PackedMatrix varset; // The matrix, without variable assignements. The xor-clause is read from here. This matrix only follows the 'matrix' with its row-swap, row-xor, and row-delete operations.
BitArray var_is_set;
- vector<Var> col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives UINT_MAX if the COL has been zeroed (i.e. the variable assigned)
+ vector<Var> col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives unassigned_var if the COL has been zeroed (i.e. the variable assigned)
uint16_t num_rows; // number of active rows in the matrix. Unactive rows are rows that contain only zeros (and if they are conflicting, then the conflict has been treated)
uint num_cols; // number of active columns in the matrix. The columns at the end that have all be zeroed are no longer active
int least_column_changed; // when updating the matrix, this value contains the smallest column number that has been updated (Gauss elim. can start from here instead of from column 0)
uint16_t past_the_end_last_one_in_col;
- vector<uint16_t> last_one_in_col; //last_one_in_col[COL] tells the last row that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row)
+ vector<uint16_t> last_one_in_col; //last_one_in_col[COL] tells the last row+1 that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row)
uint removeable_cols; // the number of columns that have been zeroed out (i.e. assigned)
};
//Saved states
vector<matrixset> matrix_sets; // The matrixsets for depths 'decision_from' + 0, 'decision_from' + only_nth_gaussian_save, 'decision_from' + 2*only_nth_gaussian_save, ... 'decision_from' + 'decision_until'.
- matrixset origMat; // The matrixset at depth 0 of the search tree
matrixset cur_matrixset; // The current matrixset, i.e. the one we are working on, or the last one we worked on
//Varibales to keep Gauss state
bool messed_matrix_vars_since_reversal;
int gauss_last_level;
vector<Clause*> matrix_clauses_toclear;
- bool went_below_decision_from;
bool disabled; // Gauss is disabled
//State of current elimnation
//gauss init functions
void init(); // Initalise gauss state
- void fill_matrix(); // Fills the origMat matrix
- uint select_columnorder(vector<uint16_t>& var_to_col); // Fills var_to_col and col_to_var of the origMat matrix.
+ void fill_matrix(matrixset& origMat); // Fills the origMat matrix
+ uint select_columnorder(vector<uint16_t>& var_to_col, matrixset& origMat); // Fills var_to_col and col_to_var of the origMat matrix.
//Main function
uint eliminate(matrixset& matrix, uint& conflict_row); //does the actual gaussian elimination
void analyse_confl(const matrixset& m, const uint row, uint& maxlevel, uint& size, uint& best_row) const; // analyse conflcit to find the best conflict. Gets & returns the best one in 'maxlevel', 'size' and 'best row' (these are all UINT_MAX when calling this function first, i.e. when there is no other possible conflict to compare to the new in 'row')
gaussian_ret handle_matrix_confl(Clause*& confl, const matrixset& m, const uint size, const uint maxlevel, const uint best_row);
gaussian_ret handle_matrix_prop(matrixset& m, const uint row); // Handle matrix propagation at row 'row'
+ vec<Lit> tmp_clause;
//propagation&conflict handling
void cancel_until_sublevel(const uint sublevel); // cancels until sublevel 'sublevel'. The var 'sublevel' must NOT go over the current level. I.e. this function is ONLY for moving inside the current level
void print_matrix_row(const T& row) const; // Print matrix row 'row'
template<class T>
void print_matrix_row_with_assigns(const T& row) const;
- const bool check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset) const;
+ const bool check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) const;
const bool check_last_one_in_cols(matrixset& m) const;
void print_matrix(matrixset& m) const;
void print_last_one_in_cols(matrixset& m) const;
static const string lbool_to_string(const lbool toprint);
};
-inline void Gaussian::back_to_level(const uint level)
-{
- if (level <= config.decision_from) went_below_decision_from = true;
-}
-
inline bool Gaussian::should_init() const
{
return (solver.starts >= config.starts_from && config.decision_until > 0);
{
return (!disabled
&& starts >= config.starts_from
- && decisionlevel < config.decision_until
- && decisionlevel >= config.decision_from
- && decisionlevel % config.every_nth_gauss == 0);
+ && decisionlevel < config.decision_until);
}
inline void Gaussian::canceling(const uint level, const Var var)
cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl;
}
-inline void Gaussian::set_matrixset_to_cur()
-{
- /*cout << solver.decisionLevel() << endl;
- cout << decision_from << endl;
- cout << matrix_sets.size() << endl;*/
-
- if (solver.decisionLevel() == 0) {
- origMat = cur_matrixset;
- }
-
- if (solver.decisionLevel() >= config.decision_from) {
- uint level = ((solver.decisionLevel() - config.decision_from) / config.only_nth_gauss_save);
-
- assert(level <= matrix_sets.size()); //TODO check if we need this, or HOW we need this in a multi-matrix setting
- if (level == matrix_sets.size())
- matrix_sets.push_back(cur_matrixset);
- else
- matrix_sets[level] = cur_matrixset;
- }
-}
-
std::ostream& operator << (std::ostream& os, const vec<Lit>& v);
};
#define GAUSSIANCONFIG_H
#include <sys/types.h>
+#include "PackedRow.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
class GaussianConfig
{
GaussianConfig() :
only_nth_gauss_save(2)
- , decision_from(0)
, decision_until(0)
- , every_nth_gauss(1)
, starts_from(3)
{
+ if (PackedRow::tmp_row == NULL)
+ PackedRow::tmp_row = new uint64_t[1000];
+ }
+
+ ~GaussianConfig()
+ {
+ delete[] PackedRow::tmp_row;
}
//tuneable gauss parameters
uint only_nth_gauss_save; //save only every n-th gauss matrix
- uint decision_from; //start from this decision level
uint decision_until; //do Gauss until this level
- uint every_nth_gauss; //do Gauss every nth level
uint starts_from; //Gauss elimination starts from this restart number
};
-
-#endif //GAUSSIANCONFIG_H
\ No newline at end of file
+};
+#endif //GAUSSIANCONFIG_H
Logger::Logger(int& _verbosity) :
proof_graph_on(false)
- , statistics_on(false)
, mini_proof(false)
+ , statistics_on(false)
, max_print_lines(20)
, uniqueid(1)
void Logger::begin()
{
if (proof_graph_on) {
- char filename[80];
- sprintf(filename, "proofs/%d-proof%d.dot", runid, S->starts);
+ std::stringstream filename;
+ filename << "proofs/" << runid << "-proof" << S->starts << ".dot";
if (S->starts == 0)
history.push_back(uniqueid);
history.resize(S->trail.size()+1);
}
- proof = fopen(filename,"w");
- if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename), exit(-1);
+ proof = fopen(filename.str().c_str(),"w");
+ if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename.str().c_str()), exit(-1);
fprintf(proof, "digraph G {\n");
fprintf(proof,"node%d [shape=circle, label=\"BEGIN\", root];\n", history[history.size()-1]);
}
void setSolver(const Solver* S);
//types of props, confl, and finish
- enum prop_type { revert_guess_type, unit_clause_type, add_clause_type, assumption_type, guess_type, simple_propagation_type, gauss_propagation_type };
+ enum prop_type { unit_clause_type, add_clause_type, assumption_type, guess_type, simple_propagation_type, gauss_propagation_type };
enum confl_type { simple_confl_type, gauss_confl_type };
enum finish_type { model_found, unsat_model_found, restarting, done_adding_clauses };
MTL = ../cryptominisat/mtl
MTRAND = ../cryptominisat/MTRand
-SOURCES = Clause.cpp Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp
+SOURCES = Conglomerate.cpp FindUndef.cpp Gaussian.cpp Logger.cpp MatrixFinder.cpp PackedRow.cpp Solver.cpp VarReplacer.cpp XorFinder.cpp
OBJECTS = $(SOURCES:.cpp=.o)
LIB = libminisat.a
CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
//#define PART_FINDING
MatrixFinder::MatrixFinder(Solver *_S) :
- S(_S)
- , unAssigned(_S->nVars() + 1)
+ unAssigned(_S->nVars() + 1)
+ , S(_S)
{
table.resize(S->nVars(), unAssigned);
matrix_no = 0;
const uint MatrixFinder::setMatrixes()
{
- vector<uint> numXorInMatrix(matrix_no, 0);
+ vector<pair<uint, uint> > numXorInMatrix;
+ for (uint i = 0; i < matrix_no; i++)
+ numXorInMatrix.push_back(std::make_pair(i, 0));
+
vector<uint> sumXorSizeInMatrix(matrix_no, 0);
vector<vector<uint> > xorSizesInMatrix(matrix_no);
vector<vector<XorClause*> > xorsInMatrix(matrix_no);
for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) {
XorClause& x = **c;
const uint matrix = table[x[0].var()];
+ assert(matrix < matrix_no);
//for stats
- numXorInMatrix[matrix]++;
+ numXorInMatrix[matrix].second++;
sumXorSizeInMatrix[matrix] += x.size();
xorSizesInMatrix[matrix].push_back(x.size());
xorsInMatrix[matrix].push_back(&x);
#endif //PART_FINDING
}
+ std::sort(numXorInMatrix.begin(), numXorInMatrix.end(), mysorter());
+
#ifdef PART_FINDING
for (uint i = 0; i < matrix_no; i++)
findParts(xorFingerprintInMatrix[i], xorsInMatrix[i]);
#endif //PART_FINDING
uint realMatrixNum = 0;
- vector<uint> remapMatrixes(matrix_no, UINT_MAX);
- for (uint i = 0; i < matrix_no; i++) {
- if (numXorInMatrix[i] < 3)
+ for (int a = matrix_no-1; a != -1; a--) {
+ uint i = numXorInMatrix[a].first;
+
+ if (numXorInMatrix[a].second < 3)
continue;
- const uint totalSize = reverseTable[i].size()*numXorInMatrix[i];
+ const uint totalSize = reverseTable[i].size()*numXorInMatrix[a].second;
const double density = (double)sumXorSizeInMatrix[i]/(double)totalSize*100.0;
- double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[i];
+ double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[a].second;
double variance = 0.0;
for (uint i2 = 0; i2 < xorSizesInMatrix[i].size(); i2++)
variance += pow((double)xorSizesInMatrix[i][i2]-avg, 2);
variance /= xorSizesInMatrix.size();
const double stdDeviation = sqrt(variance);
- if (numXorInMatrix[i] >= 20
- && numXorInMatrix[i] <= 1000
- && realMatrixNum < (1 << 12))
+ if (numXorInMatrix[a].second >= 20
+ && numXorInMatrix[a].second <= 1000
+ && realMatrixNum < 3)
{
cout << "| Matrix no " << std::setw(4) << realMatrixNum;
- remapMatrixes[i] = realMatrixNum;
+ S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, realMatrixNum, xorsInMatrix[i]));
realMatrixNum++;
+
} else {
cout << "| Unused Matrix ";
}
- cout << std::setw(5) << numXorInMatrix[i] << " x" << std::setw(5) << reverseTable[i].size();
+ 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;
}
- for (XorClause** c = S->xorclauses.getData(), **end = c + S->xorclauses.size(); c != end; c++) {
- XorClause& x = **c;
- const uint toSet = remapMatrixes[table[x[0].var()]];
- if (toSet != UINT_MAX)
- x.setMatrix(toSet);
- else
- x.setMatrix((1 << 12)-1);
- }
-
- for (uint i = 0; i < realMatrixNum; i++)
- S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, i));
-
return realMatrixNum;
}
using std::map;
using std::vector;
+using std::pair;
class MatrixFinder {
private:
const uint setMatrixes();
+ struct mysorter
+ {
+ bool operator () (const pair<uint, uint>& left, const pair<uint, uint>& right)
+ {
+ return left.second < right.second;
+ }
+ };
+
void findParts(vector<Var>& xorFingerprintInMatrix, vector<XorClause*>& xorsInMatrix);
inline const Var fingerprint(const XorClause& c) const;
inline const bool firstPartOfSecond(const XorClause& c1, const XorClause& c2) const;
numRows(b.numRows)
, numCols(b.numCols)
{
+ #ifdef DEBUG_MATRIX
+ assert(b.numRows > 0 && b.numCols > 0);
+ #endif
+
mp = new uint64_t[numRows*(numCols+1)];
- std::copy(b.mp, b.mp+numRows*(numCols+1), mp);
+ memcpy(mp, b.mp, sizeof(uint64_t)*numRows*(numCols+1));
}
~PackedMatrix()
void resizeNumRows(const uint num_rows)
{
+ #ifdef DEBUG_MATRIX
+ assert(num_rows <= numRows);
+ #endif
+
numRows = num_rows;
}
PackedMatrix& operator=(const PackedMatrix& b)
{
- if (b.numRows*(b.numCols+1) > numRows*(numCols+1)) {
+ #ifdef DEBUG_MATRIX
+ //assert(b.numRows > 0 && b.numCols > 0);
+ #endif
+
+ if (numRows*(numCols+1) < b.numRows*(b.numCols+1)) {
delete[] mp;
mp = new uint64_t[b.numRows*(b.numCols+1)];
}
numRows = b.numRows;
numCols = b.numCols;
- std::copy(b.mp, b.mp+numRows*(numCols+1), mp);
+ memcpy(mp, b.mp, sizeof(uint64_t)*numRows*(numCols+1));
return *this;
}
return const_iterator(mp+numRows*(numCols+1), numCols);
}*/
- inline const uint size() const
+ inline const uint getSize() const
{
return numRows;
}
namespace MINISAT
{
+__thread uint64_t* PackedRow::tmp_row = NULL;
+
std::ostream& operator << (std::ostream& os, const PackedRow& m)
{
for(uint i = 0; i < m.size*64; i++) {
return *this;
}
-void PackedRow::fill(Lit* ps, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const
+void PackedRow::fill(vec<Lit>& tmp_clause, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const
{
bool final = xor_clause_inverted;
- Lit* ps_first = ps;
+ tmp_clause.clear();
uint col = 0;
bool wasundef = false;
for (uint i = 0; i < size; i++) for (uint i2 = 0; i2 < 64; i2++) {
const uint& var = col_to_var_original[col];
assert(var != UINT_MAX);
- const lbool val = assigns[var];
+ const lbool& val = assigns[var];
const bool val_bool = val.getBool();
- *ps = Lit(var, val_bool);
+ tmp_clause.push(Lit(var, val_bool));
final ^= val_bool;
if (val.isUndef()) {
assert(!wasundef);
- Lit tmp(*ps_first);
- *ps_first = *ps;
- *ps = tmp;
+ Lit tmp(tmp_clause[0]);
+ tmp_clause[0] = tmp_clause.last();
+ tmp_clause.last() = tmp;
wasundef = true;
}
- ps++;
}
col++;
}
if (wasundef) {
- *ps_first ^= final;
+ tmp_clause[0] ^= final;
//assert(ps != ps_first+1);
} else
assert(!final);
xor_clause_inverted = v.xor_clause_inverted();
}
- void fill(Lit* ps, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const;
+ void fill(vec<Lit>& tmp_clause, const vec<lbool>& assigns, const vector<Var>& col_to_var_original) const;
inline unsigned long int scan(const unsigned long int var) const
{
friend std::ostream& operator << (std::ostream& os, const PackedRow& m);
- static uint64_t *tmp_row;
+ static __thread uint64_t *tmp_row;
private:
friend class PackedMatrix;
PackedRow(const uint _size, uint64_t& _xor_clause_inverted, uint64_t* const _mp) :
size(_size)
- , xor_clause_inverted(_xor_clause_inverted)
, mp(_mp)
+ , xor_clause_inverted(_xor_clause_inverted)
{}
const uint size;
/****************************************************************************************[Solver.C]
MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+glucose -- Gilles Audemard, Laurent Simon (2008)
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
Solver::Solver() :
// Parameters: (formerly in 'SearchParams')
- var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
- , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
+ var_decay(1 / 0.95), random_var_freq(0.02)
+ , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1)
// More parameters:
//
, polarity_mode (polarity_user)
, verbosity (0)
, restrictedPickBranch(0)
- , useRealUnknowns(false)
+ , useRealUnknowns (false)
, xorFinder (true)
+ , greedyUnbound (false)
// Statistics: (formerly in 'SolverStats')
//
+ , nbDL2(0), nbBin(0), nbReduceDB(0)
, starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
, clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+
, ok (true)
- , cla_inc (1)
, var_inc (1)
+
+ , curRestart (1)
+ , conf4Stats (0)
+ , nbclausesbeforereduce (NBCLAUSESBEFOREREDUCE)
+
, qhead (0)
, simpDB_assigns (-1)
, simpDB_props (0)
, logger(verbosity)
, dynamic_behaviour_analysis(false) //do not document the proof as default
, maxRestarts(UINT_MAX)
+ , MYFLAG (0)
, learnt_clause_group(0)
- , greedyUnbound(false)
{
toReplace = new VarReplacer(this);
conglomerate = new Conglomerate(this);
for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_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 (int i = 0; i < xorclauses_tofree.size(); i++) free(xorclauses_tofree[i]);
for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i];
gauss_matrixes.clear();
delete toReplace;
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
Var Solver::newVar(bool sign, bool dvar)
{
- int v = nVars();
+ Var v = nVars();
watches .push(); // (list for positive literal)
watches .push(); // (list for negative literal)
+ binwatches.push(); // (list for positive literal)
+ binwatches.push(); // (list for negative literal)
xorwatches.push(); // (list for variables in xors)
reason .push(NULL);
assigns .push(l_Undef);
level .push(-1);
activity .push(0);
seen .push(0);
+ permDiff .push(0);
polarity .push_back((char)sign);
decision_var.push_back(dvar);
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- while (ps[i].var() >= nVars()) newVar();
xor_clause_inverted ^= ps[i].sign();
ps[i] ^= ps[i].sign();
XorClause* c = XorClause_new(ps, xor_clause_inverted, group);
xorclauses.push(c);
+ xorclauses_tofree.push(c);
attachClause(*c);
break;
}
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- while (ps[i].var() >= nVars()) newVar();
-
if (value(ps[i]) == l_True || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps.shrink(i - j);
if (ps.size() == 0) {
- if (dynamic_behaviour_analysis) logger.empty_clause(group);
+ if (dynamic_behaviour_analysis)
+ logger.empty_clause(group);
return ok = false;
} else if (ps.size() == 1) {
assert(value(ps[0]) == l_Undef);
void Solver::attachClause(XorClause& c)
{
- assert(c.size() > 1);
+ assert(c.size() > 2);
xorwatches[c[0].var()].push(&c);
xorwatches[c[1].var()].push(&c);
void Solver::attachClause(Clause& c)
{
assert(c.size() > 1);
-
- watches[(~c[0]).toInt()].push(&c);
- watches[(~c[1]).toInt()].push(&c);
+ int index0 = (~c[0]).toInt();
+ int index1 = (~c[1]).toInt();
+
+ if (c.size() == 2) {
+ binwatches[index0].push(WatchedBin(&c, c[1]));
+ binwatches[index1].push(WatchedBin(&c, c[0]));
+ } else {
+ watches[index0].push(&c);
+ watches[index1].push(&c);
+ }
if (c.learnt()) learnts_literals += c.size();
else clauses_literals += c.size();
void Solver::detachClause(const Clause& c)
{
assert(c.size() > 1);
- assert(find(watches[(~c[0]).toInt()], &c));
- assert(find(watches[(~c[1]).toInt()], &c));
- remove(watches[(~c[0]).toInt()], &c);
- remove(watches[(~c[1]).toInt()], &c);
+ if (c.size() == 2) {
+ assert(findWatchedBinCl(binwatches[(~c[0]).toInt()], &c));
+ assert(findWatchedBinCl(binwatches[(~c[1]).toInt()], &c));
+
+ removeWatchedBinCl(binwatches[(~c[0]).toInt()], &c);
+ removeWatchedBinCl(binwatches[(~c[1]).toInt()], &c);
+ } else {
+ assert(findWatchedCl(watches[(~c[0]).toInt()], &c));
+ assert(findWatchedCl(watches[(~c[1]).toInt()], &c));
+
+ removeWatchedCl(watches[(~c[0]).toInt()], &c);
+ removeWatchedCl(watches[(~c[1]).toInt()], &c);
+ }
+
if (c.learnt()) learnts_literals -= c.size();
else clauses_literals -= c.size();
}
void Solver::detachModifiedClause(const Lit lit1, const Lit lit2, const uint origSize, const Clause* address)
{
assert(origSize > 1);
- assert(find(watches[(~lit1).toInt()], address));
- assert(find(watches[(~lit2).toInt()], address));
- remove(watches[(~lit1).toInt()], address);
- remove(watches[(~lit2).toInt()], address);
+
+ if (origSize == 2) {
+ assert(findWatchedBinCl(binwatches[(~lit1).toInt()], address));
+ assert(findWatchedBinCl(binwatches[(~lit2).toInt()], address));
+ removeWatchedBinCl(binwatches[(~lit1).toInt()], address);
+ removeWatchedBinCl(binwatches[(~lit2).toInt()], address);
+ } else {
+ assert(find(watches[(~lit1).toInt()], address));
+ assert(find(watches[(~lit2).toInt()], address));
+ remove(watches[(~lit1).toInt()], address);
+ remove(watches[(~lit2).toInt()], address);
+ }
if (address->learnt()) learnts_literals -= origSize;
else clauses_literals -= origSize;
}
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
trail_lim.shrink(trail_lim.size() - level);
- for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
- (*gauss)->back_to_level(decisionLevel());
}
#ifdef VERBOSE_DEBUG
gaussconfig.decision_until = to;
}
-void Solver::set_gaussian_decision_from(const uint from)
-{
- gaussconfig.decision_from = from;
-}
-
//=================================================================================================
// Major methods:
| Effect:
| Will undo part of the trail, upto but not beyond the assumption of the current decision level.
|________________________________________________________________________________________________@*/
-void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
+void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, int &nbLevels/*, int &merged*/)
{
int pathC = 0;
Lit p = lit_Undef;
do {
assert(confl != NULL); // (otherwise should be UIP)
Clause& c = *confl;
-
- if (c.learnt())
- claBumpActivity(c);
+ if (p != lit_Undef)
+ reverse_binary_clause(c);
for (uint j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) {
const Lit& q = c[j];
if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var]))
varBumpActivity(my_var);
seen[my_var] = 1;
- if (level[my_var] >= decisionLevel())
+ if (level[my_var] >= decisionLevel()) {
pathC++;
- else {
+ #ifdef UPDATEVARACTIVITY
+ if ( reason[q.var()] != NULL && reason[q.var()]->learnt() )
+ lastDecisionLevel.push(q);
+ #endif
+ } else {
out_learnt.push(q);
if (level[my_var] > out_btlevel)
out_btlevel = level[my_var];
} else {
out_learnt.copyTo(analyze_toclear);
for (i = j = 1; i < out_learnt.size(); i++) {
- const Clause& c = *reason[out_learnt[i].var()];
+ Clause& c = *reason[out_learnt[i].var()];
+ reverse_binary_clause(c);
+
for (uint k = 1; k < c.size(); k++)
if (!seen[c[k].var()] && level[c[k].var()] > 0) {
out_learnt[j++] = out_learnt[i];
out_btlevel = level[p.var()];
}
+ nbLevels = 0;
+ MYFLAG++;
+ for(int i = 0; i < out_learnt.size(); i++) {
+ int lev = level[out_learnt[i].var()];
+ if (permDiff[lev] != MYFLAG) {
+ permDiff[lev] = MYFLAG;
+ nbLevels++;
+ //merged += nbPropagated(lev);
+ }
+ }
+
+ #ifdef UPDATEVARACTIVITY
+ if (lastDecisionLevel.size() > 0) {
+ for(int i = 0; i<lastDecisionLevel.size(); i++) {
+ if (reason[lastDecisionLevel[i].var()]->activity() < nbLevels)
+ varBumpActivity(lastDecisionLevel[i].var());
+ }
+ lastDecisionLevel.clear();
+ }
+ #endif
for (int j = 0; j < analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 0; // ('seen[]' is now cleared)
}
int top = analyze_toclear.size();
while (analyze_stack.size() > 0) {
assert(reason[analyze_stack.last().var()] != NULL);
- const Clause& c = *reason[analyze_stack.last().var()];
+ Clause& c = *reason[analyze_stack.last().var()];
+ reverse_binary_clause(c);
+
analyze_stack.pop();
for (uint i = 1; i < c.size(); i++) {
Clause **i, **j, **end;
num_props++;
+ //First propagate binary clauses
+ vec<WatchedBin> & wbin = binwatches[p.toInt()];
+ 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) {
+ uncheckedEnqueue(imp, k->clause);
+ if (dynamic_behaviour_analysis)
+ logger.propagation(imp, Logger::simple_propagation_type, k->clause->group);
+ }
+ }
+
+ //Next, propagate normal clauses
+
#ifdef VERBOSE_DEBUG
cout << "Propagating lit " << (p.sign() ? '-' : ' ') << p.var()+1 << endl;
#endif
*j++ = &c;
} else {
// Look for new watch:
- for (uint k = 2; k < c.size(); k++)
+ for (uint k = 2; k != c.size(); k++)
if (value(c[k]) != l_False) {
c[1] = c[k];
c[k] = false_lit;
uncheckedEnqueue(first, &c);
if (dynamic_behaviour_analysis)
logger.propagation(first,Logger::simple_propagation_type,c.group);
+ #ifdef DYNAMICNBLEVEL
+ if (c.learnt() && c.activity() > 2) { // GA
+ MYFLAG++;
+ int nbLevels =0;
+ for(Lit *i = c.getData(), *end = i+c.size(); i != end; i++) {
+ int l = level[i->var()];
+ if (permDiff[l] != MYFLAG) {
+ permDiff[l] = MYFLAG;
+ nbLevels++;
+ }
+
+ }
+ if(nbLevels+1 < c.activity())
+ c.setActivity(nbLevels);
+ }
+ #endif
}
}
FoundWatch:
}
ws.shrink(i - j);
+ //Finally, propagate XOR-clauses
if (xor_as_well && !confl) confl = propagate_xors(p);
}
propagations += num_props;
cout << endl;
#endif
bool final = c.xor_clause_inverted();
- for (int k = 0, size = c.size(); k < size; k++ ) {
+ for (int k = 0, size = c.size(); k != size; k++ ) {
const lbool& val = assigns[c[k].var()];
if (val.isUndef() && k >= 2) {
Lit tmp(c[1]);
| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
|________________________________________________________________________________________________@*/
struct reduceDB_lt {
- bool operator () (Clause* x, Clause* y) {
- return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity());
+ 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;
+ if (xsize == 2 && ysize == 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;
}
};
+
void Solver::reduceDB()
{
int i, j;
- double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity
+ nbReduceDB++;
sort(learnts, reduceDB_lt());
- for (i = j = 0; i < learnts.size() / 2; i++) {
- if (learnts[i]->size() > 2 && !locked(*learnts[i]))
+ for (i = j = 0; i < learnts.size() / RATIOREMOVECLAUSES; i++){
+ if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() > 2)
removeClause(*learnts[i]);
else
learnts[j++] = learnts[i];
}
for (; i < learnts.size(); i++) {
- if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim)
- removeClause(*learnts[i]);
- else
- learnts[j++] = learnts[i];
+ learnts[j++] = learnts[i];
}
learnts.shrink(i - j);
}
maxRestarts = num;
}
-bool Solver::cleanClause(Clause& c) const
+bool Solver::cleanClause(Clause& c)
{
+ assert(c.size() >= 2);
+ Lit first = c[0];
+ Lit second = c[1];
+
Lit *i, *j, *end;
uint at = 0;
for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) {
} else assert(at > 1);
assert(value(*i) != l_True);
}
- c.shrink(i-j);
+ if ((c.size() > 2) && (c.size() - (i-j) == 2)) {
+ detachModifiedClause(first, second, c.size(), &c);
+ c.shrink(i-j);
+ attachClause(c);
+ } else
+ c.shrink(i-j);
return (i-j > 0);
}
void Solver::cleanClauses(vec<XorClause*>& cs)
{
uint useful = 0;
- for (int s = 0; s < cs.size(); s++) {
- XorClause& c = *cs[s];
+ 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();
c.shrink(i-j);
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);
+ removeClause(c);
+ s++;
+ } else
+ *ss++ = *s++;
+
#ifdef VERBOSE_DEBUG
std::cout << "Cleaned clause:";
c.plain_print();
#endif
assert(c.size() > 1);
}
+ cs.shrink(s-ss);
#ifdef VERBOSE_DEBUG
cout << "cleanClauses(XorClause) useful:" << useful << endl;
| all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
|________________________________________________________________________________________________@*/
-lbool Solver::search(int nof_conflicts, int nof_learnts)
+lbool Solver::search(int nof_conflicts)
{
assert(ok);
int conflictC = 0;
else if (ret != l_Nothing) return ret;
}
if (at_least_one_continue) continue;
- ret = new_decision(nof_conflicts, nof_learnts, conflictC);
+ ret = new_decision(nof_conflicts, conflictC);
if (ret != l_Nothing) return ret;
}
}
}
-llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC)
+llbool Solver::new_decision(int& nof_conflicts, int& conflictC)
{
if (nof_conflicts >= 0 && conflictC >= nof_conflicts) {
// Reached bound on number of conflicts:
return l_False;
}
- if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
- // Reduce the set of learnt clauses:
+ // Reduce the set of learnt clauses:
+ if (conflicts >= curRestart * nbclausesbeforereduce) {
+ curRestart ++;
reduceDB();
+ nbclausesbeforereduce += 500;
+ }
Lit next = lit_Undef;
while (decisionLevel() < assumptions.size()) {
assert(value(next) == l_Undef);
newDecisionLevel();
uncheckedEnqueue(next);
- if (dynamic_behaviour_analysis) logger.propagation(next, Logger::guess_type);
+ if (dynamic_behaviour_analysis)
+ logger.propagation(next, Logger::guess_type);
return l_Nothing;
}
#endif
int backtrack_level;
+ int nbLevels;
conflicts++;
conflictC++;
return l_False;
}
learnt_clause.clear();
- analyze(confl, learnt_clause, backtrack_level);
+ analyze(confl, learnt_clause, backtrack_level, nbLevels);
+ conf4Stats++;
+
if (dynamic_behaviour_analysis)
logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause);
cancelUntil(backtrack_level);
} else {
Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true);
learnts.push(c);
+ c->setActivity(nbLevels); // LS
+ if (nbLevels <= 2) nbDL2++;
attachClause(*c);
- claBumpActivity(*c);
uncheckedEnqueue(learnt_clause[0], c);
if (dynamic_behaviour_analysis) {
}
varDecayActivity();
- claDecayActivity();
return l_Nothing;
}
model.clear();
conflict.clear();
+ curRestart = 1;
if (!ok) return l_False;
assumps.copyTo(assumptions);
double nof_conflicts = restart_first;
- double nof_learnts = nClauses() * learntsize_factor;
lbool status = l_Undef;
+ if (nClauses() * learntsize_factor < nbclausesbeforereduce) {
+ if (nClauses() * learntsize_factor < nbclausesbeforereduce/2)
+ nbclausesbeforereduce = nbclausesbeforereduce/4;
+ else
+ nbclausesbeforereduce = (nClauses() * learntsize_factor)/2;
+ }
+
toReplace->performReplace();
if (!ok) return l_False;
removeSatisfied(clauses);
cleanClauses(clauses);
uint sumLengths = 0;
- XorFinder xorFinder(this, clauses, xorclauses);
+ 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);
cleanClauses(learnts);
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)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts());
+ 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();
- status = search((int)nof_conflicts, (int)nof_learnts);
+ status = search((int)nof_conflicts);
nof_conflicts *= restart_inc;
- nof_learnts *= learntsize_inc;
for (Gaussian **gauss = &gauss_matrixes[0], **end= gauss + gauss_matrixes.size(); gauss != end; gauss++)
(*gauss)->clear_clauses();
if (conflict.size() == 0)
ok = false;
}
+
+ #ifdef LS_STATS_NBBUMP
+ for(int i=0;i<learnts.size();i++)
+ printf("## %d %d %d\n", learnts[i]->size(),learnts[i]->activity(),
+ (unsigned int)learnts[i]->nbBump());
+ #endif
cancelUntil(0);
return status;
/****************************************************************************************[Solver.h]
MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+glucose -- Gilles Audemard, Laurent Simon (2008)
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
#include "VarReplacer.h"
#include "GaussianConfig.h"
#include "Logger.h"
+#include "constants.h"
namespace MINISAT
{
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
+ template<class T>
+ void removeWatchedCl(vec<T> &ws, const Clause *c);
+ template<class T>
+ bool findWatchedCl(vec<T>& ws, const Clause *c);
+ template<class T>
+ void removeWatchedBinCl(vec<T> &ws, const Clause *c);
+ template<class T>
+ bool findWatchedBinCl(vec<T>& ws, const Clause *c);
// Read state:
//
// Mode of operation:
//
double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95)
- double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999)
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)
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
+ friend class FindUndef;
+ bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef)
void set_gaussian_decision_until(const uint to);
void set_gaussian_decision_from(const uint from);
//
uint64_t starts, decisions, rnd_decisions, propagations, conflicts;
uint64_t clauses_literals, learnts_literals, max_literals, tot_literals;
+ uint64_t nbDL2, nbBin, nbReduceDB;
//Logging
void needStats(); // Prepares the solver to output statistics
const vec<Clause*>& get_learnts() const; //Get all learnt clauses
const vec<Clause*>& get_unitary_learnts() const; //return the set of unitary learned clauses
void dump_sorted_learnts(const char* file);
- friend class FindUndef;
- bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef)
protected:
vector<Gaussian*> gauss_matrixes;
//
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
vec<Clause*> clauses; // List of problem clauses.
- vec<XorClause*> xorclauses; // List of problem xor-clauses.
+ vec<XorClause*> xorclauses; // List of problem xor-clauses. Will not be freed
+ vec<XorClause*> xorclauses_tofree;// List of problem xor-clauses. Will be freed
vec<Clause*> learnts; // List of learnt clauses.
vec<Clause*> unitary_learnts; // List of learnt clauses.
- double cla_inc; // Amount to bump next clause with.
vec<double> activity; // A heuristic measurement of the activity of a variable.
double var_inc; // Amount to bump next variable with.
vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<vec<XorClause*> > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses.
+ vec<vec<WatchedBin> > binwatches;
vec<lbool> assigns; // The current assignments
vector<bool> polarity; // The preferred polarity of each variable.
vector<bool> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
vec<int32_t> trail_lim; // Separator indices for different decision levels in 'trail'.
vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
vec<int32_t> level; // 'level[var]' contains the level at which the assignment was made.
+ vec<Var> permDiff; // LS: permDiff[var] contains the current conflict number... Used to count the number of different decision level variables in learnt clause
+ #ifdef UPDATEVARACTIVITY
+ vec<Lit> lastDecisionLevel;
+ #endif
+ int64_t curRestart;
+ int64_t conf4Stats;
+ int nbclausesbeforereduce;
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
vec<Lit> analyze_stack;
vec<Lit> analyze_toclear;
vec<Lit> add_tmp;
+ unsigned long int MYFLAG;
//Logging
uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause
// Main internal methods:
//
+ //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.
void newDecisionLevel (); // Begins a new decision level.
Clause* propagate (const bool xor_as_well = true); // Perform unit propagation. Returns possibly conflicting clause.
Clause* propagate_xors (const Lit& p);
void cancelUntil (int level); // Backtrack until a certain level.
- void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+ void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel, int &nblevels); // (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_learnts); // Search for a given number of conflicts.
+ lbool search (int nof_conflicts); // Search for a given number of conflicts.
void reduceDB (); // Reduce the set of learnt clauses.
template<class T>
void removeSatisfied (vec<T*>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
void cleanClauses (vec<XorClause*>& cs);
- bool cleanClause (Clause& c) const;
+ bool cleanClause (Clause& c);
void cleanClauses (vec<Clause*>& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses
llbool handle_conflict (vec<Lit>& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause
- llbool new_decision (int& nof_conflicts, int& nof_learnts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made
+ llbool new_decision (int& nof_conflicts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made
// Maintaining Variable/Clause activity:
//
void detachClause (const XorClause& c);
void detachClause (const Clause& c); // Detach a clause to watcher lists.
void detachModifiedClause(const Lit lit1, const Lit lit2, const uint size, const Clause* address);
- template<class T>
- void removeClause(T& c); // Detach and free a clause.
+ void removeClause(Clause& c); // Detach and free a clause.
+ void removeClause(XorClause& c); // Detach and free a clause.
bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
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:
//
order_heap.decrease(v);
}
-inline void Solver::claDecayActivity()
-{
- cla_inc *= clause_decay;
-}
-inline void Solver::claBumpActivity (Clause& c)
-{
- if ( (c.activity() += cla_inc) > 1e20 ) {
- // Rescale:
- for (int i = 0; i < learnts.size(); i++)
- learnts[i]->activity() *= 1e-20;
- 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);
cout << "New decision level:" << trail_lim.size() << endl;
#endif
}
+/*inline int Solver::nbPropagated(int level) {
+ if (level == decisionLevel())
+ return trail.size() - trail_lim[level-1] - 1;
+ return trail_lim[level] - trail_lim[level-1] - 1;
+}*/
inline int Solver::decisionLevel () const
{
return trail_lim.size();
}
cs.shrink(i - j);
}
+template <class T>
+inline void Solver::removeWatchedCl(vec<T> &ws, const Clause *c) {
+ int j = 0;
+ for (; j < ws.size() && ws[j] != c; j++);
+ assert(j < ws.size());
+ for (; j < ws.size()-1; j++) ws[j] = ws[j+1];
+ ws.pop();
+}
+template <class T>
+inline void Solver::removeWatchedBinCl(vec<T> &ws, const Clause *c) {
+ int j = 0;
+ for (; j < ws.size() && ws[j].clause != c; j++);
+ assert(j < ws.size());
+ for (; j < ws.size()-1; j++) ws[j] = ws[j+1];
+ ws.pop();
+}
template<class T>
-void Solver::removeClause(T& c)
+inline bool Solver::findWatchedCl(vec<T>& ws, const Clause *c)
+{
+ int j = 0;
+ for (; j < ws.size() && ws[j] != c; j++);
+ return j < ws.size();
+}
+template<class T>
+inline bool Solver::findWatchedBinCl(vec<T>& ws, const Clause *c)
+{
+ int j = 0;
+ for (; j < ws.size() && ws[j].clause != c; j++);
+ return j < ws.size();
+}
+inline void Solver::reverse_binary_clause(Clause& c) const {
+ if (c.size() == 2 && value(c[0]) == l_False) {
+ assert(value(c[1]) == l_True);
+ Lit tmp = c[0];
+ 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);
free(&c);
}
+inline void Solver::removeClause(XorClause& c)
+{
+ detachClause(c);
+ c.mark(1);
+}
//=================================================================================================
-CryptoMiniSat SVN revision: r454 , GIT revision: 91b7fc803564cfd5e5af363c81c1c68bdced162b
+CryptoMiniSat
+SVN revision: r484
+GIT revision: 36a94d9b25be76b24dd26a413928a3ae559c3983
+
case 0: {
if (!c.xor_clause_inverted())
S->ok = false;
- free(&c);
r++;
break;
}
case 1: {
S->uncheckedEnqueue(Lit(c[0].var(), !c.xor_clause_inverted()));
- free(&c);
r++;
break;
}
default: {
- S->attachClause(c);
- *a++ = *r++;
+ if (c.size() == 2) {
+ S->addBinaryXorClause(c, c.xor_clause_inverted(), c.group);
+ c.mark(1);
+ r++;
+ } else {
+ S->attachClause(c);
+ *a++ = *r++;
+ }
break;
}
}
//triangular cycle
if (lit1.var() == lit2.var()) {
- if (lit1.sign() ^ lit2.sign() != lit.sign()) {
+ if ((lit1.sign() ^ lit2.sign()) != lit.sign()) {
#ifdef VERBOSE_DEBUG
cout << "Inverted cycle in var-replacement -> UNSAT" << endl;
#endif
using std::make_pair;
-XorFinder::XorFinder(Solver* _S, vec<Clause*>& _cls, vec<XorClause*>& _xorcls) :
+XorFinder::XorFinder(Solver* _S, vec<Clause*>& _cls) :
cls(_cls)
- , xorcls(_xorcls)
, S(_S)
{
}
}
default: {
XorClause* x = XorClause_new(lits, impair, old_group);
- xorcls.push(x);
+ S->xorclauses.push(x);
+ S->xorclauses_tofree.push(x);
S->attachClause(*x);
#ifdef VERBOSE_DEBUG
{
public:
- XorFinder(Solver* S, vec<Clause*>& cls, vec<XorClause*>& xorcls);
+ XorFinder(Solver* S, vec<Clause*>& cls);
uint doByPart(uint& sumLengths, const uint minSize, const uint maxSize);
uint doNoPart(uint& sumLengths, const uint minSize, const uint maxSize);
void clearToRemove();
vec<Clause*>& cls;
- vec<XorClause*>& xorcls;
bool clauseEqual(const Clause& c1, const Clause& c2) const;
bool impairSigns(const Clause& c) const;
--- /dev/null
+#define RATIOREMOVECLAUSES 2
+#define NBCLAUSESBEFOREREDUCE 20000
+#define DYNAMICNBLEVEL
+#define CONSTANTREMOVECLAUSE
+#define UPDATEVARACTIVITY
+#define BLOCK
projects / francis / stp.git / commitdiff