+++ /dev/null
-/************************************************************************************[UnsoundSimpSolver.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 <math.h>
-#include "Sort.h"
-#include "UnsoundSimpSolver.h"
-
-
-namespace MINISAT {
-
-//=================================================================================================
-// Constructor/Destructor:
-
-
-UnsoundSimpSolver::UnsoundSimpSolver() :
- grow (0)
- , asymm_mode (false)
- , redundancy_check (false)
- , merges (0)
- , asymm_lits (0)
- , remembered_clauses (0)
- , elimorder (1)
- , use_simplification (true)
- , elim_heap (ElimLt(n_occ))
- , bwdsub_assigns (0)
-{
- vec<Lit> dummy(1,lit_Undef);
- bwdsub_tmpunit = Clause_new(dummy);
- remove_satisfied = false;
-}
-
-
-UnsoundSimpSolver::~UnsoundSimpSolver()
-{
- free(bwdsub_tmpunit);
-
- // NOTE: elimtable.size() might be lower than nVars() at the moment
- for (int i = 0; i < elimtable.size(); i++)
- for (int j = 0; j < elimtable[i].eliminated.size(); j++)
- free(elimtable[i].eliminated[j]);
-}
-
-
-Var UnsoundSimpSolver::newVar(bool sign, bool dvar) {
- Var v = Solver::newVar(sign, dvar);
-
- if (use_simplification){
- n_occ .push(0);
- n_occ .push(0);
- occurs .push();
- frozen .push((char)false);
- touched .push(0);
- elim_heap.insert(v);
- elimtable.push();
- }
- return v; }
-
-
-
-bool UnsoundSimpSolver::solve(const vec<Lit>& assumps, bool do_simp, bool turn_off_simp) {
- vec<Var> extra_frozen;
- bool result = true;
-
- do_simp &= use_simplification;
-
- //if (do_simp){
- // Assumptions must be temporarily frozen to run variable elimination:
- for (int i = 0; i < assumps.size(); i++){
- Var v = var(assumps[i]);
-
- // If an assumption has been eliminated, remember it.
- if (isEliminated(v))
- remember(v);
-
- if (!frozen[v]){
- // Freeze and store.
- setFrozen(v, true);
- extra_frozen.push(v);
- } }
-
- result = eliminate(turn_off_simp);
- //}
- //
-
- if (result)
- result = Solver::solve(assumps);
-
- if (result) {
- extendModel();
- //#ifndef NDEBUG
- verifyModel();
- //#endif
- }
-
- if (do_simp)
- // Unfreeze the assumptions that were frozen:
- for (int i = 0; i < extra_frozen.size(); i++)
- setFrozen(extra_frozen[i], false);
-
- return result;
-}
-
-
-
-bool UnsoundSimpSolver::addClause(vec<Lit>& ps)
-{
- for (int i = 0; i < ps.size(); i++)
- if (isEliminated(var(ps[i])))
- remember(var(ps[i]));
-
- int nclauses = clauses.size();
-
- if (redundancy_check && implied(ps))
- return true;
-
- if (!Solver::addClause(ps))
- return false;
-
- if (use_simplification && clauses.size() == nclauses + 1){
- Clause& c = *clauses.last();
-
- subsumption_queue.insert(&c);
-
- for (int i = 0; i < c.size(); i++){
- assert(occurs.size() > var(c[i]));
- assert(!find(occurs[var(c[i])], &c));
-
- occurs[var(c[i])].push(&c);
- n_occ[toInt(c[i])]++;
- touched[var(c[i])] = 1;
- assert(elimtable[var(c[i])].order == 0);
- if (elim_heap.inHeap(var(c[i])))
- elim_heap.increase_(var(c[i]));
- }
- }
-
- return true;
-}
-
-
-void UnsoundSimpSolver::removeClause(Clause& c)
-{
- assert(!c.learnt());
-
- if (use_simplification)
- for (int i = 0; i < c.size(); i++){
- n_occ[toInt(c[i])]--;
- updateElimHeap(var(c[i]));
- }
-
- detachClause(c);
- c.mark(1);
-}
-
-
-bool UnsoundSimpSolver::strengthenClause(Clause& c, Lit l)
-{
- assert(decisionLevel() == 0);
- assert(c.mark() == 0);
- assert(!c.learnt());
- assert(find(watches[toInt(~c[0])], &c));
- assert(find(watches[toInt(~c[1])], &c));
-
- // FIX: this is too inefficient but would be nice to have (properly implemented)
- // if (!find(subsumption_queue, &c))
- subsumption_queue.insert(&c);
-
- // If l is watched, delete it from watcher list and watch a new literal
- if (c[0] == l || c[1] == l){
- Lit other = c[0] == l ? c[1] : c[0];
- if (c.size() == 2){
- removeClause(c);
- c.strengthen(l);
- }else{
- c.strengthen(l);
- remove(watches[toInt(~l)], &c);
-
- // Add a watch for the correct literal
- watches[toInt(~(c[1] == other ? c[0] : c[1]))].push(&c);
-
- // !! this version assumes that remove does not change the order !!
- //watches[toInt(~c[1])].push(&c);
- clauses_literals -= 1;
- }
- }
- else{
- c.strengthen(l);
- clauses_literals -= 1;
- }
-
- // if subsumption-indexing is active perform the necessary updates
- if (use_simplification){
- remove(occurs[var(l)], &c);
- n_occ[toInt(l)]--;
- updateElimHeap(var(l));
- }
-
- return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true;
-}
-
-
-// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
-bool UnsoundSimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
-{
- merges++;
- out_clause.clear();
-
- 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;
-}
-
-
-// Returns FALSE if clause is always satisfied.
-bool UnsoundSimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
-{
- merges++;
-
- bool ps_smallest = _ps.size() < _qs.size();
- const Clause& ps = ps_smallest ? _qs : _ps;
- const Clause& qs = ps_smallest ? _ps : _qs;
- const Lit* __ps = (const Lit*)ps;
- const Lit* __qs = (const Lit*)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;
- }
- next:;
- }
-
- return true;
-}
-
-
-void UnsoundSimpSolver::gatherTouchedClauses()
-{
- //fprintf(stderr, "Gathering clauses for backwards subsumption\n");
- int ntouched = 0;
- for (int i = 0; i < touched.size(); i++)
- if (touched[i]){
- const vec<Clause*>& cs = getOccurs(i);
- ntouched++;
- for (int j = 0; j < cs.size(); j++)
- if (cs[j]->mark() == 0){
- subsumption_queue.insert(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 < subsumption_queue.size(); i++)
- subsumption_queue[i]->mark(0);
-}
-
-
-bool UnsoundSimpSolver::implied(const vec<Lit>& c)
-{
- assert(decisionLevel() == 0);
-
- trail_lim.push(trail.size());
- for (int i = 0; i < c.size(); i++)
- if (value(c[i]) == l_True){
- cancelUntil(0);
- return false;
- }else if (value(c[i]) != l_False){
- assert(value(c[i]) == l_Undef);
- uncheckedEnqueue(~c[i]);
- }
-
- bool result = propagate() != NULL;
- cancelUntil(0);
- return result;
-}
-
-
-// Backward subsumption + backward subsumption resolution
-bool UnsoundSimpSolver::backwardSubsumptionCheck(bool verbose)
-{
- int cnt = 0;
- int subsumed = 0;
- int deleted_literals = 0;
- assert(decisionLevel() == 0);
-
- while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
-
- // Check top-level assignments by creating a dummy clause and placing it in the queue:
- if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
- Lit l = trail[bwdsub_assigns++];
- (*bwdsub_tmpunit)[0] = l;
- bwdsub_tmpunit->calcAbstraction();
- assert(bwdsub_tmpunit->mark() == 0);
- subsumption_queue.insert(bwdsub_tmpunit); }
-
- Clause& c = *subsumption_queue.peek(); subsumption_queue.pop();
-
- if (c.mark()) continue;
-
- if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
- reportf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
-
- assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
-
- // 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]);
-
- // Search all candidates:
- vec<Clause*>& _cs = getOccurs(best);
- Clause** cs = (Clause**)_cs;
-
- for (int j = 0; j < _cs.size(); j++)
- if (c.mark())
- break;
- else if (!cs[j]->mark() && cs[j] != &c){
- Lit l = c.subsumes(*cs[j]);
-
- if (l == lit_Undef)
- subsumed++, removeClause(*cs[j]);
- else if (l != lit_Error){
- deleted_literals++;
-
- if (!strengthenClause(*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 UnsoundSimpSolver::asymm(Var v, Clause& c)
-{
- assert(decisionLevel() == 0);
-
- if (c.mark() || satisfied(c)) return true;
-
- trail_lim.push(trail.size());
- Lit l = lit_Undef;
- for (int i = 0; i < c.size(); i++)
- if (var(c[i]) != v && value(c[i]) != l_False)
- uncheckedEnqueue(~c[i]);
- else
- l = c[i];
-
- if (propagate() != NULL){
- cancelUntil(0);
- asymm_lits++;
- if (!strengthenClause(c, l))
- return false;
- }else
- cancelUntil(0);
-
- return true;
-}
-
-
-bool UnsoundSimpSolver::asymmVar(Var v)
-{
- assert(!frozen[v]);
- assert(use_simplification);
-
- vec<Clause*> pos, neg;
- const vec<Clause*>& cls = getOccurs(v);
-
- if (value(v) != l_Undef || cls.size() == 0)
- return true;
-
- for (int i = 0; i < cls.size(); i++)
- if (!asymm(v, *cls[i]))
- return false;
-
- return backwardSubsumptionCheck();
-}
-
-
-void UnsoundSimpSolver::verifyModel()
-{
- bool failed = false;
- int cnt = 0;
- // NOTE: elimtable.size() might be lower than nVars() at the moment
- for (int i = 0; i < elimtable.size(); i++)
- if (elimtable[i].order > 0)
- for (int j = 0; j < elimtable[i].eliminated.size(); j++){
- cnt++;
- Clause& c = *elimtable[i].eliminated[j];
- for (int k = 0; k < c.size(); k++)
- if (modelValue(c[k]) == l_True)
- goto next;
-
- reportf("unsatisfied clause: ");
- printClause(*elimtable[i].eliminated[j]);
- reportf("\n");
- failed = true;
- next:;
- }
-
- assert(!failed);
- reportf("Verified %d eliminated clauses.\n", cnt);
-}
-
-
-bool UnsoundSimpSolver::eliminateVar(Var v, bool fail, bool stop_unsoundness)
-{
- if (!fail && asymm_mode && !asymmVar(v)) return false;
-
- const vec<Clause*>& cls = getOccurs(v);
-
-// if (value(v) != l_Undef || cls.size() == 0) return true;
- if (value(v) != l_Undef) return true;
-
- // Split the occurrences into positive and negative:
- vec<Clause*> pos, neg;
- for (int i = 0; i < cls.size(); i++)
- (find(*cls[i], Lit(v)) ? pos : neg).push(cls[i]);
-
- // Check if number of clauses decreases:
- int cnt = 0;
- for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(*pos[i], *neg[j], v) && ++cnt > cls.size() + grow)
- return true;
-
- // Delete and store old clauses:
- setDecisionVar(v, false);
- elimtable[v].order = elimorder++;
- assert(elimtable[v].eliminated.size() == 0);
- for (int i = 0; i < cls.size(); i++){
- elimtable[v].eliminated.push(Clause_new(*cls[i]));
- removeClause(*cls[i]); }
-
- // Produce clauses in cross product:
- int top = clauses.size();
- vec<Lit> resolvent;
- for (int i = 0; i < pos.size(); i++)
- for (int j = 0; j < neg.size(); j++)
- if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
- return false;
-
-
- if(!stop_unsoundness)
- {
- //abductive logic
- vec<Lit > resolvedClauses;
- for (int i = 0; i < pos.size(); i++) {
- for (int j = 0; j < pos.size(); j++) {
- if(i == j)
- continue;
- abductive_merge(*pos[i], *pos[j], v, resolvedClauses, true);
- if(!addClause(resolvedClauses))
- return false;
- }
- }
- //}
-
- resolvedClauses.clear();
- for (int i = 0; i < neg.size(); i++) {
- for (int j = 0; j < neg.size(); j++) {
- if(i == j)
- continue;
- abductive_neg_merge(*neg[i], *neg[j], v, resolvedClauses,true);
- if(!addClause(resolvedClauses))
- return false;
- }
- }
- }
-
- // DEBUG: For checking that a clause set is saturated with respect
- // to variable elimination. If the clause set is expected
- // to be saturated at this point, this constitutes an
- // error.
- if (fail){
- reportf("eliminated var %d, %d <= %d\n", v+1, cnt, cls.size());
- reportf("previous clauses:\n");
- for (int i = 0; i < cls.size(); i++){
- printClause(*cls[i]); reportf("\n"); }
- reportf("new clauses:\n");
- for (int i = top; i < clauses.size(); i++){
- printClause(*clauses[i]); reportf("\n"); }
- assert(0); }
-
- return backwardSubsumptionCheck();
-}
-
-
-void UnsoundSimpSolver::remember(Var v)
-{
- assert(decisionLevel() == 0);
- assert(isEliminated(v));
-
- vec<Lit> clause;
-
- // Re-activate variable:
- elimtable[v].order = 0;
- setDecisionVar(v, true); // Not good if the variable wasn't a decision variable before. Not sure how to fix this right now.
-
- if (use_simplification)
- updateElimHeap(v);
-
- // Reintroduce all old clauses which may implicitly remember other clauses:
- for (int i = 0; i < elimtable[v].eliminated.size(); i++){
- Clause& c = *elimtable[v].eliminated[i];
- clause.clear();
- for (int j = 0; j < c.size(); j++)
- clause.push(c[j]);
-
- remembered_clauses++;
- check(addClause(clause));
- free(&c);
- }
-
- elimtable[v].eliminated.clear();
-}
-
-
-void UnsoundSimpSolver::extendModel()
-{
- vec<Var> vs;
-
- // NOTE: elimtable.size() might be lower than nVars() at the moment
- for (int v = 0; v < elimtable.size(); v++)
- if (elimtable[v].order > 0)
- vs.push(v);
-
- sort(vs, ElimOrderLt(elimtable));
-
- for (int i = 0; i < vs.size(); i++){
- Var v = vs[i];
- Lit l = lit_Undef;
-
- for (int j = 0; j < elimtable[v].eliminated.size(); j++){
- Clause& c = *elimtable[v].eliminated[j];
-
- for (int k = 0; k < c.size(); k++)
- if (var(c[k]) == v)
- l = c[k];
- else if (modelValue(c[k]) != l_False)
- goto next;
-
- assert(l != lit_Undef);
- model[v] = lbool(!sign(l));
- break;
-
- next:;
- }
-
- if (model[v] == l_Undef)
- model[v] = l_True;
- }
-}
-
-
-bool UnsoundSimpSolver::eliminate(bool turn_off_elim)
-{
- if (!ok || !use_simplification)
- return ok;
-
- // Main simplification loop:
- //assert(subsumption_queue.size() == 0);
- //gatherTouchedClauses();
- while (subsumption_queue.size() > 0 || elim_heap.size() > 0){
-
- //fprintf(stderr, "subsumption phase: (%d)\n", subsumption_queue.size());
- if (!backwardSubsumptionCheck(true))
- return false;
-
- //fprintf(stderr, "elimination phase:\n (%d)", elim_heap.size());
- for (int cnt = 0; !elim_heap.empty(); cnt++){
- bool stop_unsoundness = true;
- if(cnt > log(nClauses())) {
- stop_unsoundness = false;
- //return true;
- }
-
- Var elim = elim_heap.removeMin();
-
- if (verbosity >= 2 && cnt % 100 == 0)
- reportf("elimination left: %10d\r", elim_heap.size());
-
- if (!frozen[elim] && !eliminateVar(elim, false, stop_unsoundness))
- return false;
- }
-
- assert(subsumption_queue.size() == 0);
- gatherTouchedClauses();
- }
-
- // Cleanup:
- cleanUpClauses();
- order_heap.filter(VarFilter(*this));
-
-#ifdef INVARIANTS
- // Check that no more subsumption is possible:
- reportf("Checking that no more subsumption is possible\n");
- for (int i = 0; i < clauses.size(); i++){
- if (i % 1000 == 0)
- reportf("left %10d\r", clauses.size() - i);
-
- assert(clauses[i]->mark() == 0);
- for (int j = 0; j < i; j++)
- assert(clauses[i]->subsumes(*clauses[j]) == lit_Error);
- }
- reportf("done.\n");
-
- // Check that no more elimination is possible:
- reportf("Checking that no more elimination is possible\n");
- for (int i = 0; i < nVars(); i++)
- if (!frozen[i]) eliminateVar(i, true, true);
- reportf("done.\n");
- checkLiteralCount();
-#endif
-
- // If no more simplification is needed, free all simplification-related data structures:
- if (turn_off_elim){
- use_simplification = false;
- touched.clear(true);
- occurs.clear(true);
- n_occ.clear(true);
- subsumption_queue.clear(true);
- elim_heap.clear(true);
- remove_satisfied = true;
- }
-
-
- return true;
-}
-
-
-void UnsoundSimpSolver::cleanUpClauses()
-{
- int i , j;
- vec<Var> 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)
- free(clauses[i]);
- else
- clauses[j++] = clauses[i];
- clauses.shrink(i - j);
-}
-
-
-//=================================================================================================
-// Convert to DIMACS:
-
-
-void UnsoundSimpSolver::toDimacs(FILE* f, Clause& c)
-{
- if (satisfied(c)) return;
-
- for (int i = 0; i < c.size(); i++)
- if (value(c[i]) != l_False)
- fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", var(c[i])+1);
- fprintf(f, "0\n");
-}
-
-
-void UnsoundSimpSolver::toDimacs(const char* file)
-{
- assert(decisionLevel() == 0);
- FILE* f = fopen(file, "wr");
- if (f != NULL){
-
- // Cannot use removeClauses here because it is not safe
- // to deallocate them at this point. Could be improved.
- int cnt = 0;
- for (int i = 0; i < clauses.size(); i++)
- if (!satisfied(*clauses[i]))
- cnt++;
-
- fprintf(f, "p cnf %d %d\n", nVars(), cnt);
-
- for (int i = 0; i < clauses.size(); i++)
- toDimacs(f, *clauses[i]);
-
- fprintf(stderr, "Wrote %d clauses...\n", clauses.size());
- }else
- fprintf(stderr, "could not open file %s\n", file);
-}
-
-
-// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
-bool UnsoundSimpSolver::abductive_merge(const Clause& _ps,
- const Clause& _qs,
- Var v,
- vec<Lit>& out_clause, bool s) {
- merges++;
- out_clause.clear();
-
- 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)
- out_clause.push(qs[i]);
- }
-
- for (int j = 0; j < ps.size(); j++) {
- if(var(ps[j]) != v)
- out_clause.push(ps[j]);
- }
-
- return true;
-} //end of abductive_merge()
-
-// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
-bool UnsoundSimpSolver::abductive_neg_merge(const Clause& _ps,
- const Clause& _qs,
- Var v, vec<Lit>& out_clause, bool s) {
- merges++;
- out_clause.clear();
-
- bool ps_smallest = _ps.size() < _qs.size();
- const Clause& ps = ps_smallest ? _qs : _ps;
- const Clause& qs = ps_smallest ? _ps : _qs;
-
- //if(s) {
- for (int i = 0; i < qs.size(); i++){
- if (var(qs[i]) != v)
- out_clause.push(qs[i]);
- }
- //}
- //else {
- for (int j = 0; j < ps.size(); j++) {
- if(var(ps[j]) != v)
- out_clause.push(ps[j]);
- }
- //}
- return true;
-} //end of abductive_merge()
-};
+++ /dev/null
-/****************************************************************************
-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.
-***************************************************************************/
-
-#ifndef UnsoundSimpSolver_h
-#define UnsoundSimpSolver_h
-
-#include <cstdio>
-
-#include "../mtl/Queue.h"
-#include "../core/Solver.h"
-
-
-namespace MINISAT {
-
-class UnsoundSimpSolver : public Solver {
- public:
- // Constructor/Destructor:
- //
- UnsoundSimpSolver();
- ~UnsoundSimpSolver();
-
- // Problem specification:
- //
- Var newVar (bool polarity = true, bool dvar = true);
- bool addClause (vec<Lit>& ps);
-
- // Variable mode:
- //
- void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
-
- // Solving:
- //
- bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
- bool solve (bool do_simp = true, bool turn_off_simp = true);
- bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
-
- // Generate a (possibly simplified) DIMACS file:
- //
- void toDimacs (const char* file);
-
- // Mode of operation:
- //
- int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
- bool asymm_mode; // Shrink clauses by asymmetric branching.
- bool redundancy_check; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
-
- // Statistics:
- //
- int merges;
- int asymm_lits;
- int remembered_clauses;
-
-// protected:
- public:
-
- // Helper structures:
- //
- struct ElimData {
- int order; // 0 means not eliminated, >0 gives an index in the elimination order
- vec<Clause*> eliminated;
- ElimData() : order(0) {} };
-
- struct ElimOrderLt {
- const vec<ElimData>& elimtable;
- ElimOrderLt(const vec<ElimData>& et) : elimtable(et) {}
- bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } };
-
- struct ElimLt {
- const vec<int>& n_occ;
- ElimLt(const vec<int>& no) : n_occ(no) {}
- int cost (Var x) const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
- bool operator()(Var x, Var y) const { return cost(x) < cost(y); } };
-
-
- // Solver state:
- //
- int elimorder;
- bool use_simplification;
- vec<ElimData> elimtable;
- vec<char> touched;
- vec<vec<Clause*> > occurs;
- vec<int> n_occ;
- Heap<ElimLt> elim_heap;
- Queue<Clause*> subsumption_queue;
- vec<char> frozen;
- int bwdsub_assigns;
-
- // Temporaries:
- //
- Clause* bwdsub_tmpunit;
-
- // Main internal methods:
- //
- bool asymm (Var v, Clause& c);
- bool asymmVar (Var v);
- void updateElimHeap (Var v);
- void cleanOcc (Var v);
- vec<Clause*>& getOccurs (Var x);
- void gatherTouchedClauses ();
- bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
- bool merge (const Clause& _ps, const Clause& _qs, Var v);
- bool abductive_merge (const Clause& _ps,
- const Clause& _qs,
- Var v, vec<Lit >& out_clauses, bool s=true);
- bool abductive_neg_merge (const Clause& _ps,
- const Clause& _qs,
- Var v, vec<Lit>& out_clause, bool s=true);
-
- bool backwardSubsumptionCheck (bool verbose = false);
- bool eliminateVar (Var v, bool fail = false,
- bool stop_unsoundness=false);
- void remember (Var v);
- void extendModel ();
- void verifyModel ();
-
- void removeClause (Clause& c);
- bool strengthenClause (Clause& c, Lit l);
- void cleanUpClauses ();
- bool implied (const vec<Lit>& c);
- void toDimacs (FILE* f, Clause& c);
- bool isEliminated (Var v) const;
-
-};
-
-
-//=================================================================================================
-// Implementation of inline methods:
-
-inline void UnsoundSimpSolver::updateElimHeap(Var v) {
- if (elimtable[v].order == 0)
- elim_heap.update(v); }
-
-inline void UnsoundSimpSolver::cleanOcc(Var v) {
- assert(use_simplification);
- Clause **begin = (Clause**)occurs[v];
- Clause **end = begin + occurs[v].size();
- Clause **i, **j;
- for (i = begin, j = end; i < j; i++)
- if ((*i)->mark() == 1){
- *i = *(--j);
- i--;
- }
- //occurs[v].shrink_(end - j); // This seems slower. Why?!
- occurs[v].shrink(end - j);
-}
-
-inline vec<Clause*>& UnsoundSimpSolver::getOccurs(Var x) {
- cleanOcc(x); return occurs[x]; }
-
-inline bool UnsoundSimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; }
-inline void UnsoundSimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
-inline bool UnsoundSimpSolver::solve (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
-
-//=================================================================================================
-#endif
-};
projects / francis / stp.git / commitdiff