Adding phase-caching to minisat.

(A Lightweight Component Caching Scheme for Satisfiability Solvers <http://www.springerlink.com/content/y802q03263x84159/>)

diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 771d79f62a30eb78bb6932c76f0a466c33a24f4a..dd5e1e66719cbc54939c49962011cc851d016fe1 100644 (file)
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -394,9 +394,10 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
 void Solver::uncheckedEnqueue(Lit p, Clause* from)
 {
     assert(value(p) == l_Undef);
-    assigns [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
-    level   [var(p)] = decisionLevel();
-    reason  [var(p)] = from;
+    assigns  [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
+    level    [var(p)] = decisionLevel();
+    reason   [var(p)] = from;
+    polarity [var(p)] = sign(p);
     trail.push(p);
 }
 

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 1cd5d0bfe0f43d7f6794f4f8b9fd8b9d17f1db2b..2468990f2ea322c81fa684134b3cdde6d7c2f276 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -109,6 +109,8 @@ class SatSolver {
       d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
       // Do not delete the satisfied clauses, just the learnt ones
       d_minisat->remove_satisfied = false;
+      // Make minisat reuse the literal values
+      d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
     }
 
     ~SatSolver() {