From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 22 Dec 2009 18:41:33 +0000 (+0000)
Subject: Updating CMS2 to r681, fixing multiple bugs, and adding some polish
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=29a288b6840a519c5f2e4569dd0885cb475e257a;p=francis%2Fstp.git

Updating CMS2 to r681, fixing multiple bugs, and adding some polish

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@539 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp
index f3040a1..49c12cd 100644
--- a/src/sat/cryptominisat2/Conglomerate.cpp
+++ b/src/sat/cryptominisat2/Conglomerate.cpp
@@ -37,8 +37,8 @@ namespace MINISAT
 {
 using namespace MINISAT;
 
-Conglomerate::Conglomerate(Solver *_S) :
-    S(_S)
+Conglomerate::Conglomerate(Solver *_s) :
+    S(_s)
 {}
 
 Conglomerate::~Conglomerate()
diff --git a/src/sat/cryptominisat2/FindUndef.cpp b/src/sat/cryptominisat2/FindUndef.cpp
index 7d7b0a2..8710ee3 100644
--- a/src/sat/cryptominisat2/FindUndef.cpp
+++ b/src/sat/cryptominisat2/FindUndef.cpp
@@ -23,8 +23,8 @@ along with this program.  If not, see <http://www.gnu.org/licenses/>.
 namespace MINISAT
 {
 
-FindUndef::FindUndef(Solver& _S) :
-    S(_S)
+FindUndef::FindUndef(Solver& _s) :
+    S(_s)
     , isPotentialSum(0)
 {
     dontLookAtClause.resize(S.clauses.size(), false);
diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp
index 9dc5748..3a64273 100644
--- a/src/sat/cryptominisat2/Gaussian.cpp
+++ b/src/sat/cryptominisat2/Gaussian.cpp
@@ -134,7 +134,7 @@ uint Gaussian::select_columnorder(vector<uint16_t>& var_to_col, matrixset& origM
     uint num_xorclauses  = 0;
     for (uint32_t i = 0; i != xorclauses.size(); i++) {
         #ifdef DEBUG_GAUSS
-        assert(xorclauses[i]->mark() || !solver.satisfied(*xorclauses[i]));
+        assert(xorclauses[i]->mark() || !Solver.cpplauseCleaner->satisfied(*xorclauses[i]));
         #endif
         if (!xorclauses[i]->mark()) {
             num_xorclauses++;
@@ -158,11 +158,10 @@ uint Gaussian::select_columnorder(vector<uint16_t>& var_to_col, matrixset& origM
     origMat.var_is_set.setZero();
 
     origMat.col_to_var.clear();
-    for (int i = solver.order_heap.size()-1; i >= 0 ; i--)
-        //for inverse order:
-        //for (int i = 0; i < order_heap.size() ; i++)
+    Heap<Solver::VarOrderLt> order_heap(solver.order_heap);
+    while (!order_heap.empty())
     {
-        Var v = solver.order_heap[i];
+        Var v = order_heap.removeMin();
 
         if (var_to_col[v] == 1) {
             #ifdef DEBUG_GAUSS
@@ -206,11 +205,11 @@ void Gaussian::fill_matrix(matrixset& 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();
+    memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size());
 
     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);
-    origMat.past_the_end_last_one_in_col = origMat.num_cols;
+    origMat.first_one_in_row.resize(origMat.num_rows);
     
     origMat.removeable_cols = 0;
     origMat.least_column_changed = -1;
@@ -249,17 +248,17 @@ void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint col)
     uint row_num = 0;
 
     if (solver.assigns[var].getBool()) {
-        for (uint end = m.last_one_in_col[col];  row_num != end && row_num != m.num_rows; ++this_row, row_num++) {
+        for (uint end = m.last_one_in_col[col];  row_num != end; ++this_row, row_num++) {
             if ((*this_row)[col]) {
-                changed_rows.setBit(row_num);
+                changed_rows[row_num] = true;
                 (*this_row).invert_is_true();
                 (*this_row).clearBit(col);
             }
         }
     } else {
-        for (uint end = m.last_one_in_col[col];  row_num != end && row_num != m.num_rows; ++this_row, row_num++) {
+        for (uint end = m.last_one_in_col[col];  row_num != end; ++this_row, row_num++) {
             if ((*this_row)[col]) {
-                changed_rows.setBit(row_num);
+                changed_rows[row_num] = true;
                 (*this_row).clearBit(col);
             }
         }
@@ -267,7 +266,7 @@ void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint col)
 
     #ifdef DEBUG_GAUSS
     bool c = false;
-    for(PackedMatrix::iterator r = m.matrix.begin(), end = r + m.matrix.getSize(); r != end; ++r)
+    for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = r + m.matrix.getSize(); r != end; ++r)
         c |= (*r)[col];
     assert(!c);
     #endif
@@ -290,7 +289,7 @@ void Gaussian::update_matrix_by_col_all(matrixset& m)
     assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m));
     #endif
     
-    changed_rows.setZero();
+    memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size());
 
     uint last = 0;
     uint col = 0;
@@ -305,10 +304,9 @@ void Gaussian::update_matrix_by_col_all(matrixset& m)
             last = 0;
     }
     m.num_cols -= 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, m);
+    check_matrix_against_varset(m.matrix, m);
     #endif
 
     #ifdef VERBOSE_DEBUG
@@ -323,6 +321,12 @@ void Gaussian::update_matrix_by_col_all(matrixset& m)
     cout << "removeable cols:" << m.removeable_cols << endl;*/
 }
 
+inline void Gaussian::update_last_one_in_col(matrixset& m)
+{
+    for (uint16_t* i = &m.last_one_in_col[0]+m.last_one_in_col.size()-1, *end = &m.last_one_in_col[0]-1; i != end && *i >= m.num_rows; i--)
+        *i = m.num_rows;
+}
+
 Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
 {
     if (solver.decisionLevel() >= badlevel)
@@ -337,6 +341,7 @@ Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
         assert(level < matrix_sets.size());
         cur_matrixset = matrix_sets[level];
     }
+    update_last_one_in_col(cur_matrixset);
     update_matrix_by_col_all(cur_matrixset);
 
     messed_matrix_vars_since_reversal = false;
@@ -347,7 +352,7 @@ Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
     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, cur_matrixset);
+    check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset);
     #endif
     
     gaussian_ret ret;
@@ -361,6 +366,9 @@ Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
     } else {*/
         ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl);
     //}
+    #ifdef DEBUG_GAUSS
+    assert(ret == conflict || nothing_to_propagate(cur_matrixset));
+    #endif
     
     if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) {
         badlevel = solver.decisionLevel();
@@ -410,26 +418,33 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
 
     uint i = 0;
     uint j = m.least_column_changed + 1;
+    PackedMatrix::iterator beginIt = m.matrix.beginMatrix();
+    PackedMatrix::iterator rowIt = m.matrix.beginMatrix();
 
+    #ifdef DEBUG_GAUSS
+    check_first_one_in_row(m, j);
+    #endif
+    
     if (j) {
         uint16_t until = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows);
-        if (j > m.past_the_end_last_one_in_col)
+        if (j-1 > m.first_one_in_row[m.num_rows-1])
             until = m.num_rows;
-        for (;i != until; i++) if (changed_rows[i] && m.matrix.getMatrixAt(i).popcnt_is_one())
+        for (;i != until; i++, ++rowIt) if (changed_rows[i] && (*rowIt).popcnt_is_one(m.first_one_in_row[i]))
             propagatable_rows.push(i);
     }
     
-    if (j > m.past_the_end_last_one_in_col) {
+    #ifdef VERBOSE_DEBUG
+    cout << "At while() start: i,j = " << i << ", " << j << endl;
+    cout << "num_rows:" << m.num_rows << " num_cols:" << m.num_cols << endl;
+    #endif
+    
+    if (j > m.num_cols) {
         #ifdef VERBOSE_DEBUG
         cout << "Going straight to finish" << endl;
         #endif
         goto finish;
     }
     
-    #ifdef VERBOSE_DEBUG
-    cout << "At while() start: i,j = " << i << ", " << j << endl;
-    #endif
-    
     #ifdef DEBUG_GAUSS
     assert(i <= m.num_rows && j <= m.num_cols);
     #endif
@@ -442,19 +457,17 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
             continue;
         }
 
-        PackedMatrix::iterator this_matrix_row = m.matrix.beginMatrix() + i;
-        PackedMatrix::iterator end = m.matrix.beginMatrix() + std::min(m.last_one_in_col[j], m.num_rows);
+        PackedMatrix::iterator this_matrix_row = rowIt;
+        PackedMatrix::iterator end = beginIt + m.last_one_in_col[j];
         for (; this_matrix_row != end; ++this_matrix_row) {
             if ((*this_matrix_row)[j])
                 break;
         }
-        uint best_row = this_matrix_row - m.matrix.beginMatrix();
 
         if (this_matrix_row != end) {
-            PackedRow matrix_row_i = m.matrix.getMatrixAt(i);
 
             //swap rows i and maxi, but do not change the value of i;
-            if (i != best_row) {
+            if (this_matrix_row != rowIt) {
                 #ifdef VERBOSE_DEBUG
                 no_exchanged++;
                 #endif
@@ -464,14 +477,14 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
                 //    conflict_row = i;
                 //    return 0;
                 //}
-                matrix_row_i.swapBoth(*this_matrix_row);
+                (*rowIt).swapBoth(*this_matrix_row);
             }
             #ifdef DEBUG_GAUSS
-            assert(m.matrix[i].popcnt(j) == m.matrix[i].popcnt());
-            assert(m.matrix[i][j]);
+            assert(m.matrix.getMatrixAt(i).popcnt(j) == m.matrix.getMatrixAt(i).popcnt());
+            assert(m.matrix.getMatrixAt(i)[j]);
             #endif
 
-            if (matrix_row_i.popcnt_is_one(j))
+            if ((*rowIt).popcnt_is_one(j))
                 propagatable_rows.push(i);
 
             //Now A[i,j] will contain the old value of A[maxi,j];
@@ -483,21 +496,23 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
                 number_of_row_additions++;
                 #endif
                 
-                (*this_matrix_row).xorBoth(matrix_row_i);
+                (*this_matrix_row).xorBoth(*rowIt);
                 //Would early abort, but would not find the best conflict (and would be expensive)
                 //if (it->is_true() &&it->isZero()) {
                 //    conflict_row = i2;
                 //    return 0;
                 //}
             }
+            m.first_one_in_row[i] = j;
             i++;
+            ++rowIt;
             m.last_one_in_col[j] = i;
-        } else
+        } else {
+            m.first_one_in_row[i] = j;
             m.last_one_in_col[j] = i + 1;
+        }
         j++;
     }
-
-    m.past_the_end_last_one_in_col = j;
     
     finish:
 
@@ -515,14 +530,14 @@ uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
     assert(check_last_one_in_cols(m));
     uint row = 0;
     uint col = 0;
-    for (; col < m.num_cols && row < m.num_rows && row < i && col < m.past_the_end_last_one_in_col; col++) {
-        assert(m.matrix[row].popcnt() == m.matrix[row].popcnt(col));
-        assert(!(m.col_to_var[col] == unassigned_var && m.matrix[row][col]));
-        if (m.col_to_var[col] == unassigned_var || !m.matrix[row][col]) {
+    for (; col < m.num_cols && row < m.num_rows && row < i ; col++) {
+        assert(m.matrix.getMatrixAt(row).popcnt() == m.matrix.getMatrixAt(row).popcnt(col));
+        assert(!(m.col_to_var[col] == unassigned_var && m.matrix.getMatrixAt(row)[col]));
+        if (m.col_to_var[col] == unassigned_var || !m.matrix.getMatrixAt(row)[col]) {
             #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.col_to_var[col] == unassigned_var || std::min(m.last_one_in_col[col]-1, (int)m.num_rows) == row);
+            assert(m.col_to_var[col] == unassigned_var || std::min((uint16_t)(m.last_one_in_col[col]-1), m.num_rows) == row);
             continue;
         }
         row++;
@@ -593,7 +608,7 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint
 
     for (uint row = last_row; row != m.num_rows; row++) {
         #ifdef DEBUG_GAUSS
-        assert(m.matrix[row].isZero());
+        assert(m.matrix.getMatrixAt(row).isZero());
         #endif
         if (m.matrix.getMatrixAt(row).is_true())
             analyse_confl(m, row, maxlevel, size, best_row);
@@ -604,6 +619,11 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint
 
     #ifdef DEBUG_GAUSS
     assert(check_no_conflict(m));
+    assert(last_row == 0 || !m.matrix.getMatrixAt(last_row-1).isZero());
+    #endif
+    
+    #ifdef VERBOSE_DEBUG
+    cout << "Resizing matrix to num_rows = " << last_row << endl;
     #endif
     m.num_rows = last_row;
     m.matrix.resizeNumRows(m.num_rows);
@@ -651,7 +671,7 @@ void Gaussian::cancel_until_sublevel(const uint sublevel)
     for (Gaussian **gauss = &(solver.gauss_matrixes[0]), **end= gauss + solver.gauss_matrixes.size(); gauss != end; gauss++)
         if (*gauss != this) (*gauss)->canceling(sublevel);
 
-    for (int level = solver.trail.size()-1; level >= sublevel; level--) {
+    for (int level = solver.trail.size()-1; level >= (int)sublevel; level--) {
         Var     var  = solver.trail[level].var();
         #ifdef VERBOSE_DEBUG
         cout << "(" << matrix_no << ")Canceling var " << var+1 << endl;
@@ -675,11 +695,11 @@ void Gaussian::analyse_confl(const matrixset& m, const uint row, uint& maxlevel,
     #ifdef VERBOSE_DEBUG
     cout << "(" << matrix_no << ")matrix conflict found!" << endl;
     cout << "(" << matrix_no << ")conflict clause's vars: ";
-    print_matrix_row_with_assigns(m.varset[row]);
+    print_matrix_row_with_assigns(m.matrix.getVarsetAt(row));
     cout << endl;
     
     cout << "(" << matrix_no << ")corresponding matrix's row (should be empty): ";
-    print_matrix_row(m.matrix[row]);
+    print_matrix_row(m.matrix.getMatrixAt(row));
     cout << endl;
     #endif
 
@@ -737,9 +757,9 @@ Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row
 {
     #ifdef VERBOSE_DEBUG
     cout << "(" << matrix_no << ")matrix prop found!" << endl;
-    cout << m.matrix[row] << endl;
+    cout << m.matrix.getMatrixAt(row) << endl;
     cout << "(" << matrix_no << ")matrix row:";
-    print_matrix_row(m.matrix[row]);
+    print_matrix_row(m.matrix.getMatrixAt(row));
     cout << endl;
     #endif
 
@@ -848,7 +868,7 @@ void Gaussian::print_matrix_row(const T& row) const
         else cout << col_to_var_original[var]+1 << ", ";
         var++;
     }
-    if (!row.is_true()) cout << "xor_clause_inverted";
+    cout << "final:" << row.is_true() << endl;;
 }
 
 template<class T>
@@ -937,7 +957,6 @@ void Gaussian::print_last_one_in_cols(matrixset& m) const
     for (uint i = 0; i < m.num_cols; i++) {
         cout << "last_one_in_col[" << i << "]-1 = " << m.last_one_in_col[i]-1 << endl;
     }
-    cout << "m.past_the_end_last_one_in_col:" <<  m.past_the_end_last_one_in_col << endl;
 }
 
 const bool Gaussian::nothing_to_propagate(matrixset& m) const
@@ -971,10 +990,8 @@ const bool Gaussian::check_last_one_in_cols(matrixset& m) const
     return true;
 }
 
-const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMatrix& varset, const matrixset& m) const
+const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, const matrixset& m) const
 {
-    assert(matrix.getSize() == varset.getSize());
-    
     for (uint i = 0; i < matrix.getSize(); i++) {
         const PackedRow mat_row = matrix.getMatrixAt(i);
         const PackedRow var_row = matrix.getVarsetAt(i);
@@ -1012,6 +1029,38 @@ const bool Gaussian::check_matrix_against_varset(PackedMatrix& matrix, PackedMat
     }
 }
 
+const void Gaussian::check_first_one_in_row(matrixset& m, const uint j)
+{
+    if (j) {
+        uint16_t until2 = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows);
+        if (j-1 > m.first_one_in_row[m.num_rows-1]) {
+            until2 = m.num_rows;
+            #ifdef VERBOSE_DEBUG
+            cout << "j-1 > m.first_one_in_row[m.num_rows-1]" << "j:" << j << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl;
+            #endif
+        }
+        for (uint i2 = 0; i2 != until2; i2++) {
+            #ifdef VERBOSE_DEBUG
+            cout << endl << "row " << i2 << " (num rows:" << m.num_rows << ")" << endl;
+            cout << m.matrix.getMatrixAt(i2) << endl;
+            cout << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl;
+            cout << "first_one_in_row:" << m.first_one_in_row[i2] << endl;
+            cout << "num_cols:" << m.num_cols << endl;
+            cout << "popcnt:" << m.matrix.getMatrixAt(i2).popcnt() << endl;
+            cout << "popcnt_is_one():" << m.matrix.getMatrixAt(i2).popcnt_is_one() << endl;
+            cout << "popcnt_is_one("<< m.first_one_in_row[i2] <<"): " << m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]) << endl;
+            #endif
+            
+            for (uint i3 = 0; i3 < m.first_one_in_row[i2]; i3++) {
+                assert(m.matrix.getMatrixAt(i2)[i3] == 0);
+            }
+            assert(m.matrix.getMatrixAt(i2)[m.first_one_in_row[i2]]);
+            assert(m.matrix.getMatrixAt(i2).popcnt_is_one() ==
+            m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]));
+        }
+    }
+}
+
 const uint Gaussian::get_called() const
 {
     return called;
diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h
index 309345d..242a156 100644
--- a/src/sat/cryptominisat2/Gaussian.h
+++ b/src/sat/cryptominisat2/Gaussian.h
@@ -29,6 +29,9 @@ namespace MINISAT
 {
 using namespace MINISAT;
 
+//#define VERBOSE_DEBUG
+//#define DEBUG_GAUSS
+
 #ifdef VERBOSE_DEBUG
 using std::vector;
 using std::cout;
@@ -40,8 +43,6 @@ class Clause;
 static const uint16_t unassigned_col = -1;
 static const Var unassigned_var = -1;
 
-//#define VERBOSE_DEBUG
-//#define DEBUG_GAUSS
 class Gaussian
 {
 public:
@@ -87,8 +88,8 @@ protected:
         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+1 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> first_one_in_row;
         uint removeable_cols; // the number of columns that have been zeroed out (i.e. assigned)
     };
 
@@ -104,7 +105,7 @@ protected:
     
     //State of current elimnation
     vec<uint> propagatable_rows; //used to store which rows were deemed propagatable during elimination
-    BitArray changed_rows; //used to store which rows were deemed propagatable during elimination
+    vector<unsigned char> changed_rows; //used to store which rows were deemed propagatable during elimination
 
     //Statistics
     uint useful_prop; //how many times Gauss gave propagation as a result
@@ -143,6 +144,7 @@ protected:
     bool should_check_gauss(const uint decisionlevel, const uint starts) const;
     void disable_if_necessary();
     void reset_stats();
+    void update_last_one_in_col(matrixset& m);
     
 private:
     
@@ -153,8 +155,9 @@ private:
     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 matrixset& m) const;
+    const bool check_matrix_against_varset(PackedMatrix& matrix,const matrixset& m) const;
     const bool check_last_one_in_cols(matrixset& m) const;
+    const void check_first_one_in_row(matrixset& m, const uint j);
     void print_matrix(matrixset& m) const;
     void print_last_one_in_cols(matrixset& m) const;
     static const string lbool_to_string(const lbool toprint);
diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp
index 857a481..a74f12c 100644
--- a/src/sat/cryptominisat2/Logger.cpp
+++ b/src/sat/cryptominisat2/Logger.cpp
@@ -64,12 +64,12 @@ Logger::Logger(int& _verbosity) :
 {
     runid /= 10;
     runid = time(NULL) % 10000;
-    if (verbosity >= 1) printf("RunID is: #%d\n",runid);
+    if (verbosity >= 1) printf("c RunID is: #%d\n",runid);
 }
 
-void Logger::setSolver(const Solver* _S)
+void Logger::setSolver(const Solver* _s)
 {
-    S = _S;
+    S = _s;
 }
 
 // Adds a new variable to the knowledge of the logger
@@ -101,8 +101,9 @@ void Logger::new_group(const uint group)
 void Logger::cut_name_to_size(string& name) const
 {
     uint len = name.length();
-    if (len > 0 && name[len-1] == '\r') {
+    while(len > 0 && (name[len-1] == ' ' || name[len-1] == 0x0A || name[len-1] == 0x0D)) {
         name[len-1] = '\0';
+        name.resize(len-1);
         len--;
     }
     
@@ -704,7 +705,20 @@ void Logger::print_general_stats() const
     print_line("Avg. literals per learnt clause",(double)S->learnts_literals/(double)S->nLearnts());
     print_line("Progress estimate (%):", S->progress_estimate*100.0);
     print_line("All unitary learnts until now", S->get_unitary_learnts_num());
-    
+    print_footer();
+}
+
+void Logger::print_learnt_unitaries(const uint from, const string display) const
+{
+    print_footer();
+    print_simple_line(display);
+    print_header("var", "name", "value");
+    for (uint i = from; i < S->trail.size(); i++) {
+        Var var = S->trail[i].var();
+        bool sign = S->trail[i].sign();
+        std::stringstream ss;
+        print_line(var+1, varnames[var], sign);
+    }
     print_footer();
 }
 
@@ -738,6 +752,8 @@ void Logger::printstats() const
     print_branch_depth_distrib();
     print_learnt_clause_distrib();
     print_matrix_stats();
+    print_learnt_unitaries(0," Unitary clauses learnt until now");
+    print_learnt_unitaries(last_unitary_learnt_clauses, " Unitary clauses during this restart");
     print_advanced_stats();
     print_general_stats();
 }
diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h
index b7d5ad9..f0dca86 100644
--- a/src/sat/cryptominisat2/Logger.h
+++ b/src/sat/cryptominisat2/Logger.h
@@ -98,6 +98,7 @@ private:
     void print_statistics_note() const;
     void print_matrix_stats() const;
     void print_general_stats() const;
+    void print_learnt_unitaries(const uint from, const string display) const;
 
     uint max_print_lines;
     template<class T>
diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp
index 07d1ff8..b196a55 100644
--- a/src/sat/cryptominisat2/MatrixFinder.cpp
+++ b/src/sat/cryptominisat2/MatrixFinder.cpp
@@ -39,9 +39,9 @@ using std::endl;
 
 //#define PART_FINDING
 
-MatrixFinder::MatrixFinder(Solver *_S) :
-    unAssigned(_S->nVars() + 1)
-    , S(_S)
+MatrixFinder::MatrixFinder(Solver *_s) :
+    unAssigned(_s->nVars() + 1)
+    , S(_s)
 {
 }
 
@@ -182,13 +182,13 @@ const uint MatrixFinder::setMatrixes()
             && realMatrixNum < 3)
         {
             if (S->verbosity >=1)
-                cout << "|  Matrix no " << std::setw(4) << realMatrixNum;
+                cout << "c |  Matrix no " << std::setw(4) << realMatrixNum;
             S->gauss_matrixes.push_back(new Gaussian(*S, S->gaussconfig, realMatrixNum, xorsInMatrix[i]));
             realMatrixNum++;
             
         } else {
             if (S->verbosity >=1  && numXorInMatrix[a].second >= 20)
-                cout << "|  Unused Matrix ";
+                cout << "c |  Unused Matrix ";
         }
         if (S->verbosity >=1 && numXorInMatrix[a].second >= 20) {
             cout << std::setw(5) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size();
diff --git a/src/sat/cryptominisat2/PackedRow.cpp b/src/sat/cryptominisat2/PackedRow.cpp
index 22c88ca..e9356eb 100644
--- a/src/sat/cryptominisat2/PackedRow.cpp
+++ b/src/sat/cryptominisat2/PackedRow.cpp
@@ -24,7 +24,7 @@ std::ostream& operator << (std::ostream& os, const PackedRow& m)
     for(uint i = 0; i < m.size*64; i++) {
         os << m[i];
     }
-    os << " -- xor: " << !m.is_true();
+    os << " -- xor: " << m.is_true();
     return os;
 }
 
diff --git a/src/sat/cryptominisat2/PackedRow.h b/src/sat/cryptominisat2/PackedRow.h
index 0fa9905..4c2d67d 100644
--- a/src/sat/cryptominisat2/PackedRow.h
+++ b/src/sat/cryptominisat2/PackedRow.h
@@ -100,14 +100,10 @@ public:
             uint64_t tmp = mp[i];
             while(tmp) {
                 popcount += tmp & 1;
-                popcount += tmp & 2;
-                popcount += tmp & 4;
-                popcount += tmp & 8;
-                if (popcount > 1) return false;
-                tmp >>= 4;
+                tmp >>= 1;
             }
         }
-        return popcount;
+        return popcount == 1;
     }
     
     bool popcnt_is_one(uint from) const
@@ -130,10 +126,8 @@ public:
 
     inline const bool isZero() const
     {
-        const uint64_t*  mp2 = (const uint64_t*)mp;
-        
         for (uint i = 0; i != size; i++) {
-            if (mp2[i]) return false;
+            if (mp[i]) return false;
         }
         return true;
     }
@@ -158,29 +152,6 @@ public:
         mp[i/64] |= ((uint64_t)1 << (i%64));
     }
     
-    void swap(PackedRow b)
-    {
-        #ifdef DEBUG_ROW
-        assert(size > 0);
-        assert(b.size > 0);
-        assert(b.size == size);
-        #endif
-        
-        uint64_t * __restrict mp1 = mp-1;
-        uint64_t * __restrict mp2 = b.mp-1;
-        
-        uint i = size+1;
-        
-        while(i != 0) {
-            uint64_t tmp(*mp2);
-            *mp2 = *mp1;
-            *mp1 = tmp;
-            mp1++;
-            mp2++;
-            i--;
-        }
-    }
-    
     void swapBoth(PackedRow b)
     {
         #ifdef DEBUG_ROW
@@ -195,9 +166,7 @@ public:
         uint i = 2*(size+1);
         
         while(i != 0) {
-            uint64_t tmp(*mp2);
-            *mp2 = *mp1;
-            *mp1 = tmp;
+            std::swap(*mp1, *mp2);
             mp1++;
             mp2++;
             i--;
diff --git a/src/sat/cryptominisat2/RestartTypeChooser.cpp b/src/sat/cryptominisat2/RestartTypeChooser.cpp
index 960c3e7..f198479 100644
--- a/src/sat/cryptominisat2/RestartTypeChooser.cpp
+++ b/src/sat/cryptominisat2/RestartTypeChooser.cpp
@@ -24,8 +24,8 @@ namespace MINISAT
 {
 using namespace MINISAT;
 
-RestartTypeChooser::RestartTypeChooser(const Solver* const _S) :
-    S(_S)
+RestartTypeChooser::RestartTypeChooser(const Solver* const _s) :
+    S(_s)
     , topX(100)
     , limit(30)
 {
@@ -74,7 +74,7 @@ void RestartTypeChooser::calcHeap()
     std::cout << "First vars:" << std::endl;
     #endif
     Heap<Solver::VarOrderLt> tmp(S->order_heap);
-    uint thisTopX = std::min(S->order_heap.size(), (int)topX);
+    uint thisTopX = std::min(S->order_heap.size(), topX);
     for (uint i = 0; i != thisTopX; i++) {
         #ifdef VERBOSE_DEBUG
         std::cout << tmp.removeMin()+1 << ", ";
diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index acae0cb..0a2b5c4 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -60,7 +60,7 @@ Solver::Solver() :
         , xorFinder        (true)
         , performReplace   (true)
         , greedyUnbound    (false)
-        , restartType       (static_restart)
+        , fixRestartType   (auto_restart)
 
         // Statistics: (formerly in 'SolverStats')
         //
@@ -83,6 +83,7 @@ Solver::Solver() :
         , progress_estimate(0)
         , remove_satisfied (true)
         , mtrand((unsigned long int)0)
+        , restartType      (static_restart)
         #ifdef STATS_NEEDED
         , logger(verbosity)
         , dynamic_behaviour_analysis(false) //do not document the proof as default
@@ -1323,6 +1324,8 @@ inline void Solver::chooseRestartType(const lbool& status, RestartTypeChooser& r
 {
     if (status.isUndef() && starts > 2 && starts < 8) {
         RestartType tmp = restartTypeChooser.choose();
+        if (fixRestartType != auto_restart)
+            tmp = fixRestartType;
         if (starts == 7) {
             if (tmp == dynamic_restart) {
                 nbDecisionLevelHistory.fastclear();
@@ -1330,10 +1333,10 @@ inline void Solver::chooseRestartType(const lbool& status, RestartTypeChooser& r
                 totalSumOfDecisionLevel = 0;
                 clearGaussMatrixes();
                 if (verbosity >= 1)
-                    printf("|                           Decided on dynamic restart strategy                         |\n");
+                    printf("c |                           Decided on dynamic restart strategy                         |\n");
             } else  {
                 if (verbosity >= 1)
-                    printf("|                            Decided on static restart strategy                         |\n");
+                    printf("c |                            Decided on static restart strategy                         |\n");
             }
             restartType = tmp;
         }
@@ -1376,7 +1379,7 @@ inline void Solver::performStepsBeforeSolve()
             time = cpuTime();
             uint foundCong = conglomerate->conglomerateXors();
             if (verbosity >=1)
-                printf("|  Conglomerating XORs:  %4.2lf s (removed %6d vars)                         |\n", cpuTime()-time, foundCong);
+                printf("c |  Conglomerating XORs:  %4.2lf s (removed %6d vars)                         |\n", cpuTime()-time, foundCong);
             if (!ok) return;
             
             uint new_total = 0;
@@ -1385,8 +1388,8 @@ inline void Solver::performStepsBeforeSolve()
                 new_total += xorclauses[i]->size();
             }
             if (verbosity >=1) {
-                printf("|  Sum xclauses before: %8d, after: %12d                         |\n", orig_num_cls, new_num_cls);
-                printf("|  Sum xlits before: %11d, after: %12d                         |\n", orig_total, new_total);
+                printf("c |  Sum xclauses before: %8d, after: %12d                         |\n", orig_num_cls, new_num_cls);
+                printf("c |  Sum xlits before: %11d, after: %12d                         |\n", orig_total, new_total);
             }
             
             if (performReplace
@@ -1402,7 +1405,7 @@ inline void Solver::performStepsBeforeSolve()
         MatrixFinder m(this);
         const uint numMatrixes = m.findMatrixes();
         if (verbosity >=1)
-            printf("|  Finding matrixes :    %4.2lf s (found  %5d)                                |\n", cpuTime()-time, numMatrixes);
+            printf("c |  Finding matrixes :    %4.2lf s (found  %5d)                                |\n", cpuTime()-time, numMatrixes);
     }
 }
 
@@ -1477,7 +1480,7 @@ lbool Solver::solve(const vec<Lit>& assumps)
             FindUndef finder(*this);
             const uint unbounded = finder.unRoll();
             if (verbosity >= 1)
-                printf("Greedy unbounding     :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded);
+                printf("c Greedy unbounding     :%5.2lf s, unbounded: %7d vars\n", cpuTime()-time, unbounded);
         }
     } if (status == l_False) {
         if (conflict.size() == 0)
@@ -1563,7 +1566,7 @@ next:
     assert(!failed);
 
     if (verbosity >=1)
-        printf("Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size());
+        printf("c Verified %d clauses.\n", clauses.size() + xorclauses.size() + conglomerate->getCalcAtFinish().size());
 }
 
 
@@ -1590,10 +1593,10 @@ void Solver::printStatHeader() const
     #else
     if (verbosity >= 1) {
     #endif
-        printf("============================[ Search Statistics ]========================================\n");
-        printf("| Conflicts |          ORIGINAL         |          LEARNT          |        GAUSS       |\n");
-        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl | Prop   Confl   On  |\n");
-        printf("=========================================================================================\n");
+        printf("c ============================[ Search Statistics ]========================================\n");
+        printf("c | Conflicts |          ORIGINAL         |          LEARNT          |        GAUSS       |\n");
+        printf("c |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl | Prop   Confl   On  |\n");
+        printf("c =========================================================================================\n");
     }
 }
 
@@ -1604,7 +1607,7 @@ void Solver::printRestartStat() const
     #else
     if (verbosity >= 1) {
     #endif
-        printf("| %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart), (int)nLearnts(), (double)learnts_literals/nLearnts());
+        printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)nClauses(), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart), (int)nLearnts(), (double)learnts_literals/nLearnts());
         print_gauss_sum_stats();
     }
 }
@@ -1616,7 +1619,7 @@ void Solver::printEndSearchStat() const
         #else
         if (verbosity >= 1) {
             #endif
-            printf("====================================================================");
+            printf("c ====================================================================");
             print_gauss_sum_stats();
         }
 }
diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index ec75bce..d4c08c2 100644
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -137,7 +137,7 @@ public:
     bool      performReplace;       // Should var-replacing be performed?
     friend class FindUndef;
     bool      greedyUnbound;        //If set, then variables will be greedily unbounded (set to l_Undef)
-    RestartType restartType;      // If set to true, the restart strategy will be dynamic
+    RestartType fixRestartType;     // If set, the solver will always choose the given restart strategy
     
 
     enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 };
@@ -221,11 +221,12 @@ protected:
     bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
     bqueue<unsigned int> nbDecisionLevelHistory; // Set of last decision level in conflict clauses
     float               totalSumOfDecisionLevel;
-    MTRand mtrand;                        // random number generaton
-    friend class Logger;
+    MTRand              mtrand;           // random number generaton
+    RestartType         restartType;      // Used internally to determine which restart strategy to choose
+    friend class        Logger;
     #ifdef STATS_NEEDED
     Logger logger;                        // dynamic logging, statistics
-    bool dynamic_behaviour_analysis;      // Is logger running?
+    bool                dynamic_behaviour_analysis; // Is logger running?
     #endif
     uint                maxRestarts;      // More than this number of restarts will not be performed
 
diff --git a/src/sat/cryptominisat2/SolverTypes.h b/src/sat/cryptominisat2/SolverTypes.h
index cb5d252..58f61c6 100644
--- a/src/sat/cryptominisat2/SolverTypes.h
+++ b/src/sat/cryptominisat2/SolverTypes.h
@@ -39,7 +39,7 @@ using namespace MINISAT;
 
 typedef uint32_t Var;
 #define var_Undef (0xffffffffU >>1)
-enum RestartType {dynamic_restart, static_restart};
+enum RestartType {dynamic_restart, static_restart, auto_restart};
 
 class Lit
 {
diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 6d08e9c..61c0254 100644
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,3 +1,3 @@
 CryptoMiniSat
-SVN revision: 656
-GIT revision: 87b9139cb43d296de0bd680226607ee7f3e3e755
+SVN revision: 681
+GIT revision: 14117f70a8eaa1c54e813f028252fa4449fdc151
diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 731d702..575a347 100644
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -33,13 +33,13 @@ using std::endl;
 namespace MINISAT
 {
 
-VarReplacer::VarReplacer(Solver *_S) :
+VarReplacer::VarReplacer(Solver *_s) :
     replacedLits(0)
     , lastReplacedLits(0)
     , replacedVars(0)
     , lastReplacedVars(0)
     , addedNewClause(false)
-    , S(_S)
+    , S(_s)
 {
 }
 
@@ -94,7 +94,7 @@ void VarReplacer::performReplace()
     clauses.clear();
     
     if (S->verbosity >=1)
-        printf("|  Replacing   %8d vars, replaced %8d lits                          |\n", replacedVars-lastReplacedVars, replacedLits-lastReplacedLits);
+        printf("c |  Replacing   %8d vars, replaced %8d lits                          |\n", replacedVars-lastReplacedVars, replacedLits-lastReplacedLits);
     
     addedNewClause = false;
     lastReplacedVars = replacedVars;
diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp
index 02ba026..c410157 100644
--- a/src/sat/cryptominisat2/XorFinder.cpp
+++ b/src/sat/cryptominisat2/XorFinder.cpp
@@ -39,10 +39,10 @@ using std::endl;
 
 using std::make_pair;
 
-XorFinder::XorFinder(Solver* _S, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
+XorFinder::XorFinder(Solver* _s, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
     cls(_cls)
     , type(_type)
-    , S(_S)
+    , S(_s)
 {
 }
 
@@ -68,7 +68,7 @@ uint XorFinder::doNoPart(const uint minSize, const uint maxSize)
     uint found = findXors(sumLengths);
     
     if (S->verbosity >=1)
-        printf("|  Finding XORs:        %5.2lf s (found: %7d, avg size: %3.1lf)               |\n", cpuTime()-time, found, (double)sumLengths/(double)found);
+        printf("c |  Finding XORs:        %5.2lf s (found: %7d, avg size: %3.1lf)               |\n", cpuTime()-time, found, (double)sumLengths/(double)found);
     
     if (found > 0) {
         clearToRemove();
diff --git a/src/sat/cryptominisat2/mtl/Heap.h b/src/sat/cryptominisat2/mtl/Heap.h
index 4857b13..64114ae 100644
--- a/src/sat/cryptominisat2/mtl/Heap.h
+++ b/src/sat/cryptominisat2/mtl/Heap.h
@@ -44,7 +44,7 @@ class Heap {
     static inline uint32_t parent(uint32_t i) { return (i-1) >> 1; }
 
 
-    inline void percolateUp(int i)
+    inline void percolateUp(uint32_t i)
     {
         uint32_t x = heap[i];
         while (i != 0 && lt(x, heap[parent(i)])){
@@ -61,7 +61,7 @@ class Heap {
     {
         uint32_t x = heap[i];
         while (left(i) < heap.size()){
-            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
+            uint32_t child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
             if (!lt(heap[child], x)) break;
             heap[i]          = heap[child];
             indices[heap[i]] = i;
@@ -81,15 +81,15 @@ class Heap {
     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());
+        memcpy(heap.getData(), other.heap.getData(), sizeof(uint32_t)*other.heap.size());
         indices.growTo(other.indices.size());
-        memcpy(indices.getData(), other.indices.getData(), sizeof(int)*other.indices.size());
+        memcpy(indices.getData(), other.indices.getData(), sizeof(uint32_t)*other.indices.size());
     }
 
-    int  size      ()          const { return heap.size(); }
+    uint32_t  size      ()          const { return heap.size(); }
     bool empty     ()          const { return heap.size() == 0; }
     bool inHeap    (uint32_t n)     const { return n < indices.size() && indices[n] != UINT32_MAX; }
-    int  operator[](uint32_t index) const { assert(index < heap.size()); return heap[index]; }
+    uint32_t  operator[](uint32_t index) const { assert(index < heap.size()); return heap[index]; }
 
     void decrease  (uint32_t n) { assert(inHeap(n)); percolateUp(indices[n]); }
 
@@ -108,9 +108,9 @@ class Heap {
     }
 
 
-    int  removeMin()
+    uint32_t  removeMin()
     {
-        int x            = heap[0];
+        uint32_t x            = heap[0];
         heap[0]          = heap.last();
         indices[heap[0]] = 0;
         indices[x]       = UINT32_MAX;
@@ -172,7 +172,7 @@ class Heap {
     // COMPAT: should be removed
     void setBounds (uint32_t n) { }
     void increase  (uint32_t n) { decrease(n); }
-    int  getmin    ()      { return removeMin(); }
+    uint32_t  getmin    ()      { return removeMin(); }
 
 };