diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-04 18:45:15 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-04 18:45:15 +0000 |
| commit | 45b7c76aba6ac71726fb2bf46c45ad7ce6bc8c99 (patch) | |
| tree | 2b324f278e1078bbd9f15dd5b3471a302f8a5c27 | |
| parent | 5efc0cd28524a45b8fb25c4b1c0f8c42830fc3ef (diff) | |
Adding phase-caching to minisat.
(A Lightweight Component Caching Scheme for Satisfiability Solvers <http://www.springerlink.com/content/y802q03263x84159/>)
| -rw-r--r-- | src/prop/minisat/core/Solver.C | 7 | ||||
| -rw-r--r-- | 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<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 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() { |