From 45b7c76aba6ac71726fb2bf46c45ad7ce6bc8c99 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 4 Mar 2010 18:45:15 +0000 Subject: [PATCH] Adding phase-caching to minisat. (A Lightweight Component Caching Scheme for Satisfiability Solvers ) --- src/prop/minisat/core/Solver.C | 7 ++++--- src/prop/sat.h | 2 ++ 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index 771d79f62..dd5e1e667 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -394,9 +394,10 @@ void Solver::analyzeFinal(Lit p, vec& 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 1cd5d0bfe..2468990f2 100644 --- 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() { -- 2.30.2