From 40feb785ee98ead840f043f336a5d403c9752b94 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Mon, 5 Apr 2010 04:00:56 +0000 Subject: STP: Switch to standard C++ file suffix. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100390 91177308-0d34-0410-b5e6-96231b3b80d8 --- stp/sat/Simplifier.C | 542 --------------------------------- stp/sat/Simplifier.cpp | 542 +++++++++++++++++++++++++++++++++ stp/sat/Solver.C | 811 ------------------------------------------------- stp/sat/Solver.cpp | 811 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 1353 insertions(+), 1353 deletions(-) delete mode 100644 stp/sat/Simplifier.C create mode 100644 stp/sat/Simplifier.cpp delete mode 100644 stp/sat/Solver.C create mode 100644 stp/sat/Solver.cpp diff --git a/stp/sat/Simplifier.C b/stp/sat/Simplifier.C deleted file mode 100644 index 1c192e20..00000000 --- a/stp/sat/Simplifier.C +++ /dev/null @@ -1,542 +0,0 @@ -/************************************************************************************[Simplifier.C] -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 "Solver.h" - -namespace MINISAT { - -static const int grow = 0; - -//#define WEAKEN -//#define MATING -//#define ASSYMM - -bool Solver::assymmetricBranching(Clause& c) -{ - assert(decisionLevel() == 0); - - //fprintf(stderr, "assymmetric branching on clause: "); printClause(c); fprintf(stderr, "\n"); - if (satisfied(c)){ - //fprintf(stderr, "subsumed.\n"); - return true; } - - int old; - vec copy; for (int i = 0; i < c.size(); i++) copy.push(c[i]); - - do { - assert(copy.size() == c.size()); - - old = copy.size(); - - //fprintf(stderr, "checking that clause is normalized\n"); - //for (int i = 0; i < copy.size(); i++) - // assert(value(copy[i]) == l_Undef); - - for (int i = 0; i < copy.size(); i++){ - trail_lim.push(trail.size()); - //fprintf(stderr, " -- trying to delete literal "); printLit(copy[i]); - for (int j = 0; j < copy.size(); j++) - if (j != i) - check(enqueue(~copy[j])); - - if (propagate() != NULL){ - //fprintf(stderr, " succeeded\n"); - cancelUntil(0); - Lit l = copy[i]; - assert(find(copy, l)); - remove(copy, l); - if (!strengthen(c, l)) - return false; - i--; - - if (c.size() == 1) - return propagate() == NULL; - else - assert(qhead == trail.size()); - } - else - //fprintf(stderr, " failed\n"); - - cancelUntil(0); - } - - //} while (false); - } while (copy.size() < old); - - return true; -} - -// Returns FALSE if clause is always satisfied ('out_clause' should not be used). -//bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& out_clause) -bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& out_clause) -{ - stats.merges++; - - bool ps_smallest = _ps.size() < _qs.size(); - const Clause& ps = ps_smallest ? _qs : _ps; - const Clause& qs = ps_smallest ? _ps : _qs; - - for (int i = 0; i < qs.size(); i++){ - if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) { - if (ps[j] == ~qs[i]) - return false; - else - goto next; - } - out_clause.push(qs[i]); - } - next:; - } - - for (int i = 0; i < ps.size(); i++) - if (var(ps[i]) != v) - out_clause.push(ps[i]); - - return true; -} - - -void Solver::gather(vec& clauses) -{ - //fprintf(stderr, "Gathering clauses for backwards subsumption\n"); - int ntouched = 0; - assert(touched.size() == occurs.size()); - clauses.clear(); - for (int i = 0; i < touched.size(); i++) - if (touched[i]){ - const vec& cs = getOccurs(i); - ntouched++; - for (int j = 0; j < cs.size(); j++) - if (cs[j]->mark() == 0){ - clauses.push(cs[j]); - cs[j]->mark(2); - } - touched[i] = 0; - } - - //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size()); - for (int i = 0; i < clauses.size(); i++) - clauses[i]->mark(0); -} - - -/*_________________________________________________________________________________________________ -| -| subsumes : (_c : ClauseId) (c : Clause&) (_d : ClauseId) (d : Clause&) -> bool -| -| Description: -| Checks if c subsumes d, and at the same time, if c can be used to simplify d by subsumption -| resolution. -| -| Input: -| Indices into the 'clauses' vector _c, _d, and references to the corresponding clauses c, d. -| -| Result: -| lit_Error - No subsumption or simplification -| lit_Undef - Clause c subsumes d -| l - The literal l can be deleted from d -|________________________________________________________________________________________________@*/ -inline Lit Solver::subsumes(const Clause& c, const Clause& d) -{ - stats.subsumption_checks++; - if (d.size() < c.size() || (c.abstraction() & ~d.abstraction()) != 0) - return lit_Error; - - Lit ret = lit_Undef; - - for (int i = 0; i < c.size(); i++) { - // search for c[i] or ~c[i] - for (int j = 0; j < d.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 - stats.subsumption_misses++; - return lit_Error; - ok:; - } - - return ret; -} - - -// Backward subsumption + backward subsumption resolution -bool Solver::backwardSubsumptionCheck() -{ - while (subsumption_queue.size() > 0 || qhead < trail.size()){ - - // if propagation queue is non empty, take the first literal and - // create a dummy unit clause - if (qhead < trail.size()){ - Lit l = trail[qhead++]; - (*bwdsub_tmpunit)[0] = l; - assert(bwdsub_tmpunit->mark() == 0); - subsumption_queue.push(bwdsub_tmpunit); - } - Clause& c = *subsumption_queue.last(); subsumption_queue.pop(); - - if (c.mark()) - continue; - - if (c.size() == 1 && !enqueue(c[0])) - return false; - - // (1) find best variable to scan - Var best = var(c[0]); - for (int i = 1; i < c.size(); i++) - if (occurs[var(c[i])].size() < occurs[best].size()) - best = var(c[i]); - - // (2) search all candidates - const vec& cs = getOccurs(best); - - for (int j = 0; j < cs.size(); j++) - if (cs[j] != &c){ - if (cs[j]->mark()) - continue; - if (c.mark()) - break; - - //fprintf(stderr, "backward candidate "); printClause(*cs[j]); fprintf(stderr, "\n"); - Lit l = subsumes(c, *cs[j]); - if (l == lit_Undef){ - //fprintf(stderr, "clause backwards subsumed\n"); - //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n"); - //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n"); - removeClause(*cs[j], false); - }else if (l != lit_Error){ - //fprintf(stderr, "backwards subsumption resolution\n"); - //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n"); - //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n"); - - assert(cs[j]->size() > 1); - assert(find(*cs[j], ~l)); - - subsumption_queue.push(cs[j]); - if (!strengthen(*cs[j], ~l)) - return false; - - // did current candidate get deleted from cs? then check candidate at index j again - if (var(l) == best) - j--; - } - } - } - - return true; -} - - -bool Solver::eliminateVar(Var v, bool fail) -{ - assert(hasVarProp(v, p_frozen)); - - vec pos, neg; - const vec& cls = getOccurs(v); - - if (value(v) != l_Undef || cls.size() == 0) - return true; - - //fprintf(stderr, "trying to eliminate var %d\n", v+1); - for (int i = 0; i < cls.size(); i++){ - //fprintf(stderr, "clause: "); printClause(*cls[i]); fprintf(stderr, "\n"); - if (find(*cls[i], Lit(v))) - pos.push(cls[i]); - else{ - assert(find(*cls[i], ~Lit(v))); - neg.push(cls[i]); - } - } - -#ifdef WEAKEN - vec posc(pos.size(), 0); - vec negc(neg.size(), 0); -#endif - // check if number of clauses decreases - int cnt = 0; - vec resolvent; - for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++){ - resolvent.clear(); - if (merge(*pos[i], *neg[j], v, resolvent)){ - cnt++; -#ifdef WEAKEN - posc[i]++; - negc[j]++; -#endif - } -#ifndef WEAKEN - if (cnt > cls.size() + grow) - return true; -#else -#ifdef MATING - if (cnt > cls.size() + grow) - if (posc[i] > 0) - break; -#endif -#endif - assert(pos.size() <= n_occ[toInt(Lit(v))]); - assert(neg.size() <= n_occ[toInt(~Lit(v))]); - } - -#ifdef WEAKEN -#ifdef MATING - for (int i = 0; i < neg.size(); i++) - if (negc[i] == 0) - for (int j = 0; j < pos.size(); j++){ - resolvent.clear(); - if (merge(*neg[i], *pos[j], v, resolvent)){ - negc[i]++; - break; - } - } -#endif - for (int i = 0; i < pos.size(); i++) - if (posc[i] == 0) - removeClause(*pos[i], false); - - for (int i = 0; i < neg.size(); i++) - if (negc[i] == 0) - removeClause(*neg[i], false); - - if (cnt > cls.size() + grow) - return true; -#endif - //if (pos.size() != n_occ[toInt(Lit(v))]) - // fprintf(stderr, "pos.size() = %d, n_occ[toInt(Lit(v))] = %d\n", pos.size(), n_occ[toInt(Lit(v))]); - assert(pos.size() == n_occ[toInt(Lit(v))]); - //if (neg.size() != n_occ[toInt(~Lit(v))]) - // fprintf(stderr, "neg.size() = %d, n_occ[toInt(Lit(v))] = %d\n", neg.size(), n_occ[toInt(Lit(v))]); - assert(neg.size() == n_occ[toInt(~Lit(v))]); - assert(cnt <= cls.size() + grow); - setVarProp(v, p_decisionvar, false); - - // produce clauses in cross product - int top = clauses.size(); - for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++){ - resolvent.clear(); -#ifdef WEAKEN - if (pos[i]->mark() == 1) - break; - if (neg[j]->mark() == 1) - continue; -#endif - - if (merge(*pos[i], *neg[j], v, resolvent)){ - int i, j; - for (i = j = 0; i < resolvent.size(); i++) - if (value(resolvent[i]) == l_True) - goto next; - else if (value(resolvent[i]) == l_Undef) - resolvent[j++] = resolvent[i]; - resolvent.shrink(i - j); - - if (resolvent.size() == 1){ - if (!enqueue(resolvent[0])) - return false; - }else{ - int apa = clauses.size(); - check(newClause(resolvent, false, true)); - assert(apa + 1 == clauses.size()); - } - } - next:; - } - - if (fail){ - fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); - fprintf(stderr, "previous clauses:\n"); - for (int i = 0; i < cls.size(); i++){ - printClause(*cls[i]); - fprintf(stderr, "\n"); - } - - fprintf(stderr, "new clauses:\n"); - for (int i = top; i < clauses.size(); i++){ - printClause(*clauses[i]); - fprintf(stderr, "\n"); - } - - assert(0); } - - //fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); - //fprintf(stderr, "previous clauses:\n"); - //for (int i = 0; i < cls.size(); i++){ - // printClause(*cls[i]); - // fprintf(stderr, "\n"); - //} - // - //fprintf(stderr, "new clauses:\n"); - //for (int i = top; i < clauses.size(); i++){ - // printClause(*clauses[i]); - // fprintf(stderr, "\n"); - //} - - // delete + store old clauses - eliminated_var.push(v); - eliminated_lim.push(eliminated.size()); - for (int i = 0; i < cls.size(); i++){ - eliminated.push(Clause_new(*cls[i])); - -#ifdef WEAKEN - if (cls[i]->mark() == 0) -#endif - removeClause(*cls[i], false); - - } - - assert(subsumption_queue.size() == 0); - for (int i = top; i < clauses.size(); i++) -#ifdef ASSYMM - if (clauses[i]->mark() == 0) - if (!assymmetricBranching(*clauses[i])) - return false; - else - subsumption_queue.push(clauses[i]); -#else - if (clauses[i]->mark() == 0) - subsumption_queue.push(clauses[i]); -#endif - - return backwardSubsumptionCheck(); -} - - -void Solver::extendModel() -{ - assert(eliminated_var.size() == eliminated_lim.size()); - for (int i = eliminated_var.size()-1; i >= 0; i--){ - Var v = eliminated_var[i]; - Lit l = lit_Undef; - - //fprintf(stderr, "extending var %d\n", v+1); - - for (int j = eliminated_lim[i]; j < (i+1 >= eliminated_lim.size() ? eliminated.size() : eliminated_lim[i+1]); j++){ - assert(j < eliminated.size()); - Clause& c = *eliminated[j]; - - //fprintf(stderr, "checking clause: "); printClause(c); fprintf(stderr, "\n"); - - for (int k = 0; k < c.size(); k++) - if (var(c[k]) == v) - l = c[k]; - else if (value(c[k]) != l_False) - goto next; - - assert(l != lit_Undef); - //fprintf(stderr, "Fixing var %d to %d\n", v+1, !sign(l)); - - assigns[v] = toInt(lbool(!sign(l))); - break; - - next:; - } - - if (value(v) == l_Undef) - assigns[v] = toInt(l_True); - } -} - - -bool Solver::eliminate() -{ - assert(subsumption); - - int cnt = 0; - //fprintf(stderr, "eliminating variables\n"); - -#ifdef INVARIANTS - // check that all clauses are simplified - fprintf(stderr, "Checking that all clauses are normalized prior to variable elimination\n"); - for (int i = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 0){ - Clause& c = *clauses[i]; - for (int j = 0; j < c.size(); j++) - assert(value(c[j]) == l_Undef); - } - fprintf(stderr, "done.\n"); -#endif - - for (;;){ - gather(subsumption_queue); - - if (subsumption_queue.size() == 0 && heap.size() == 0) - break; - - //fprintf(stderr, "backwards subsumption: %10d\n", subsumption_queue.size()); - if (!backwardSubsumptionCheck()) - return false; - - //fprintf(stderr, "variable elimination: %10d\n", heap.size()); - cnt = 0; - for (;;){ - assert(!heap.empty() || heap.size() == 0); - if (heap.empty()) - break; - - Var elim = heap.getmin(); - - assert(hasVarProp(elim, p_frozen)); - - //for (int i = 1; i < heap.heap.size(); i++) - // assert(heap.comp(elim, heap.heap[i]) || !heap.comp(elim, heap.heap[i])); - - //if (cnt++ % 100 == 0) - // fprintf(stderr, "left %10d\r", heap.size()); - - if (!eliminateVar(elim)) - return false; - } - } -#ifdef INVARIANTS - // check that no more subsumption is possible - fprintf(stderr, "Checking that no more subsumption is possible\n"); - cnt = 0; - for (int i = 0; i < clauses.size(); i++){ - if (cnt++ % 1000 == 0) - fprintf(stderr, "left %10d\r", clauses.size() - i); - for (int j = 0; j < i; j++) - assert(clauses[i]->mark() || - clauses[j]->mark() || - subsumes(*clauses[i], *clauses[j]) == lit_Error); - } - fprintf(stderr, "done.\n"); - - // check that no more elimination is possible - fprintf(stderr, "Checking that no more elimination is possible\n"); - for (int i = 0; i < nVars(); i++){ - if (hasVarProp(i, p_frozen)) - eliminateVar(i, true); - } - fprintf(stderr, "done.\n"); - -#endif - - assert(qhead == trail.size()); - - return true; -} -}; diff --git a/stp/sat/Simplifier.cpp b/stp/sat/Simplifier.cpp new file mode 100644 index 00000000..1c192e20 --- /dev/null +++ b/stp/sat/Simplifier.cpp @@ -0,0 +1,542 @@ +/************************************************************************************[Simplifier.C] +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 "Solver.h" + +namespace MINISAT { + +static const int grow = 0; + +//#define WEAKEN +//#define MATING +//#define ASSYMM + +bool Solver::assymmetricBranching(Clause& c) +{ + assert(decisionLevel() == 0); + + //fprintf(stderr, "assymmetric branching on clause: "); printClause(c); fprintf(stderr, "\n"); + if (satisfied(c)){ + //fprintf(stderr, "subsumed.\n"); + return true; } + + int old; + vec copy; for (int i = 0; i < c.size(); i++) copy.push(c[i]); + + do { + assert(copy.size() == c.size()); + + old = copy.size(); + + //fprintf(stderr, "checking that clause is normalized\n"); + //for (int i = 0; i < copy.size(); i++) + // assert(value(copy[i]) == l_Undef); + + for (int i = 0; i < copy.size(); i++){ + trail_lim.push(trail.size()); + //fprintf(stderr, " -- trying to delete literal "); printLit(copy[i]); + for (int j = 0; j < copy.size(); j++) + if (j != i) + check(enqueue(~copy[j])); + + if (propagate() != NULL){ + //fprintf(stderr, " succeeded\n"); + cancelUntil(0); + Lit l = copy[i]; + assert(find(copy, l)); + remove(copy, l); + if (!strengthen(c, l)) + return false; + i--; + + if (c.size() == 1) + return propagate() == NULL; + else + assert(qhead == trail.size()); + } + else + //fprintf(stderr, " failed\n"); + + cancelUntil(0); + } + + //} while (false); + } while (copy.size() < old); + + return true; +} + +// Returns FALSE if clause is always satisfied ('out_clause' should not be used). +//bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& out_clause) +bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& out_clause) +{ + stats.merges++; + + bool ps_smallest = _ps.size() < _qs.size(); + const Clause& ps = ps_smallest ? _qs : _ps; + const Clause& qs = ps_smallest ? _ps : _qs; + + for (int i = 0; i < qs.size(); i++){ + if (var(qs[i]) != v){ + for (int j = 0; j < ps.size(); j++) + if (var(ps[j]) == var(qs[i])) { + if (ps[j] == ~qs[i]) + return false; + else + goto next; + } + out_clause.push(qs[i]); + } + next:; + } + + for (int i = 0; i < ps.size(); i++) + if (var(ps[i]) != v) + out_clause.push(ps[i]); + + return true; +} + + +void Solver::gather(vec& clauses) +{ + //fprintf(stderr, "Gathering clauses for backwards subsumption\n"); + int ntouched = 0; + assert(touched.size() == occurs.size()); + clauses.clear(); + for (int i = 0; i < touched.size(); i++) + if (touched[i]){ + const vec& cs = getOccurs(i); + ntouched++; + for (int j = 0; j < cs.size(); j++) + if (cs[j]->mark() == 0){ + clauses.push(cs[j]); + cs[j]->mark(2); + } + touched[i] = 0; + } + + //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size()); + for (int i = 0; i < clauses.size(); i++) + clauses[i]->mark(0); +} + + +/*_________________________________________________________________________________________________ +| +| subsumes : (_c : ClauseId) (c : Clause&) (_d : ClauseId) (d : Clause&) -> bool +| +| Description: +| Checks if c subsumes d, and at the same time, if c can be used to simplify d by subsumption +| resolution. +| +| Input: +| Indices into the 'clauses' vector _c, _d, and references to the corresponding clauses c, d. +| +| Result: +| lit_Error - No subsumption or simplification +| lit_Undef - Clause c subsumes d +| l - The literal l can be deleted from d +|________________________________________________________________________________________________@*/ +inline Lit Solver::subsumes(const Clause& c, const Clause& d) +{ + stats.subsumption_checks++; + if (d.size() < c.size() || (c.abstraction() & ~d.abstraction()) != 0) + return lit_Error; + + Lit ret = lit_Undef; + + for (int i = 0; i < c.size(); i++) { + // search for c[i] or ~c[i] + for (int j = 0; j < d.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 + stats.subsumption_misses++; + return lit_Error; + ok:; + } + + return ret; +} + + +// Backward subsumption + backward subsumption resolution +bool Solver::backwardSubsumptionCheck() +{ + while (subsumption_queue.size() > 0 || qhead < trail.size()){ + + // if propagation queue is non empty, take the first literal and + // create a dummy unit clause + if (qhead < trail.size()){ + Lit l = trail[qhead++]; + (*bwdsub_tmpunit)[0] = l; + assert(bwdsub_tmpunit->mark() == 0); + subsumption_queue.push(bwdsub_tmpunit); + } + Clause& c = *subsumption_queue.last(); subsumption_queue.pop(); + + if (c.mark()) + continue; + + if (c.size() == 1 && !enqueue(c[0])) + return false; + + // (1) find best variable to scan + Var best = var(c[0]); + for (int i = 1; i < c.size(); i++) + if (occurs[var(c[i])].size() < occurs[best].size()) + best = var(c[i]); + + // (2) search all candidates + const vec& cs = getOccurs(best); + + for (int j = 0; j < cs.size(); j++) + if (cs[j] != &c){ + if (cs[j]->mark()) + continue; + if (c.mark()) + break; + + //fprintf(stderr, "backward candidate "); printClause(*cs[j]); fprintf(stderr, "\n"); + Lit l = subsumes(c, *cs[j]); + if (l == lit_Undef){ + //fprintf(stderr, "clause backwards subsumed\n"); + //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n"); + //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n"); + removeClause(*cs[j], false); + }else if (l != lit_Error){ + //fprintf(stderr, "backwards subsumption resolution\n"); + //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n"); + //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n"); + + assert(cs[j]->size() > 1); + assert(find(*cs[j], ~l)); + + subsumption_queue.push(cs[j]); + if (!strengthen(*cs[j], ~l)) + return false; + + // did current candidate get deleted from cs? then check candidate at index j again + if (var(l) == best) + j--; + } + } + } + + return true; +} + + +bool Solver::eliminateVar(Var v, bool fail) +{ + assert(hasVarProp(v, p_frozen)); + + vec pos, neg; + const vec& cls = getOccurs(v); + + if (value(v) != l_Undef || cls.size() == 0) + return true; + + //fprintf(stderr, "trying to eliminate var %d\n", v+1); + for (int i = 0; i < cls.size(); i++){ + //fprintf(stderr, "clause: "); printClause(*cls[i]); fprintf(stderr, "\n"); + if (find(*cls[i], Lit(v))) + pos.push(cls[i]); + else{ + assert(find(*cls[i], ~Lit(v))); + neg.push(cls[i]); + } + } + +#ifdef WEAKEN + vec posc(pos.size(), 0); + vec negc(neg.size(), 0); +#endif + // check if number of clauses decreases + int cnt = 0; + vec resolvent; + for (int i = 0; i < pos.size(); i++) + for (int j = 0; j < neg.size(); j++){ + resolvent.clear(); + if (merge(*pos[i], *neg[j], v, resolvent)){ + cnt++; +#ifdef WEAKEN + posc[i]++; + negc[j]++; +#endif + } +#ifndef WEAKEN + if (cnt > cls.size() + grow) + return true; +#else +#ifdef MATING + if (cnt > cls.size() + grow) + if (posc[i] > 0) + break; +#endif +#endif + assert(pos.size() <= n_occ[toInt(Lit(v))]); + assert(neg.size() <= n_occ[toInt(~Lit(v))]); + } + +#ifdef WEAKEN +#ifdef MATING + for (int i = 0; i < neg.size(); i++) + if (negc[i] == 0) + for (int j = 0; j < pos.size(); j++){ + resolvent.clear(); + if (merge(*neg[i], *pos[j], v, resolvent)){ + negc[i]++; + break; + } + } +#endif + for (int i = 0; i < pos.size(); i++) + if (posc[i] == 0) + removeClause(*pos[i], false); + + for (int i = 0; i < neg.size(); i++) + if (negc[i] == 0) + removeClause(*neg[i], false); + + if (cnt > cls.size() + grow) + return true; +#endif + //if (pos.size() != n_occ[toInt(Lit(v))]) + // fprintf(stderr, "pos.size() = %d, n_occ[toInt(Lit(v))] = %d\n", pos.size(), n_occ[toInt(Lit(v))]); + assert(pos.size() == n_occ[toInt(Lit(v))]); + //if (neg.size() != n_occ[toInt(~Lit(v))]) + // fprintf(stderr, "neg.size() = %d, n_occ[toInt(Lit(v))] = %d\n", neg.size(), n_occ[toInt(Lit(v))]); + assert(neg.size() == n_occ[toInt(~Lit(v))]); + assert(cnt <= cls.size() + grow); + setVarProp(v, p_decisionvar, false); + + // produce clauses in cross product + int top = clauses.size(); + for (int i = 0; i < pos.size(); i++) + for (int j = 0; j < neg.size(); j++){ + resolvent.clear(); +#ifdef WEAKEN + if (pos[i]->mark() == 1) + break; + if (neg[j]->mark() == 1) + continue; +#endif + + if (merge(*pos[i], *neg[j], v, resolvent)){ + int i, j; + for (i = j = 0; i < resolvent.size(); i++) + if (value(resolvent[i]) == l_True) + goto next; + else if (value(resolvent[i]) == l_Undef) + resolvent[j++] = resolvent[i]; + resolvent.shrink(i - j); + + if (resolvent.size() == 1){ + if (!enqueue(resolvent[0])) + return false; + }else{ + int apa = clauses.size(); + check(newClause(resolvent, false, true)); + assert(apa + 1 == clauses.size()); + } + } + next:; + } + + if (fail){ + fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); + fprintf(stderr, "previous clauses:\n"); + for (int i = 0; i < cls.size(); i++){ + printClause(*cls[i]); + fprintf(stderr, "\n"); + } + + fprintf(stderr, "new clauses:\n"); + for (int i = top; i < clauses.size(); i++){ + printClause(*clauses[i]); + fprintf(stderr, "\n"); + } + + assert(0); } + + //fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); + //fprintf(stderr, "previous clauses:\n"); + //for (int i = 0; i < cls.size(); i++){ + // printClause(*cls[i]); + // fprintf(stderr, "\n"); + //} + // + //fprintf(stderr, "new clauses:\n"); + //for (int i = top; i < clauses.size(); i++){ + // printClause(*clauses[i]); + // fprintf(stderr, "\n"); + //} + + // delete + store old clauses + eliminated_var.push(v); + eliminated_lim.push(eliminated.size()); + for (int i = 0; i < cls.size(); i++){ + eliminated.push(Clause_new(*cls[i])); + +#ifdef WEAKEN + if (cls[i]->mark() == 0) +#endif + removeClause(*cls[i], false); + + } + + assert(subsumption_queue.size() == 0); + for (int i = top; i < clauses.size(); i++) +#ifdef ASSYMM + if (clauses[i]->mark() == 0) + if (!assymmetricBranching(*clauses[i])) + return false; + else + subsumption_queue.push(clauses[i]); +#else + if (clauses[i]->mark() == 0) + subsumption_queue.push(clauses[i]); +#endif + + return backwardSubsumptionCheck(); +} + + +void Solver::extendModel() +{ + assert(eliminated_var.size() == eliminated_lim.size()); + for (int i = eliminated_var.size()-1; i >= 0; i--){ + Var v = eliminated_var[i]; + Lit l = lit_Undef; + + //fprintf(stderr, "extending var %d\n", v+1); + + for (int j = eliminated_lim[i]; j < (i+1 >= eliminated_lim.size() ? eliminated.size() : eliminated_lim[i+1]); j++){ + assert(j < eliminated.size()); + Clause& c = *eliminated[j]; + + //fprintf(stderr, "checking clause: "); printClause(c); fprintf(stderr, "\n"); + + for (int k = 0; k < c.size(); k++) + if (var(c[k]) == v) + l = c[k]; + else if (value(c[k]) != l_False) + goto next; + + assert(l != lit_Undef); + //fprintf(stderr, "Fixing var %d to %d\n", v+1, !sign(l)); + + assigns[v] = toInt(lbool(!sign(l))); + break; + + next:; + } + + if (value(v) == l_Undef) + assigns[v] = toInt(l_True); + } +} + + +bool Solver::eliminate() +{ + assert(subsumption); + + int cnt = 0; + //fprintf(stderr, "eliminating variables\n"); + +#ifdef INVARIANTS + // check that all clauses are simplified + fprintf(stderr, "Checking that all clauses are normalized prior to variable elimination\n"); + for (int i = 0; i < clauses.size(); i++) + if (clauses[i]->mark() == 0){ + Clause& c = *clauses[i]; + for (int j = 0; j < c.size(); j++) + assert(value(c[j]) == l_Undef); + } + fprintf(stderr, "done.\n"); +#endif + + for (;;){ + gather(subsumption_queue); + + if (subsumption_queue.size() == 0 && heap.size() == 0) + break; + + //fprintf(stderr, "backwards subsumption: %10d\n", subsumption_queue.size()); + if (!backwardSubsumptionCheck()) + return false; + + //fprintf(stderr, "variable elimination: %10d\n", heap.size()); + cnt = 0; + for (;;){ + assert(!heap.empty() || heap.size() == 0); + if (heap.empty()) + break; + + Var elim = heap.getmin(); + + assert(hasVarProp(elim, p_frozen)); + + //for (int i = 1; i < heap.heap.size(); i++) + // assert(heap.comp(elim, heap.heap[i]) || !heap.comp(elim, heap.heap[i])); + + //if (cnt++ % 100 == 0) + // fprintf(stderr, "left %10d\r", heap.size()); + + if (!eliminateVar(elim)) + return false; + } + } +#ifdef INVARIANTS + // check that no more subsumption is possible + fprintf(stderr, "Checking that no more subsumption is possible\n"); + cnt = 0; + for (int i = 0; i < clauses.size(); i++){ + if (cnt++ % 1000 == 0) + fprintf(stderr, "left %10d\r", clauses.size() - i); + for (int j = 0; j < i; j++) + assert(clauses[i]->mark() || + clauses[j]->mark() || + subsumes(*clauses[i], *clauses[j]) == lit_Error); + } + fprintf(stderr, "done.\n"); + + // check that no more elimination is possible + fprintf(stderr, "Checking that no more elimination is possible\n"); + for (int i = 0; i < nVars(); i++){ + if (hasVarProp(i, p_frozen)) + eliminateVar(i, true); + } + fprintf(stderr, "done.\n"); + +#endif + + assert(qhead == trail.size()); + + return true; +} +}; diff --git a/stp/sat/Solver.C b/stp/sat/Solver.C deleted file mode 100644 index 0fcb6149..00000000 --- a/stp/sat/Solver.C +++ /dev/null @@ -1,811 +0,0 @@ -/****************************************************************************************[Solver.C] -MiniSat -- Copyright (c) 2003-2005, 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 "Solver.h" -#include "Sort.h" -#include - -namespace MINISAT { -//================================================================================================= -// Operations on clauses: - - -/*_________________________________________________________________________________________________ -| -| newClause : (ps : const vec&) (learnt : bool) -> [void] -| -| Description: -| Allocate and add a new clause to the SAT solvers clause database. -| -| Input: -| ps - The new clause as a vector of literals. -| learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the -| asserting literal. An appropriate 'enqueue()' operation will be performed on this -| literal. One of the watches will always be on this literal, the other will be set to -| the literal with the highest decision level. -| -| Effect: -| Activity heuristics are updated. -|________________________________________________________________________________________________@*/ -bool Solver::newClause(const vec& ps_, bool learnt, bool normalized) -{ - vec qs; - if (!learnt && !normalized){ - assert(decisionLevel() == 0); - ps_.copyTo(qs); // Make a copy of the input vector. - - // Remove duplicates: - sortUnique(qs); - - // Check if clause is satisfied: - for (int i = 0; i < qs.size()-1; i++){ - if (qs[i] == ~qs[i+1]) - return true; } - for (int i = 0; i < qs.size(); i++){ - if (value(qs[i]) == l_True) - return true; } - - // Remove false literals: - int i, j; - for (i = j = 0; i < qs.size(); i++) - if (value(qs[i]) != l_False) - qs[j++] = qs[i]; - qs.shrink(i - j); - } - const vec& ps = learnt || normalized ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals. - - if (ps.size() == 0) - return false; - else if (ps.size() == 1){ - assert(decisionLevel() == 0); - return enqueue(ps[0]); - }else{ - // Allocate clause: - Clause* c = Clause_new(ps, learnt); - - if (learnt){ - // Put the second watch on the first literal with highest decision level: - // (requires that this method is called at the level where the clause is asserting!) - int i; - for (i = 1; i < ps.size() && position(trailpos[var(ps[i])]) < trail_lim.last(); i++) - ; - (*c)[1] = ps[i]; - (*c)[i] = ps[1]; - - // Bump, enqueue, store clause: - claBumpActivity(*c); // (newly learnt clauses should be considered active) - check(enqueue((*c)[0], c)); - learnts.push(c); - stats.learnts_literals += c->size(); - }else{ - // Store clause: - clauses.push(c); - stats.clauses_literals += c->size(); - - if (subsumption){ - c->calcAbstraction(); - for (int i = 0; i < c->size(); i++){ - assert(!find(occurs[var((*c)[i])], c)); - occurs[var((*c)[i])].push(c); - n_occ[toInt((*c)[i])]++; - touched[var((*c)[i])] = 1; - - if (heap.inHeap(var((*c)[i]))) - updateHeap(var((*c)[i])); - } - } - - } - // Watch clause: - watches[toInt(~(*c)[0])].push(c); - watches[toInt(~(*c)[1])].push(c); - } - - return true; -} - - -// Disposes a clauses and removes it from watcher lists. NOTE! -// Low-level; does NOT change the 'clauses' and 'learnts' vector. -// -void Solver::removeClause(Clause& c, bool dealloc) -{ - //fprintf(stderr, "delete %d: ", _c); printClause(c); fprintf(stderr, "\n"); - assert(c.mark() == 0); - - if (c.size() > 1){ - assert(find(watches[toInt(~c[0])], &c)); - assert(find(watches[toInt(~c[1])], &c)); - remove(watches[toInt(~c[0])], &c); - remove(watches[toInt(~c[1])], &c); } - - if (c.learnt()) stats.learnts_literals -= c.size(); - else stats.clauses_literals -= c.size(); - - if (subsumption && !c.learnt()){ - for (int i = 0; i < c.size(); i++){ - if (dealloc){ - assert(find(occurs[var(c[i])], &c)); - remove(occurs[var(c[i])], &c); - } - n_occ[toInt(c[i])]--; - updateHeap(var(c[i])); - } - } - - if (dealloc) - xfree(&c); - else - c.mark(1); -} - - -bool Solver::satisfied(Clause& c) const -{ - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True) - return true; - return false; } - - -bool Solver::strengthen(Clause& c, Lit l) -{ - assert(decisionLevel() == 0); - assert(c.size() > 1); - assert(c.mark() == 0); - - assert(toInt(~c[0]) < watches.size()); - assert(toInt(~c[1]) < watches.size()); - - assert(find(watches[toInt(~c[0])], &c)); - assert(find(watches[toInt(~c[1])], &c)); - assert(find(c,l)); - - if (c.learnt()) stats.learnts_literals -= 1; - else stats.clauses_literals -= 1; - - if (c[0] == l || c[1] == l){ - assert(find(watches[toInt(~l)], &c)); - remove(c,l); - remove(watches[toInt(~l)], &c); - if (c.size() > 1){ - assert(!find(watches[toInt(~c[1])], &c)); - watches[toInt(~c[1])].push(&c); } - else { - assert(find(watches[toInt(~c[0])], &c)); - remove(watches[toInt(~c[0])], &c); - removeClause(c, false); - } - } - else - remove(c,l); - - assert(c.size() == 1 || find(watches[toInt(~c[0])], &c)); - assert(c.size() == 1 || find(watches[toInt(~c[1])], &c)); - - if (subsumption){ - assert(find(occurs[var(l)], &c)); - remove(occurs[var(l)], &c); - assert(!find(occurs[var(l)], &c)); - - c.calcAbstraction(); - - n_occ[toInt(l)]--; - updateHeap(var(l)); - } - - return c.size() == 1 ? enqueue(c[0]) : true; -} - - -//================================================================================================= -// Minor methods: - - -// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be -// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). -// -Var Solver::newVar(bool polarity, bool dvar) { - int index; - index = nVars(); - watches .push(); // (list for positive literal) - watches .push(); // (list for negative literal) - reason .push(NULL); - assigns .push(toInt(l_Undef)); - trailpos .push(TrailPos(0,0)); - activity .push(0); - order .newVar(polarity,dvar); - seen .push(0); - touched .push(0); - if (subsumption){ - occurs .push(); - n_occ .push(0); - n_occ .push(0); - heap .setBounds(index+1); - } - return index; } - - -// Returns FALSE if immediate conflict. -bool Solver::assume(Lit p) { - trail_lim.push(trail.size()); - return enqueue(p); } - - -// Revert to the state at given level. -void Solver::cancelUntil(int level) { - if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ - Var x = var(trail[c]); - assigns[x] = toInt(l_Undef); - reason [x] = NULL; - order.undo(x); } - qhead = trail_lim[level]; - trail.shrink(trail.size() - trail_lim[level]); - trail_lim.shrink(trail_lim.size() - level); - } -} - - -//================================================================================================= -// Major methods: - - -/*_________________________________________________________________________________________________ -| -| analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] -| -| Description: -| Analyze conflict and produce a reason clause. -| -| Pre-conditions: -| * 'out_learnt' is assumed to be cleared. -| * Current decision level must be greater than root level. -| -| Post-conditions: -| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. -| -| Effect: -| Will undo part of the trail, upto but not beyond the assumption of the current decision level. -|________________________________________________________________________________________________@*/ -void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) -{ - int pathC = 0; - int btpos = -1; - Lit p = lit_Undef; - - // Generate conflict clause: - // - out_learnt.push(); // (leave room for the asserting literal) - int index = trail.size()-1; - do{ - assert(confl != NULL); // (otherwise should be UIP) - Clause& c = *confl; - - if (c.learnt()) - claBumpActivity(c); - - for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ - Lit q = c[j]; - if (!seen[var(q)] && position(trailpos[var(q)]) >= trail_lim[0]){ - varBumpActivity(q); - seen[var(q)] = 1; - if (position(trailpos[var(q)]) >= trail_lim.last()) - pathC++; - else{ - out_learnt.push(q); - btpos = max(btpos, position(trailpos[var(q)])); - } - } - } - - // Select next clause to look at: - while (!seen[var(trail[index--])]); - p = trail[index+1]; - confl = reason[var(p)]; - seen[var(p)] = 0; - pathC--; - - }while (pathC > 0); - out_learnt[0] = ~p; - - // Find correct backtrack level - for (out_btlevel = trail_lim.size()-1; out_btlevel > 0 && trail_lim[out_btlevel-1] > btpos; out_btlevel--) - ; - - int i, j; - if (expensive_ccmin){ - // Simplify conflict clause (a lot): - // - uint min_level = 0; - for (i = 1; i < out_learnt.size(); i++) - min_level |= abstractLevel(trailpos[var(out_learnt[i])]); // (maintain an abstraction of levels involved in conflict) - - out_learnt.copyTo(analyze_toclear); - for (i = j = 1; i < out_learnt.size(); i++) - if (reason[var(out_learnt[i])] == NULL || !analyze_removable(out_learnt[i], min_level)) - out_learnt[j++] = out_learnt[i]; - }else{ - // Simplify conflict clause (a little): - // - out_learnt.copyTo(analyze_toclear); - for (i = j = 1; i < out_learnt.size(); i++){ - Clause& c = *reason[var(out_learnt[i])]; - for (int k = 1; k < c.size(); k++) - if (!seen[var(c[k])] && position(trailpos[var(c[k])]) >= trail_lim[0]){ - out_learnt[j++] = out_learnt[i]; - break; } - } - } - - stats.max_literals += out_learnt.size(); - out_learnt.shrink(i - j); - stats.tot_literals += out_learnt.size(); - - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) -} - - -// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed. -// -bool Solver::analyze_removable(Lit p, uint min_level) -{ - analyze_stack.clear(); analyze_stack.push(p); - int top = analyze_toclear.size(); - while (analyze_stack.size() > 0){ - assert(reason[var(analyze_stack.last())] != NULL); - Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); - - for (int i = 1; i < c.size(); i++){ - Lit p = c[i]; - TrailPos tp = trailpos[var(p)]; - if (!seen[var(p)] && position(tp) >= trail_lim[0]){ - if (reason[var(p)] != NULL && (abstractLevel(tp) & min_level) != 0){ - seen[var(p)] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - }else{ - for (int j = top; j < analyze_toclear.size(); j++) - seen[var(analyze_toclear[j])] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; - } - } - } - } - - return true; -} - - -/*_________________________________________________________________________________________________ -| -| analyzeFinal : (p : Lit) -> [void] -| -| Description: -| Specialized analysis procedure to express the final conflict in terms of assumptions. -| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and -| stores the result in 'out_conflict'. -|________________________________________________________________________________________________@*/ -void Solver::analyzeFinal(Lit p, vec& out_conflict) -{ - out_conflict.clear(); - out_conflict.push(p); - - if (decisionLevel() == 0) - return; - - seen[var(p)] = 1; - - int start = position(trailpos[var(p)]); - for (int i = start; i >= trail_lim[0]; i--){ - Var x = var(trail[i]); - if (seen[x]){ - if (reason[x] == NULL){ - assert(position(trailpos[x]) >= trail_lim[0]); - out_conflict.push(~trail[i]); - }else{ - Clause& c = *reason[x]; - for (int j = 1; j < c.size(); j++) - if (position(trailpos[var(c[j])]) >= trail_lim[0]) - seen[var(c[j])] = 1; - } - seen[x] = 0; - } - } -} - - -/*_________________________________________________________________________________________________ -| -| enqueue : (p : Lit) (from : Clause*) -> [bool] -| -| Description: -| Puts a new fact on the propagation queue as well as immediately updating the variable's value. -| Should a conflict arise, FALSE is returned. -| -| Input: -| p - The fact to enqueue -| from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'. -| Default value is NULL (no reason). -| -| Output: -| TRUE if fact was enqueued without conflict, FALSE otherwise. -|________________________________________________________________________________________________@*/ -bool Solver::enqueue(Lit p, Clause* from) -{ - - if (value(p) != l_Undef) - return value(p) != l_False; - else{ - assigns [var(p)] = toInt(lbool(!sign(p))); - trailpos[var(p)] = TrailPos(trail.size(),decisionLevel()); - reason [var(p)] = from; - trail.push(p); - return true; - } -} - - -/*_________________________________________________________________________________________________ -| -| propagate : [void] -> [Clause*] -| -| Description: -| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, -| otherwise NULL. -| -| Post-conditions: -| * the propagation queue is empty, even if there was a conflict. -|________________________________________________________________________________________________@*/ -Clause* Solver::propagate() -{ - if (decisionLevel() == 0 && subsumption) - return backwardSubsumptionCheck() ? NULL : propagate_tmpempty; - - Clause* confl = NULL; - //fprintf(stderr, "propagate, qhead = %d, qtail = %d\n", qhead, qtail); - while (qhead < trail.size()){ - stats.propagations++; - simpDB_props--; - - Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. - vec& ws = watches[toInt(p)]; - Clause **i, **j, **end; - - for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){ - Clause& c = **i++; - - // Make sure the false literal is data[1]: - Lit false_lit = ~p; - if (c[0] == false_lit) - c[0] = c[1], c[1] = false_lit; - - assert(c[1] == false_lit); - - // If 0th watch is true, then clause is already satisfied. - Lit first = c[0]; - if (value(first) == l_True){ - *j++ = &c; - }else{ - // Look for new watch: - for (int k = 2; k < c.size(); k++) - if (value(c[k]) != l_False){ - c[1] = c[k]; c[k] = false_lit; - watches[toInt(~c[1])].push(&c); - goto FoundWatch; } - - // Did not find watch -- clause is unit under assignment: - *j++ = &c; - if (!enqueue(first, &c)){ - confl = &c; - qhead = trail.size(); - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - FoundWatch:; - } - } - ws.shrink(i - j); - } - - return confl; -} - - -/*_________________________________________________________________________________________________ -| -| reduceDB : () -> [void] -| -| Description: -| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked -| 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()); } }; -void Solver::reduceDB() -{ - int i, j; - double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity - - sort(learnts, reduceDB_lt()); - for (i = j = 0; i < learnts.size() / 2; i++){ - if (learnts[i]->size() > 2 && !locked(*learnts[i])) - 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.shrink(i - j); -} - - -/*_________________________________________________________________________________________________ -| -| simplifyDB : [void] -> [bool] -| -| Description: -| Simplify the clause database according to the current top-level assigment. Currently, the only -| thing done here is the removal of satisfied clauses, but more things can be put here. -|________________________________________________________________________________________________@*/ -bool Solver::simplifyDB(bool expensive) -{ - assert(decisionLevel() == 0); - if (!ok || propagate() != NULL) - return ok = false; - - if (nAssigns() == simpDB_assigns || - (!subsumption && simpDB_props > 0)) // (nothing has changed or preformed a simplification too recently) - return true; - - if (subsumption){ - if (expensive && !eliminate()) - return ok = false; - - // Move this cleanup code to its own method ? - int i , j; - vec dirty; - for (i = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 1){ - Clause& c = *clauses[i]; - for (int k = 0; k < c.size(); k++) - if (!seen[var(c[k])]){ - seen[var(c[k])] = 1; - dirty.push(var(c[k])); - } - } - - for (i = 0; i < dirty.size(); i++){ - cleanOcc(dirty[i]); - seen[dirty[i]] = 0; - } - - for (i = j = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 1) - xfree(clauses[i]); - else - clauses[j++] = clauses[i]; - clauses.shrink(i - j); - } - - // Remove satisfied clauses: - for (int type = 0; type < (subsumption ? 1 : 2); type++){ // (only scan learnt clauses if subsumption is on) - vec& cs = type ? learnts : clauses; - int j = 0; - for (int i = 0; i < cs.size(); i++){ - assert(cs[i]->mark() == 0); - if (satisfied(*cs[i])) - removeClause(*cs[i]); - else - cs[j++] = cs[i]; - } - cs.shrink(cs.size()-j); - } - order.cleanup(); - - simpDB_assigns = nAssigns(); - simpDB_props = stats.clauses_literals + stats.learnts_literals; // (shouldn't depend on 'stats' really, but it will do for now) - - return true; -} - - -/*_________________________________________________________________________________________________ -| -| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] -| -| Description: -| Search for a model the specified number of conflicts, keeping the number of learnt clauses -| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to -| indicate infinity. -| -| Output: -| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If -| 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) -{ - assert(ok); - int backtrack_level; - int conflictC = 0; - vec learnt_clause; - - stats.starts++; - var_decay = 1 / params.var_decay; - cla_decay = 1 / params.clause_decay; - - for (;;){ - Clause* confl = propagate(); - if (confl != NULL){ - // CONFLICT - stats.conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; - - learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level); - cancelUntil(backtrack_level); - newClause(learnt_clause, true); - varDecayActivity(); - claDecayActivity(); - - }else{ - // NO CONFLICT - - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ - // Reached bound on number of conflicts: - progress_estimate = progressEstimate(); - cancelUntil(0); - return l_Undef; } - - // Simplify the set of problem clauses: - if (decisionLevel() == 0 && !simplifyDB()) - return l_False; - - if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) - // Reduce the set of learnt clauses: - reduceDB(); - - Lit next = lit_Undef; - - if (decisionLevel() < assumptions.size()){ - // Perform user provided assumption: - next = assumptions[decisionLevel()]; - if (value(next) == l_False){ - analyzeFinal(~next, conflict); - return l_False; } - }else{ - // New variable decision: - stats.decisions++; - next = order.select(params.random_var_freq, decisionLevel()); - } - if (next == lit_Undef) - // Model found: - return l_True; - - check(assume(next)); - } - } -} - - -// Return search-space coverage. Not extremely reliable. -// -double Solver::progressEstimate() -{ - double progress = 0; - double F = 1.0 / nVars(); - - for (int i = 0; i <= decisionLevel(); i++){ - int beg = i == 0 ? 0 : trail_lim[i - 1]; - int end = i == decisionLevel() ? trail.size() : trail_lim[i]; - progress += pow(F, i) * (end - beg); - } - - return progress / nVars(); -} - - -// Divide all variable activities by 1e100. -// -void Solver::varRescaleActivity() -{ - for (int i = 0; i < nVars(); i++) - activity[i] *= 1e-100; - var_inc *= 1e-100; -} - - -// Divide all constraint activities by 1e100. -// -void Solver::claRescaleActivity() -{ - for (int i = 0; i < learnts.size(); i++) - learnts[i]->activity() *= 1e-20; - cla_inc *= 1e-20; -} - - -/*_________________________________________________________________________________________________ -| -| solve : (assumps : const vec&) -> [bool] -| -| Description: -| Top-level solve. -|________________________________________________________________________________________________@*/ -bool Solver::solve(const vec& assumps) -{ - model.clear(); - conflict.clear(); - - if (!simplifyDB(true)) return false; - - - double nof_conflicts = params.restart_first; - double nof_learnts = nClauses() * params.learntsize_factor; - lbool status = l_Undef; - assumps.copyTo(assumptions); - - if (verbosity >= 1){ - reportf("==================================[MINISAT]====================================\n"); - reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); - reportf("===============================================================================\n"); - } - - // Search: - while (status == l_Undef){ - if (verbosity >= 1) - //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); - reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); - status = search((int)nof_conflicts, (int)nof_learnts); - nof_conflicts *= params.restart_inc; - nof_learnts *= params.learntsize_inc; - } - - if (verbosity >= 1) - reportf("==============================================================================\n"); - - if (status == l_True){ - // Copy model: - extendModel(); -#if 1 - //fprintf(stderr, "Verifying model.\n"); - for (int i = 0; i < clauses.size(); i++) - assert(satisfied(*clauses[i])); - for (int i = 0; i < eliminated.size(); i++) - assert(satisfied(*eliminated[i])); -#endif - model.growTo(nVars()); - for (int i = 0; i < nVars(); i++) model[i] = value(i); - }else{ - assert(status == l_False); - if (conflict.size() == 0) - ok = false; - } - - cancelUntil(0); - return status == l_True; -} -};//end of MINISAT namespace diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp new file mode 100644 index 00000000..0fcb6149 --- /dev/null +++ b/stp/sat/Solver.cpp @@ -0,0 +1,811 @@ +/****************************************************************************************[Solver.C] +MiniSat -- Copyright (c) 2003-2005, 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 "Solver.h" +#include "Sort.h" +#include + +namespace MINISAT { +//================================================================================================= +// Operations on clauses: + + +/*_________________________________________________________________________________________________ +| +| newClause : (ps : const vec&) (learnt : bool) -> [void] +| +| Description: +| Allocate and add a new clause to the SAT solvers clause database. +| +| Input: +| ps - The new clause as a vector of literals. +| learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the +| asserting literal. An appropriate 'enqueue()' operation will be performed on this +| literal. One of the watches will always be on this literal, the other will be set to +| the literal with the highest decision level. +| +| Effect: +| Activity heuristics are updated. +|________________________________________________________________________________________________@*/ +bool Solver::newClause(const vec& ps_, bool learnt, bool normalized) +{ + vec qs; + if (!learnt && !normalized){ + assert(decisionLevel() == 0); + ps_.copyTo(qs); // Make a copy of the input vector. + + // Remove duplicates: + sortUnique(qs); + + // Check if clause is satisfied: + for (int i = 0; i < qs.size()-1; i++){ + if (qs[i] == ~qs[i+1]) + return true; } + for (int i = 0; i < qs.size(); i++){ + if (value(qs[i]) == l_True) + return true; } + + // Remove false literals: + int i, j; + for (i = j = 0; i < qs.size(); i++) + if (value(qs[i]) != l_False) + qs[j++] = qs[i]; + qs.shrink(i - j); + } + const vec& ps = learnt || normalized ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals. + + if (ps.size() == 0) + return false; + else if (ps.size() == 1){ + assert(decisionLevel() == 0); + return enqueue(ps[0]); + }else{ + // Allocate clause: + Clause* c = Clause_new(ps, learnt); + + if (learnt){ + // Put the second watch on the first literal with highest decision level: + // (requires that this method is called at the level where the clause is asserting!) + int i; + for (i = 1; i < ps.size() && position(trailpos[var(ps[i])]) < trail_lim.last(); i++) + ; + (*c)[1] = ps[i]; + (*c)[i] = ps[1]; + + // Bump, enqueue, store clause: + claBumpActivity(*c); // (newly learnt clauses should be considered active) + check(enqueue((*c)[0], c)); + learnts.push(c); + stats.learnts_literals += c->size(); + }else{ + // Store clause: + clauses.push(c); + stats.clauses_literals += c->size(); + + if (subsumption){ + c->calcAbstraction(); + for (int i = 0; i < c->size(); i++){ + assert(!find(occurs[var((*c)[i])], c)); + occurs[var((*c)[i])].push(c); + n_occ[toInt((*c)[i])]++; + touched[var((*c)[i])] = 1; + + if (heap.inHeap(var((*c)[i]))) + updateHeap(var((*c)[i])); + } + } + + } + // Watch clause: + watches[toInt(~(*c)[0])].push(c); + watches[toInt(~(*c)[1])].push(c); + } + + return true; +} + + +// Disposes a clauses and removes it from watcher lists. NOTE! +// Low-level; does NOT change the 'clauses' and 'learnts' vector. +// +void Solver::removeClause(Clause& c, bool dealloc) +{ + //fprintf(stderr, "delete %d: ", _c); printClause(c); fprintf(stderr, "\n"); + assert(c.mark() == 0); + + if (c.size() > 1){ + assert(find(watches[toInt(~c[0])], &c)); + assert(find(watches[toInt(~c[1])], &c)); + remove(watches[toInt(~c[0])], &c); + remove(watches[toInt(~c[1])], &c); } + + if (c.learnt()) stats.learnts_literals -= c.size(); + else stats.clauses_literals -= c.size(); + + if (subsumption && !c.learnt()){ + for (int i = 0; i < c.size(); i++){ + if (dealloc){ + assert(find(occurs[var(c[i])], &c)); + remove(occurs[var(c[i])], &c); + } + n_occ[toInt(c[i])]--; + updateHeap(var(c[i])); + } + } + + if (dealloc) + xfree(&c); + else + c.mark(1); +} + + +bool Solver::satisfied(Clause& c) const +{ + for (int i = 0; i < c.size(); i++) + if (value(c[i]) == l_True) + return true; + return false; } + + +bool Solver::strengthen(Clause& c, Lit l) +{ + assert(decisionLevel() == 0); + assert(c.size() > 1); + assert(c.mark() == 0); + + assert(toInt(~c[0]) < watches.size()); + assert(toInt(~c[1]) < watches.size()); + + assert(find(watches[toInt(~c[0])], &c)); + assert(find(watches[toInt(~c[1])], &c)); + assert(find(c,l)); + + if (c.learnt()) stats.learnts_literals -= 1; + else stats.clauses_literals -= 1; + + if (c[0] == l || c[1] == l){ + assert(find(watches[toInt(~l)], &c)); + remove(c,l); + remove(watches[toInt(~l)], &c); + if (c.size() > 1){ + assert(!find(watches[toInt(~c[1])], &c)); + watches[toInt(~c[1])].push(&c); } + else { + assert(find(watches[toInt(~c[0])], &c)); + remove(watches[toInt(~c[0])], &c); + removeClause(c, false); + } + } + else + remove(c,l); + + assert(c.size() == 1 || find(watches[toInt(~c[0])], &c)); + assert(c.size() == 1 || find(watches[toInt(~c[1])], &c)); + + if (subsumption){ + assert(find(occurs[var(l)], &c)); + remove(occurs[var(l)], &c); + assert(!find(occurs[var(l)], &c)); + + c.calcAbstraction(); + + n_occ[toInt(l)]--; + updateHeap(var(l)); + } + + return c.size() == 1 ? enqueue(c[0]) : true; +} + + +//================================================================================================= +// Minor methods: + + +// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be +// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). +// +Var Solver::newVar(bool polarity, bool dvar) { + int index; + index = nVars(); + watches .push(); // (list for positive literal) + watches .push(); // (list for negative literal) + reason .push(NULL); + assigns .push(toInt(l_Undef)); + trailpos .push(TrailPos(0,0)); + activity .push(0); + order .newVar(polarity,dvar); + seen .push(0); + touched .push(0); + if (subsumption){ + occurs .push(); + n_occ .push(0); + n_occ .push(0); + heap .setBounds(index+1); + } + return index; } + + +// Returns FALSE if immediate conflict. +bool Solver::assume(Lit p) { + trail_lim.push(trail.size()); + return enqueue(p); } + + +// Revert to the state at given level. +void Solver::cancelUntil(int level) { + if (decisionLevel() > level){ + for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + Var x = var(trail[c]); + assigns[x] = toInt(l_Undef); + reason [x] = NULL; + order.undo(x); } + qhead = trail_lim[level]; + trail.shrink(trail.size() - trail_lim[level]); + trail_lim.shrink(trail_lim.size() - level); + } +} + + +//================================================================================================= +// Major methods: + + +/*_________________________________________________________________________________________________ +| +| analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] +| +| Description: +| Analyze conflict and produce a reason clause. +| +| Pre-conditions: +| * 'out_learnt' is assumed to be cleared. +| * Current decision level must be greater than root level. +| +| Post-conditions: +| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +| +| Effect: +| Will undo part of the trail, upto but not beyond the assumption of the current decision level. +|________________________________________________________________________________________________@*/ +void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) +{ + int pathC = 0; + int btpos = -1; + Lit p = lit_Undef; + + // Generate conflict clause: + // + out_learnt.push(); // (leave room for the asserting literal) + int index = trail.size()-1; + do{ + assert(confl != NULL); // (otherwise should be UIP) + Clause& c = *confl; + + if (c.learnt()) + claBumpActivity(c); + + for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ + Lit q = c[j]; + if (!seen[var(q)] && position(trailpos[var(q)]) >= trail_lim[0]){ + varBumpActivity(q); + seen[var(q)] = 1; + if (position(trailpos[var(q)]) >= trail_lim.last()) + pathC++; + else{ + out_learnt.push(q); + btpos = max(btpos, position(trailpos[var(q)])); + } + } + } + + // Select next clause to look at: + while (!seen[var(trail[index--])]); + p = trail[index+1]; + confl = reason[var(p)]; + seen[var(p)] = 0; + pathC--; + + }while (pathC > 0); + out_learnt[0] = ~p; + + // Find correct backtrack level + for (out_btlevel = trail_lim.size()-1; out_btlevel > 0 && trail_lim[out_btlevel-1] > btpos; out_btlevel--) + ; + + int i, j; + if (expensive_ccmin){ + // Simplify conflict clause (a lot): + // + uint min_level = 0; + for (i = 1; i < out_learnt.size(); i++) + min_level |= abstractLevel(trailpos[var(out_learnt[i])]); // (maintain an abstraction of levels involved in conflict) + + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) + if (reason[var(out_learnt[i])] == NULL || !analyze_removable(out_learnt[i], min_level)) + out_learnt[j++] = out_learnt[i]; + }else{ + // Simplify conflict clause (a little): + // + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++){ + Clause& c = *reason[var(out_learnt[i])]; + for (int k = 1; k < c.size(); k++) + if (!seen[var(c[k])] && position(trailpos[var(c[k])]) >= trail_lim[0]){ + out_learnt[j++] = out_learnt[i]; + break; } + } + } + + stats.max_literals += out_learnt.size(); + out_learnt.shrink(i - j); + stats.tot_literals += out_learnt.size(); + + for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) +} + + +// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed. +// +bool Solver::analyze_removable(Lit p, uint min_level) +{ + analyze_stack.clear(); analyze_stack.push(p); + int top = analyze_toclear.size(); + while (analyze_stack.size() > 0){ + assert(reason[var(analyze_stack.last())] != NULL); + Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); + + for (int i = 1; i < c.size(); i++){ + Lit p = c[i]; + TrailPos tp = trailpos[var(p)]; + if (!seen[var(p)] && position(tp) >= trail_lim[0]){ + if (reason[var(p)] != NULL && (abstractLevel(tp) & min_level) != 0){ + seen[var(p)] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + }else{ + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } + } + } + } + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +void Solver::analyzeFinal(Lit p, vec& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[var(p)] = 1; + + int start = position(trailpos[var(p)]); + for (int i = start; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); + if (seen[x]){ + if (reason[x] == NULL){ + assert(position(trailpos[x]) >= trail_lim[0]); + out_conflict.push(~trail[i]); + }else{ + Clause& c = *reason[x]; + for (int j = 1; j < c.size(); j++) + if (position(trailpos[var(c[j])]) >= trail_lim[0]) + seen[var(c[j])] = 1; + } + seen[x] = 0; + } + } +} + + +/*_________________________________________________________________________________________________ +| +| enqueue : (p : Lit) (from : Clause*) -> [bool] +| +| Description: +| Puts a new fact on the propagation queue as well as immediately updating the variable's value. +| Should a conflict arise, FALSE is returned. +| +| Input: +| p - The fact to enqueue +| from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'. +| Default value is NULL (no reason). +| +| Output: +| TRUE if fact was enqueued without conflict, FALSE otherwise. +|________________________________________________________________________________________________@*/ +bool Solver::enqueue(Lit p, Clause* from) +{ + + if (value(p) != l_Undef) + return value(p) != l_False; + else{ + assigns [var(p)] = toInt(lbool(!sign(p))); + trailpos[var(p)] = TrailPos(trail.size(),decisionLevel()); + reason [var(p)] = from; + trail.push(p); + return true; + } +} + + +/*_________________________________________________________________________________________________ +| +| propagate : [void] -> [Clause*] +| +| Description: +| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, +| otherwise NULL. +| +| Post-conditions: +| * the propagation queue is empty, even if there was a conflict. +|________________________________________________________________________________________________@*/ +Clause* Solver::propagate() +{ + if (decisionLevel() == 0 && subsumption) + return backwardSubsumptionCheck() ? NULL : propagate_tmpempty; + + Clause* confl = NULL; + //fprintf(stderr, "propagate, qhead = %d, qtail = %d\n", qhead, qtail); + while (qhead < trail.size()){ + stats.propagations++; + simpDB_props--; + + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec& ws = watches[toInt(p)]; + Clause **i, **j, **end; + + for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){ + Clause& c = **i++; + + // Make sure the false literal is data[1]: + Lit false_lit = ~p; + if (c[0] == false_lit) + c[0] = c[1], c[1] = false_lit; + + assert(c[1] == false_lit); + + // If 0th watch is true, then clause is already satisfied. + Lit first = c[0]; + if (value(first) == l_True){ + *j++ = &c; + }else{ + // Look for new watch: + for (int k = 2; k < c.size(); k++) + if (value(c[k]) != l_False){ + c[1] = c[k]; c[k] = false_lit; + watches[toInt(~c[1])].push(&c); + goto FoundWatch; } + + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + if (!enqueue(first, &c)){ + confl = &c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + FoundWatch:; + } + } + ws.shrink(i - j); + } + + return confl; +} + + +/*_________________________________________________________________________________________________ +| +| reduceDB : () -> [void] +| +| Description: +| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked +| 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()); } }; +void Solver::reduceDB() +{ + int i, j; + double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + + sort(learnts, reduceDB_lt()); + for (i = j = 0; i < learnts.size() / 2; i++){ + if (learnts[i]->size() > 2 && !locked(*learnts[i])) + 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.shrink(i - j); +} + + +/*_________________________________________________________________________________________________ +| +| simplifyDB : [void] -> [bool] +| +| Description: +| Simplify the clause database according to the current top-level assigment. Currently, the only +| thing done here is the removal of satisfied clauses, but more things can be put here. +|________________________________________________________________________________________________@*/ +bool Solver::simplifyDB(bool expensive) +{ + assert(decisionLevel() == 0); + if (!ok || propagate() != NULL) + return ok = false; + + if (nAssigns() == simpDB_assigns || + (!subsumption && simpDB_props > 0)) // (nothing has changed or preformed a simplification too recently) + return true; + + if (subsumption){ + if (expensive && !eliminate()) + return ok = false; + + // Move this cleanup code to its own method ? + int i , j; + vec dirty; + for (i = 0; i < clauses.size(); i++) + if (clauses[i]->mark() == 1){ + Clause& c = *clauses[i]; + for (int k = 0; k < c.size(); k++) + if (!seen[var(c[k])]){ + seen[var(c[k])] = 1; + dirty.push(var(c[k])); + } + } + + for (i = 0; i < dirty.size(); i++){ + cleanOcc(dirty[i]); + seen[dirty[i]] = 0; + } + + for (i = j = 0; i < clauses.size(); i++) + if (clauses[i]->mark() == 1) + xfree(clauses[i]); + else + clauses[j++] = clauses[i]; + clauses.shrink(i - j); + } + + // Remove satisfied clauses: + for (int type = 0; type < (subsumption ? 1 : 2); type++){ // (only scan learnt clauses if subsumption is on) + vec& cs = type ? learnts : clauses; + int j = 0; + for (int i = 0; i < cs.size(); i++){ + assert(cs[i]->mark() == 0); + if (satisfied(*cs[i])) + removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(cs.size()-j); + } + order.cleanup(); + + simpDB_assigns = nAssigns(); + simpDB_props = stats.clauses_literals + stats.learnts_literals; // (shouldn't depend on 'stats' really, but it will do for now) + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] +| +| Description: +| Search for a model the specified number of conflicts, keeping the number of learnt clauses +| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to +| indicate infinity. +| +| Output: +| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If +| 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) +{ + assert(ok); + int backtrack_level; + int conflictC = 0; + vec learnt_clause; + + stats.starts++; + var_decay = 1 / params.var_decay; + cla_decay = 1 / params.clause_decay; + + for (;;){ + Clause* confl = propagate(); + if (confl != NULL){ + // CONFLICT + stats.conflicts++; conflictC++; + if (decisionLevel() == 0) return l_False; + + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); + newClause(learnt_clause, true); + varDecayActivity(); + claDecayActivity(); + + }else{ + // NO CONFLICT + + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + return l_Undef; } + + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && !simplifyDB()) + return l_False; + + if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) + // Reduce the set of learnt clauses: + reduceDB(); + + Lit next = lit_Undef; + + if (decisionLevel() < assumptions.size()){ + // Perform user provided assumption: + next = assumptions[decisionLevel()]; + if (value(next) == l_False){ + analyzeFinal(~next, conflict); + return l_False; } + }else{ + // New variable decision: + stats.decisions++; + next = order.select(params.random_var_freq, decisionLevel()); + } + if (next == lit_Undef) + // Model found: + return l_True; + + check(assume(next)); + } + } +} + + +// Return search-space coverage. Not extremely reliable. +// +double Solver::progressEstimate() +{ + double progress = 0; + double F = 1.0 / nVars(); + + for (int i = 0; i <= decisionLevel(); i++){ + int beg = i == 0 ? 0 : trail_lim[i - 1]; + int end = i == decisionLevel() ? trail.size() : trail_lim[i]; + progress += pow(F, i) * (end - beg); + } + + return progress / nVars(); +} + + +// Divide all variable activities by 1e100. +// +void Solver::varRescaleActivity() +{ + for (int i = 0; i < nVars(); i++) + activity[i] *= 1e-100; + var_inc *= 1e-100; +} + + +// Divide all constraint activities by 1e100. +// +void Solver::claRescaleActivity() +{ + for (int i = 0; i < learnts.size(); i++) + learnts[i]->activity() *= 1e-20; + cla_inc *= 1e-20; +} + + +/*_________________________________________________________________________________________________ +| +| solve : (assumps : const vec&) -> [bool] +| +| Description: +| Top-level solve. +|________________________________________________________________________________________________@*/ +bool Solver::solve(const vec& assumps) +{ + model.clear(); + conflict.clear(); + + if (!simplifyDB(true)) return false; + + + double nof_conflicts = params.restart_first; + double nof_learnts = nClauses() * params.learntsize_factor; + lbool status = l_Undef; + assumps.copyTo(assumptions); + + if (verbosity >= 1){ + reportf("==================================[MINISAT]====================================\n"); + reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); + reportf("===============================================================================\n"); + } + + // Search: + while (status == l_Undef){ + if (verbosity >= 1) + //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + status = search((int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= params.restart_inc; + nof_learnts *= params.learntsize_inc; + } + + if (verbosity >= 1) + reportf("==============================================================================\n"); + + if (status == l_True){ + // Copy model: + extendModel(); +#if 1 + //fprintf(stderr, "Verifying model.\n"); + for (int i = 0; i < clauses.size(); i++) + assert(satisfied(*clauses[i])); + for (int i = 0; i < eliminated.size(); i++) + assert(satisfied(*eliminated[i])); +#endif + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); + }else{ + assert(status == l_False); + if (conflict.size() == 0) + ok = false; + } + + cancelUntil(0); + return status == l_True; +} +};//end of MINISAT namespace -- cgit 1.4.1