zchaff_solver.cpp

命题逻辑的求解器,2004年SAT竞赛第一名的求解器

// *********************************************************************
// Copyright 2000-2004, Princeton University.  All rights reserved.
// By using this software the USER indicates that he or she has read,
// understood and will comply with the following:
//
// --- Princeton University hereby grants USER nonexclusive permission
// to use, copy and/or modify this software for internal, noncommercial,
// research purposes only. Any distribution, including commercial sale
// or license, of this software, copies of the software, its associated
// documentation and/or modifications of either is strictly prohibited
// without the prior consent of Princeton University.  Title to copyright
// to this software and its associated documentation shall at all times
// remain with Princeton University.  Appropriate copyright notice shall
// be placed on all software copies, and a complete copy of this notice
// shall be included in all copies of the associated documentation.
// No right is  granted to use in advertising, publicity or otherwise
// any trademark, service mark, or the name of Princeton University.
//
//
// --- This software and any associated documentation is provided "as is"
//
// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
// PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
//
// Princeton University shall not be liable under any circumstances for
// any direct, indirect, special, incidental, or consequential damages
// with respect to any claim by USER or any third party on account of
// or arising from the use, or inability to use, this software or its
// associated documentation, even if Princeton University has been advised
// of the possibility of those damages.
// ********************************************************************

#include <iostream>
#include <algorithm>
#include <fstream>
#include <vector>
#include <map>
#include <set>
#include <queue>

using namespace std;

#include "zchaff_solver.h"

// #define VERIFY_ON

#ifdef VERIFY_ON
ofstream verify_out("resolve_trace");
#endif

void CSolver::re_init_stats(void) {
  _stats.is_mem_out           = false;
  _stats.outcome              = UNDETERMINED;
  _stats.next_restart         = _params.restart.first_restart;
  _stats.restart_incr         = _params.restart.backtrack_incr;
  _stats.next_cls_deletion    = _params.cls_deletion.interval;
  _stats.next_var_score_decay = _params.decision.decay_period;
  _stats.current_randomness   = _params.decision.base_randomness;

  _stats.total_bubble_move            = 0;
  _stats.num_decisions                = 0;
  _stats.num_decisions_stack_conf     = 0;
  _stats.num_decisions_vsids          = 0;
  _stats.num_decisions_shrinking      = 0;
  _stats.num_backtracks               = 0;
  _stats.max_dlevel                   = 0;
  _stats.num_implications             = 0;
  _stats.num_restarts                 = 0;
  _stats.num_del_orig_cls             = 0;
  _stats.num_shrinkings               = 0;
  _stats.start_cpu_time               = get_cpu_time();
  _stats.finish_cpu_time              = 0;
  _stats.random_seed                  = 0;
}

void CSolver::init_stats(void) {
  re_init_stats();

  _stats.been_reset                   = true;
  _stats.num_free_variables           = 0;
  _stats.num_free_branch_vars         = 0;
}

void CSolver::init_parameters(void) {
  _params.verbosity                           = 0;
  _params.time_limit                          = 3600 * 24;  // a day
  _params.shrinking.size                      = 95;
  _params.shrinking.enable                    = true;
  _params.shrinking.upper_bound               = 800;
  _params.shrinking.lower_bound               = 600;
  _params.shrinking.upper_delta               = -5;
  _params.shrinking.lower_delta               = 10;
  _params.shrinking.window_width              = 20;
  _params.shrinking.bound_update_frequency    = 20;

  _params.decision.base_randomness            = 0;
  _params.decision.decay_period               = 40;
  _params.decision.bubble_init_step           = 0x400;

  _params.cls_deletion.enable                 = true ;
  _params.cls_deletion.head_activity          = 500;
  _params.cls_deletion.tail_activity          = 10;
  _params.cls_deletion.head_num_lits          = 6;
  _params.cls_deletion.tail_num_lits          = 45;
  _params.cls_deletion.tail_vs_head           = 16;
  _params.cls_deletion.interval               = 600;

  _params.restart.enable                      = true;
  _params.restart.interval                    = 700;
  _params.restart.first_restart               = 7000;
  _params.restart.backtrack_incr              = 700;
}

CSolver::CSolver(void) {
  init_parameters();
  init_stats();
  _dlevel                       = 0;
  _force_terminate              = false;
  _implication_id               = 0;
  _num_marked                   = 0;
  _num_in_new_cl                = 0;
  _outside_constraint_hook      = NULL;
  _sat_hook                     = NULL;
}

CSolver::~CSolver(void) {
  while (!_assignment_stack.empty()) {
    delete _assignment_stack.back();
    _assignment_stack.pop_back();
  }
}

void CSolver::set_time_limit(float t) {
  _params.time_limit = t;
}

float CSolver::elapsed_cpu_time(void) {
  return get_cpu_time() - _stats.start_cpu_time;
}

float CSolver::cpu_run_time(void) {
  return (_stats.finish_cpu_time - _stats.start_cpu_time);
}

void CSolver::set_variable_number(int n) {
  assert(num_variables() == 0);
  CDatabase::set_variable_number(n);
  _stats.num_free_variables = num_variables();
  while (_assignment_stack.size() <= num_variables())
    _assignment_stack.push_back(new vector<int>);
  assert(_assignment_stack.size() == num_variables() + 1);
}

int CSolver::add_variable(void) {
  int num = CDatabase::add_variable();
  ++_stats.num_free_variables;
  while (_assignment_stack.size() <= num_variables())
    _assignment_stack.push_back(new vector<int>);
  assert(_assignment_stack.size() == num_variables() + 1);
  return num;
}

void CSolver::set_mem_limit(int s) {
  CDatabase::set_mem_limit(s);
}

void CSolver::set_randomness(int n) {
  _params.decision.base_randomness = n;
}

void CSolver::set_random_seed(int seed) {
  srand(seed);
}

void CSolver::enable_cls_deletion(bool allow) {
  _params.cls_deletion.enable = allow;
}

void CSolver::add_hook(HookFunPtrT fun, int interval) {
  pair<HookFunPtrT, int> a(fun, interval);
  _hooks.push_back(pair<int, pair<HookFunPtrT, int> > (0, a));
}

void CSolver::run_periodic_functions(void) {
  // a. restart
  if (_params.restart.enable && _stats.num_backtracks > _stats.next_restart &&
      _shrinking_cls.empty()) {
    _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
    delete_unrelevant_clauses();
    restart();
    if (_stats.num_restarts % 5 == 1)
      compact_lit_pool();
    cout << "\rDecision: " << _assignment_stack[0]->size() << "/"
         <<num_variables() << "\tTime: " << get_cpu_time() -
           _stats.start_cpu_time << "/" << _params.time_limit << flush;
  }

  // b. decay variable score
  if (_stats.num_backtracks > _stats.next_var_score_decay) {
    _stats.next_var_score_decay = _stats.num_backtracks +
                                  _params.decision.decay_period;
    decay_variable_score();
  }

  // c. run hook functions
  for (unsigned i = 0; i< _hooks.size(); ++i) {
    pair<int, pair<HookFunPtrT, int> > & hook = _hooks[i];
    if (_stats.num_decisions >= hook.first) {
      hook.first += hook.second.second;
      hook.second.first((void *) this);
    }
  }
}

void CSolver::init_solve(void) {
  CDatabase::init_stats();
  re_init_stats();
  _stats.been_reset = false;

  assert(_conflicts.empty());
  assert(_conflict_lits.empty());
  assert(_num_marked == 0);
  assert(_num_in_new_cl == 0);
  assert(_dlevel == 0);

  for (unsigned i = 0, sz = variables()->size(); i < sz; ++i) {
    variable(i).score(0) = variable(i).lits_count(0);
    variable(i).score(1) = variable(i).lits_count(1);
  }

  _ordered_vars.resize(num_variables());
  update_var_score();

  set_random_seed(_stats.random_seed);

  top_unsat_cls = clauses()->end();
  --top_unsat_cls;

  _stats.shrinking_benefit = 0;
  _shrinking_cls.clear();
  _stats.shrinking_cls_length = 0;
}

void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl) {
    assert(value == 0 || value == 1);
    CVariable & var = variable(v);
    assert(var.value() == UNKNOWN);
    assert(dl == dlevel());

    var.set_dlevel(dl);
    var.set_value(value);
    var.antecedent() = ante;
    var.assgn_stack_pos() = _assignment_stack[dl]->size();
    _assignment_stack[dl]->push_back(v * 2 + !value);
    set_var_value_BCP(v, value);

    ++_stats.num_implications ;
    if (var.is_branchable())
        --num_free_variables();
}

void CSolver::set_var_value_BCP(int v, int value) {
  vector<CLitPoolElement *> & watchs = variable(v).watched(value);
  for (vector <CLitPoolElement *>::iterator itr = watchs.begin();
       itr != watchs.end(); ++itr) {
    ClauseIdx cl_idx;
    CLitPoolElement * other_watched = *itr;
    CLitPoolElement * watched = *itr;
    int dir = watched->direction();
    CLitPoolElement * ptr = watched;
    while (true) {
      ptr += dir;
      if (ptr->val() <= 0) {  // reached one end of the clause
        if (dir == 1)  // reached the right end, i.e. spacing element is cl_id
          cl_idx = ptr->get_clause_index();
        if (dir == watched->direction()) {  // we haven't go both directions.
          ptr = watched;
          dir = -dir;                     // change direction, go the other way
          continue;
        }
        // otherwise, we have already go through the whole clause
        int the_value = literal_value(*other_watched);
        if (the_value == 0)  // a conflict
          _conflicts.push_back(cl_idx);
        else if (the_value != 1)  // i.e. unknown
          queue_implication(other_watched->s_var(), cl_idx);
        break;
      }
      if (ptr->is_watched()) {  // literal is the other watched lit, skip it.
        other_watched = ptr;
        continue;
      }
      if (literal_value(*ptr) == 0)  // literal value is 0, keep going
        continue;
      // now the literal's value is either 1 or unknown, watch it instead
      int v1 = ptr->var_index();
      int sign = ptr->var_sign();
      variable(v1).watched(sign).push_back(ptr);
      ptr->set_watch(dir);
      // remove the original watched literal from watched list
      watched->unwatch();
      *itr = watchs.back();  // copy the last element in it's place
      watchs.pop_back();     // remove the last element
      --itr;                 // do this so with don't skip one during traversal
      break;
    }
  }
}

void CSolver::unset_var_value(int v) {
  if (v == 0)
    return;
  CVariable & var = variable(v);
  var.set_value(UNKNOWN);
  var.set_antecedent(NULL_CLAUSE);
  var.set_dlevel(-1);
  var.assgn_stack_pos() = -1;

  if (var.is_branchable()) {
    ++num_free_variables();
    if (var.var_score_pos() < _max_score_pos)
      _max_score_pos = var.var_score_pos();
  }
}

void CSolver::dump_assignment_stack(ostream & os ) {
  os << "Assignment Stack:  ";
  for (int i = 0; i <= dlevel(); ++i) {
    os << "(" <<i << ":";
    for (unsigned j = 0; j < (*_assignment_stack[i]).size(); ++j) {
      os << ((*_assignment_stack[i])[j]&0x1?"-":"+")
         << ((*_assignment_stack[i])[j] >> 1) << " ";
    }
    os << ") " << endl;
  }
  os << endl;
}

void CSolver::dump_implication_queue(ostream & os) {
  _implication_queue.dump(os);
}

void CSolver::delete_clause_group(int gid) {
  assert(is_gid_allocated(gid));

  if (_stats.been_reset == false)
    reset();  // if delete some clause, then implication queue are invalidated

  for (vector<CClause>::iterator itr = clauses()->begin();
       itr != clauses()->end(); ++itr) {
    CClause & cl = *itr;
    if (cl.status() != DELETED_CL) {
      if (cl.gid(gid) == true) {
        mark_clause_deleted(cl);
      }
    }
  }

  // delete the index from variables
  for (vector<CVariable>::iterator itr = variables()->begin();
         itr != variables()->end(); ++itr) {
    for (unsigned i = 0; i < 2; ++i) {  // for each phase
      // delete the lit index from the vars
#ifdef KEEP_LIT_CLAUSES
      vector<ClauseIdx> & lit_clauses = (*itr).lit_clause(i);
      for (vector<ClauseIdx>::iterator itr1 = lit_clauses.begin();
           itr1 != lit_clauses.end(); ++itr1) {
        if (clause(*itr1).status() == DELETED_CL) {
          *itr1 = lit_clauses.back();
          lit_clauses.pop_back();
          --itr1;
        }
      }
#endif
      // delete the watched index from the vars
      vector<CLitPoolElement *> & watched = (*itr).watched(i);
      for (vector<CLitPoolElement *>::iterator itr1 = watched.begin();
           itr1 != watched.end(); ++itr1) {
        if ((*itr1)->val() <= 0) {
          *itr1 = watched.back();