zchaff_solver.cpp

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

          watched.pop_back();
          --itr1;
        }
      }
    }
  }
  free_gid(gid);
}

void CSolver::reset(void) {
  if (_stats.been_reset)
    return;
  if (num_variables() == 0)
    return;
  back_track(0);
  _conflicts.clear();
  while (!_implication_queue.empty())
    _implication_queue.pop();

  _stats.outcome = UNDETERMINED;
  _stats.been_reset = true;
}

void CSolver::delete_unrelevant_clauses(void) {
  unsigned original_del_cls = num_deleted_clauses();
  int num_conf_cls = num_clauses() - init_num_clauses() + num_del_orig_cls();
  int head_count = num_conf_cls / _params.cls_deletion.tail_vs_head;
  int count = 0;
  for (vector<CClause>::iterator itr = clauses()->begin();
                                 itr != clauses()->end() - 1; ++itr) {
    CClause & cl = *itr;
    if (cl.status() != CONFLICT_CL) {
      continue;
    }
    bool cls_sat_at_dl_0 = false;
    for (int i = 0, sz = cl.num_lits(); i < sz; ++i) {
      if (literal_value(cl.literal(i)) == 1 &&
          variable(cl.literal(i).var_index()).dlevel() == 0) {
        cls_sat_at_dl_0 = true;
        break;
      }
    }
    if (cls_sat_at_dl_0) {
      int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
      for (unsigned i = 0; i < cl.num_lits(); ++i) {
        int lit_value = literal_value(cl.literal(i));
        if (lit_value == 0)
          ++val_0_lits;
        if (lit_value == 1)
          ++val_1_lits;
        if (lit_value == UNKNOWN)
          ++unknown_lits;
        if (unknown_lits + val_1_lits > 1) {
          mark_clause_deleted(cl);
          break;
        }
      }
      continue;
    }

    count++;
    int max_activity = _params.cls_deletion.head_activity -
                       (_params.cls_deletion.head_activity -
                        _params.cls_deletion.tail_activity) *
                       count/num_conf_cls;
    int max_conf_cls_size;

    if (head_count > 0) {
      max_conf_cls_size = _params.cls_deletion.head_num_lits;
      --head_count;
    } else {
      max_conf_cls_size = _params.cls_deletion.tail_num_lits;
    }

    if (cl.activity() > max_activity)
      continue;

    int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0, lit_value;
    for (unsigned i = 0; i < cl.num_lits(); ++i) {
      lit_value = literal_value(cl.literal(i));
      if (lit_value == 0)
        ++val_0_lits;
      else if (lit_value == 1)
        ++val_1_lits;
      else
        ++unknown_lits;
      if ((unknown_lits > max_conf_cls_size)) {
        mark_clause_deleted(cl);
        break;
      }
    }
  }

  // if none were recently marked for deletion...
  if (original_del_cls == num_deleted_clauses())
    return;

  // 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();
          watched.pop_back();
          --itr1;
        }
      }
    }
  }

  for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
    if (variable(i).dlevel() != 0) {
      variable(i).score(0) = variable(i).lits_count(0);
      variable(i).score(1) = variable(i).lits_count(1);
      if (variable(i).lits_count(0) == 0 && variable(i).value() == UNKNOWN) {
        queue_implication(i * 2 + 1, NULL_CLAUSE);
      }
      else if (variable(i).lits_count(1) == 0 &&
               variable(i).value() == UNKNOWN) {
        queue_implication(i * 2, NULL_CLAUSE);
      }
    } else {
      variable(i).score(0) = 0;
      variable(i).score(1) = 0;
    }
  }
  update_var_score();
}

bool CSolver::time_out(void) {
  return (get_cpu_time() - _stats.start_cpu_time> _params.time_limit);
}

void CSolver::adjust_variable_order(int * lits, int n_lits) {
  // note lits are signed vars, not CLitPoolElements
  for (int i = 0; i < n_lits; ++i) {
    int var_idx = lits[i] >> 1;
    CVariable & var = variable(var_idx);
    assert(var.value() != UNKNOWN);
    int orig_score = var.score();
    ++variable(var_idx).score(lits[i] & 0x1);
    int new_score = var.score();
    if (orig_score == new_score)
      continue;
    int pos = var.var_score_pos();
    int orig_pos = pos;
    assert(_ordered_vars[pos].first == & var);
    assert(_ordered_vars[pos].second == orig_score);
    int bubble_step = _params.decision.bubble_init_step;
    for (pos = orig_pos ; pos >= 0; pos -= bubble_step) {
      if (_ordered_vars[pos].second >= new_score)
        break;
    }
    pos += bubble_step;
    for (bubble_step = bubble_step >> 1; bubble_step > 0;
         bubble_step = bubble_step >> 1) {
      if (pos - bubble_step >= 0 &&
          _ordered_vars[pos - bubble_step].second < new_score)
        pos -= bubble_step;
    }
    // now found the position, do a swap
    _ordered_vars[orig_pos] = _ordered_vars[pos];
    _ordered_vars[orig_pos].first->set_var_score_pos(orig_pos);
    _ordered_vars[pos].first = & var;
    _ordered_vars[pos].second = new_score;
    _ordered_vars[pos].first->set_var_score_pos(pos);
    _stats.total_bubble_move += orig_pos - pos;
  }
}

void CSolver::decay_variable_score(void) {
  unsigned i, sz;
  for (i = 1, sz = variables()->size(); i < sz; ++i) {
    CVariable & var = variable(i);
    var.score(0) /= 2;
    var.score(1) /= 2;
  }
  for (i = 0, sz = _ordered_vars.size(); i < sz; ++i) {
    _ordered_vars[i].second = _ordered_vars[i].first->score();
  }
}

bool CSolver::decide_next_branch(void) {
  if (dlevel() > 0)
    assert(_assignment_stack[dlevel()]->size() > 0);
  if (!_implication_queue.empty()) {
    // some hook function did a decision, so skip my own decision making.
    // if the front of implication queue is 0, that means it's finished
    // because var index start from 1, so 2 *vid + sign won't be 0.
    // else it's a valid decision.
    return (_implication_queue.front().lit != 0);
  }
  int s_var = 0;
  if (_params.shrinking.enable) {
    while (!_shrinking_cls.empty()) {
      s_var = _shrinking_cls.begin()->second;
      _shrinking_cls.erase(_shrinking_cls.begin());
      if (variable(s_var >> 1).value() == UNKNOWN) {
        _stats.num_decisions++;
        _stats.num_decisions_shrinking++;
        ++dlevel();
        queue_implication(s_var ^ 0x1, NULL_CLAUSE);
        return true;
      }
    }
  }

  if (_outside_constraint_hook != NULL)
     _outside_constraint_hook(this);

  if (!_implication_queue.empty())
     return (_implication_queue.front().lit != 0);

  ++_stats.num_decisions;
  if (num_free_variables() == 0)  // no more free vars
     return false;

  bool cls_sat = true;
  int i, sz, var_idx, score, max_score = -1;

  for (; top_unsat_cls->status() != ORIGINAL_CL; --top_unsat_cls) {
    CClause &cl=*top_unsat_cls;
    if (cl.status() != CONFLICT_CL)
      continue;
    cls_sat = false;
    if (cl.sat_lit_idx() < (int)cl.num_lits() &&
        literal_value(cl.literal(cl.sat_lit_idx())) == 1)
      cls_sat = true;
    if (!cls_sat) {
      max_score = -1;
      for (i = 0, sz = cl.num_lits(); i < sz; ++i) {
        var_idx = cl.literal(i).var_index();
        if (literal_value(cl.literal(i)) == 1) {
          cls_sat = true;
          cl.sat_lit_idx() = i;
          break;
        }
        else if (variable(var_idx).value() == UNKNOWN) {
          score = variable(var_idx).score();
          if (score > max_score) {
            max_score = score;
            s_var = var_idx * 2;
          }
        }
      }
    }
    if (!cls_sat)
      break;
  }
  if (!cls_sat && max_score != -1) {
    ++dlevel();
    if (dlevel() > _stats.max_dlevel)
      _stats.max_dlevel = dlevel();
    CVariable& v = variable(s_var >> 1);
    if (v.score(0) < v.score(1))
      s_var += 1;
    else if (v.score(0) == v.score(1)) {
      if (v.two_lits_count(0) > v.two_lits_count(1))
        s_var+=1;
      else if (v.two_lits_count(0) == v.two_lits_count(1))
        s_var+=rand()%2;
    }
    assert(s_var >= 2);
    queue_implication(s_var, NULL_CLAUSE);
    ++_stats.num_decisions_stack_conf;
    return true;
  }

  for (unsigned i = _max_score_pos; i < _ordered_vars.size(); ++i) {
    CVariable & var = *_ordered_vars[i].first;
    if (var.value() == UNKNOWN && var.is_branchable()) {
      // move th max score position pointer
      _max_score_pos = i;
      // make some randomness happen
      if (--_stats.current_randomness < _params.decision.base_randomness)
        _stats.current_randomness = _params.decision.base_randomness;
      int randomness = _stats.current_randomness;
      if (randomness >= num_free_variables())
        randomness = num_free_variables() - 1;
      int skip = rand() % (1 + randomness);
      int index = i;
      while (skip > 0) {
        ++index;
      if (_ordered_vars[index].first->value() == UNKNOWN &&
          _ordered_vars[index].first->is_branchable())
        --skip;
      }
      CVariable * ptr = _ordered_vars[index].first;
      assert(ptr->value() == UNKNOWN && ptr->is_branchable());
      int sign = 0;
      if (ptr->score(0) < ptr->score(1))
        sign += 1;
      else if (ptr->score(0) == ptr->score(1)) {
        if (ptr->two_lits_count(0) > ptr->two_lits_count(1))
          sign += 1;
        else if (ptr->two_lits_count(0) == ptr->two_lits_count(1))
          sign += rand() % 2;
      }
      int var_idx = ptr - &(*variables()->begin());
      s_var = var_idx + var_idx + sign;
      break;
    }
  }
  assert(s_var >= 2);  // there must be a free var somewhere
  ++dlevel();
  if (dlevel() > _stats.max_dlevel)
    _stats.max_dlevel = dlevel();
  ++_stats.num_decisions_vsids;
  _implication_id = 0;
  queue_implication(s_var, NULL_CLAUSE);
  return true;
}

int CSolver::preprocess(void) {
  assert(dlevel() == 0);

  // 1. detect all the unused variables
  vector<int> un_used;
  for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
    CVariable & v = variable(i);
    if (v.lits_count(0) == 0 && v.lits_count(1) == 0) {
      un_used.push_back(i);
      queue_implication(i+i, NULL_CLAUSE);
      int r = deduce();
      assert(r == NO_CONFLICT);
    }
  }
  if (_params.verbosity > 1 && un_used.size() > 0) {
    cout << un_used.size() << " Variables are defined but not used " << endl;
    if (_params.verbosity > 2) {
      for (unsigned i = 0; i< un_used.size(); ++i)
         cout << un_used[i] << " ";
      cout << endl;
    }
  }

  // 2. detect all variables with only one phase occuring (i.e. pure literals)
  vector<int> uni_phased;
  for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) {
    CVariable & v = variable(i);
    if (v.value() != UNKNOWN)
      continue;
    if (v.lits_count(0) == 0) {  // no positive phased lits.
      queue_implication(i+i+1, NULL_CLAUSE);
      uni_phased.push_back(-i);
    }
    else if (v.lits_count(1) == 0) {  // no negative phased lits.
      queue_implication(i+i, NULL_CLAUSE);
      uni_phased.push_back(i);
    }
  }
  if (_params.verbosity > 1 && uni_phased.size() > 0) {
    cout << uni_phased.size() << " Variables only appear in one phase." <<endl;
    if (_params.verbosity > 2) {
      for (unsigned i = 0; i< uni_phased.size(); ++i)
        cout << uni_phased[i] << " ";
      cout <<endl;
    }
  }

  // 3. Unit clauses
  for (unsigned i = 0, sz = clauses()->size(); i < sz; ++i) {
    if (clause(i).status() != DELETED_CL &&
        clause(i).num_lits() == 1 &&
        variable(clause(i).literal(0).var_index()).value() == UNKNOWN)
      queue_implication(clause(i).literal(0).s_var(), i);
  }