zchaff_solver.cpp

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

        _shrinking_cls.insert(pair<int, int>
                 (variable(_conflict_lits[i]>>1).dlevel(), _conflict_lits[i]));
      }
      int prev_dl = _shrinking_cls.begin()->first;
      multimap<int, int>::iterator itr, itr_del;
      int last_dl = _shrinking_cls.rbegin()->first;

      bool found_gap = false;
      for (itr = _shrinking_cls.begin(); itr->first != last_dl;) {
        if (itr->first - prev_dl > 2) {
          found_gap = true;
          break;
        }
        prev_dl = itr->first;
        itr_del = itr;
        ++itr;
        _shrinking_cls.erase(itr_del);
      }
      if (found_gap && _shrinking_cls.size() > 0 && prev_dl < dlevel() - 1) {
        _stats.shrinking_cls_length = _conflict_lits.size();
        ++_stats.num_shrinkings;
        back_track(prev_dl + 1);
        _conflicts.clear();
#ifdef VERIFY_ON
        _resolvents.clear();
#endif
        _num_in_new_cl = 0;
        for (unsigned i = 0, sz = _conflict_lits.size(); i < sz; ++i)
          variable(_conflict_lits[i]>>1).set_new_cl_phase(UNKNOWN);
        _conflict_lits.clear();
        if (_stats.num_shrinkings %
            _params.shrinking.bound_update_frequency == 0 &&
            _recent_shrinkings.size() == _params.shrinking.window_width) {
          if (_stats.shrinking_benefit > _params.shrinking.upper_bound)
            _params.shrinking.size += _params.shrinking.upper_delta;
          else if (_stats.shrinking_benefit < _params.shrinking.lower_bound)
            _params.shrinking.size += _params.shrinking.lower_delta;
        }
        return prev_dl;
      }
    }
  }
  int back_dl = 0;
  int unit_lit = -1;

  for (unsigned i = 0; i < clause(added_cl).num_lits(); ++i) {
    int vid = clause(added_cl).literal(i).var_index();
    int sign =clause(added_cl).literal(i).var_sign();
    assert(variable(vid).value() != UNKNOWN);
    assert(literal_value(clause(added_cl).literal(i)) == 0);
    int dl = variable(vid).dlevel();
    if (dl < dlevel()) {
      if (dl > back_dl)
        back_dl = dl;
    } else {
      assert(unit_lit == -1);
      unit_lit = vid + vid + sign;
    }
  }
  if (back_dl == 0) {
    _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
    _stats.next_cls_deletion = _stats.num_backtracks +
                               _params.cls_deletion.interval;
  }

  back_track(back_dl + 1);
  queue_implication(unit_lit, added_cl);

  // after resolve the first conflict, others must also be resolved
  // for (unsigned i = 1; i < _conflicts.size(); ++i)
  //   assert(!is_conflicting(_conflicts[i]));

  _conflicts.clear();

  while (!_conflict_lits.empty()) {
    int svar = _conflict_lits.back();
    _conflict_lits.pop_back();
    CVariable & var = variable(svar >> 1);
    assert(var.new_cl_phase() == (unsigned)(svar & 0x1));
    --_num_in_new_cl;
    var.set_new_cl_phase(UNKNOWN);
  }
  assert(_num_in_new_cl == 0);
  return back_dl;
}

int CSolver::conflict_analysis_firstUIP(void) {
  int min_conf_id = _conflicts[0];
  int min_conf_length = -1;
  ClauseIdx cl;
  unsigned gflag;
  _mark_increase_score = false;
  if (_conflicts.size() > 1) {
    for (vector<ClauseIdx>::iterator ci = _conflicts.begin();
         ci != _conflicts.end(); ci++) {
      assert(_num_in_new_cl == 0);
      assert(dlevel() > 0);
      cl = *ci;
      mark_vars(cl, -1);
      // current dl must be the conflict cl.
      vector <int> & assignments = *_assignment_stack[dlevel()];
      // now add conflict lits, and unassign vars
      for (int i = assignments.size() - 1; i >= 0; --i) {
        int assigned = assignments[i];
        if (variable(assigned >> 1).is_marked()) {
          // this variable is involved in the conflict clause or its antecedent
          variable(assigned>>1).clear_marked();
          --_num_marked;
          ClauseIdx ante_cl = variable(assigned>>1).get_antecedent();
          if ( _num_marked == 0 ) {
            // the first UIP encountered, conclude add clause
            assert(variable(assigned>>1).new_cl_phase() == UNKNOWN);
            // add this assignment's reverse, e.g. UIP
            _conflict_lits.push_back(assigned ^ 0x1);
            ++_num_in_new_cl;
            variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1);
            break;
          } else {
            assert(ante_cl != NULL_CLAUSE);
            mark_vars(ante_cl, assigned >> 1);
          }
        }
      }
      if (min_conf_length == -1 ||
          (int)_conflict_lits.size() < min_conf_length) {
        min_conf_length = _conflict_lits.size();
        min_conf_id = cl;
      }

      for (vector<int>::iterator vi = _conflict_lits.begin(); vi !=
           _conflict_lits.end(); ++vi) {
        int s_var = *vi;
        CVariable & var = variable(s_var >> 1);
        assert(var.new_cl_phase() == (unsigned)(s_var & 0x1));
        var.set_new_cl_phase(UNKNOWN);
      }
      _num_in_new_cl = 0;
      _conflict_lits.clear();
#ifdef VERIFY_ON
      _resolvents.clear();
#endif
    }
  }

  assert(_num_marked == 0);
  cl = min_conf_id;
  clause(cl).activity() += 5;
  _mark_increase_score = true;
  mark_vars(cl, -1);
  gflag = clause(cl).gflag();
  vector <int> & assignments = *_assignment_stack[dlevel()];
  for (int i = assignments.size() - 1; i >= 0; --i) {
    int assigned = assignments[i];
    if (variable(assigned >> 1).is_marked()) {
      variable(assigned>>1).clear_marked();
      --_num_marked;
      ClauseIdx ante_cl = variable(assigned>>1).get_antecedent();
      if ( _num_marked == 0 ) {
        _conflict_lits.push_back(assigned ^ 0x1);
        ++_num_in_new_cl;
        variable(assigned >> 1).set_new_cl_phase((assigned ^ 0x1) & 0x1);
        break;
      } else {
        gflag |= clause(ante_cl).gflag();
        mark_vars(ante_cl, assigned >> 1);
        clause(ante_cl).activity() += 5;
      }
    }
  }
  return finish_add_conf_clause(gflag);
}

void CSolver::print_cls(ostream & os) {
  for (unsigned i = 0; i < clauses()->size(); ++i) {
    CClause & cl = clause(i);
    if (cl.status() == DELETED_CL)
      continue;
    if (cl.status() == ORIGINAL_CL) {
      os <<"0 ";
    } else {
      assert(cl.status() == CONFLICT_CL);
      os << "A ";
    }
    for (unsigned j = 1; j < 33; ++j)
      os << (cl.gid(j) ? 1 : 0);
    os << "\t";
    for (unsigned j = 0; j < cl.num_lits(); ++j) {
      os << (cl.literal(j).var_sign() ? "-":"")
         << cl.literal(j).var_index() << " ";
    }
    os <<"0" <<  endl;
  }
}

int CSolver::mem_usage(void) {
  int mem_dbase = CDatabase::mem_usage();
  int mem_assignment = 0;
  for (int i = 0; i < _stats.max_dlevel; ++i)
    mem_assignment += _assignment_stack[i]->capacity() * sizeof(int);
  mem_assignment += sizeof(vector<int>)* _assignment_stack.size();
  return mem_dbase + mem_assignment;
}

void CSolver::clean_up_dbase(void) {
  assert(dlevel() == 0);

  int mem_before = mem_usage();
  // 1. remove all the learned clauses
  for (vector<CClause>::iterator itr = clauses()->begin();
       itr != clauses()->end() - 1; ++itr) {
    CClause & cl = * itr;
    if (cl.status() != ORIGINAL_CL)
      mark_clause_deleted(cl);
  }
  // delete_unrelevant_clauses() is specialized using berkmin deletion strategy

  // 2. free up the mem for the vectors if possible
  for (unsigned i = 0; i < variables()->size(); ++i) {
    for (unsigned j = 0; j < 2; ++j) {  // both phase
      vector<CLitPoolElement *> watched;
      vector<CLitPoolElement *> & old_watched = variable(i).watched(j);
      watched.reserve(old_watched.size());
      for (vector<CLitPoolElement *>::iterator itr = old_watched.begin();
           itr != old_watched.end(); ++itr)
        watched.push_back(*itr);
        // because watched is a temp mem allocation, it will get deleted
        // out of the scope, but by swap it with the old_watched, the
        // contents are reserved.
        old_watched.swap(watched);
#ifdef KEEP_LIT_CLAUSES
        vector<int> lits_cls;
        vector<int> & old_lits_cls = variable(i).lit_clause(j);
        lits_cls.reserve(old_lits_cls.size());
        for (vector<int>::iterator itr1 = old_lits_cls.begin(); itr1 !=
            old_lits_cls.end(); ++itr1)
          lits_cls.push_back(*itr1);
        old_lits_cls.swap(lits_cls);
#endif
    }
  }

  int mem_after = mem_usage();
  if (_params.verbosity > 0) {
    cout << "Database Cleaned, releasing (approximately) "
         << mem_before - mem_after << " Bytes" << endl;
  }
}

void CSolver::update_var_score(void) {
  for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
    _ordered_vars[i-1].first = & variable(i);
    _ordered_vars[i-1].second = variable(i).score();
  }
  ::stable_sort(_ordered_vars.begin(), _ordered_vars.end(), cmp_var_stat);
  for (unsigned i = 0, sz =  _ordered_vars.size(); i < sz; ++i)
    _ordered_vars[i].first->set_var_score_pos(i);
  _max_score_pos = 0;
}

void CSolver::restart(void) {
  _stats.num_restarts += 1;
  if (_params.verbosity > 1 )
    cout << "Restarting ... " << endl;
  if (dlevel() > 0)
    back_track(1);
  assert(dlevel() == 0);
}

// this function can be called within a solving process. i.e. not after
// solve() terminate
int CSolver::add_clause_incr(int * lits, int num_lits, int gid) {
  // Do not mess up with shrinking.
  assert(!_params.shrinking.enable || _shrinking_cls.empty());
  unsigned gflag;

  if (gid == PERMANENT_GID)
    gflag = 0;
  else if (gid == VOLATILE_GID) {
    gflag = ~0x0;
  } else {
    assert(gid <= WORD_WIDTH && gid > 0);
    gflag = (1 << (gid - 1));
  }

  int cl = add_clause(lits, num_lits, gflag);
  if (cl < 0)
    return -1;
  clause(cl).set_status(ORIGINAL_CL);

  if (clause(cl).num_lits() == 1) {
    int var_idx = clause(cl).literal(0).var_index();
    if (literal_value(clause(cl).literal(0)) == 0 &&
        variable(var_idx).dlevel() == 0) {
      back_track(0);
      if (preprocess() == CONFLICT)
        _stats.outcome = UNSATISFIABLE;
    } else {
      if (dlevel() > 0)
        back_track(1);
      queue_implication(clause(cl).literal(0).s_var(), cl);
    }
    return cl;
  }

  for (unsigned i = 0, sz = clause(cl).num_lits(); i < sz; ++i) {
    int var_idx = lits[i] >> 1;
    int value = variable(var_idx).value();
    if (value == UNKNOWN)
      continue;
    if (variable(var_idx).dlevel() == 0 &&
        variable(var_idx).antecedent() == -1 &&
        literal_value(clause(cl).literal(i)) == 0) {
      back_track(0);
      if (preprocess() == CONFLICT)
        _stats.outcome = UNSATISFIABLE;
      return cl;
    }
  }

  int max_level = 0;
  int max_level2 = 0;
  int unit_lit = 0;
  int unknown_count = 0;
  int num_sat = 0;
  int sat_dlevel = -1, max_lit = 0;
  bool already_sat = false;

  for (unsigned i = 0, sz = clause(cl).num_lits();
       unknown_count < 2 && i < sz; ++i) {
    int var_idx = lits[i] / 2;
    int value = variable(var_idx).value();
    if (value == UNKNOWN) {
      unit_lit = clause(cl).literal(i).s_var();
      ++unknown_count;
    } else {
      int dl = variable(var_idx).dlevel();
      if (dl >= max_level) {
        max_level2 = max_level;
        max_level = dl;
        max_lit = clause(cl).literal(i).s_var();
      }
      else if (dl > max_level2)
        max_level2 = dl;
      if (literal_value(clause(cl).literal(i)) == 1) {
        already_sat = true;
        ++num_sat;
        sat_dlevel = dl;
      }
    }
  }
  if (unknown_count == 0) {
    if (already_sat) {
      assert(sat_dlevel > -1);
      if (num_sat == 1 && sat_dlevel == max_level && max_level > max_level2) {
        back_track(max_level2 + 1);
        assert(max_lit > 1);
        queue_implication(max_lit, cl);
      }
    } else {
      assert(is_conflicting(cl));
      if (max_level > max_level2) {
        back_track(max_level2 + 1);
        assert(max_lit > 1);
        queue_implication(max_lit, cl);
      } else {
        back_track(max_level);
        if (max_level == 0 && preprocess() == CONFLICT)
          _stats.outcome = UNSATISFIABLE;
      }
    }
  }
  else if (unknown_count == 1) {
    if (!already_sat) {
      if (max_level < dlevel())
        back_track(max_level + 1);
      queue_implication(unit_lit, cl);
    }
  }
  return cl;
}