zchaff_solver.cpp

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

  if (deduce() == CONFLICT) {
    cout << " CONFLICT during preprocess " <<endl;
#ifdef VERIFY_ON
    for (unsigned i = 1; i < variables()->size(); ++i) {
      if (variable(i).value() != UNKNOWN) {
        assert(variable(i).dlevel() <= 0);
        int ante = variable(i).antecedent();
        int ante_id = 0;
        if (ante >= 0) {
          ante_id = clause(ante).id();
          verify_out << "VAR: " << i
                     << " L: " << variable(i).assgn_stack_pos()
                     << " V: " << variable(i).value()
                     << " A: " << ante_id
                     << " Lits:";
          for (unsigned j = 0; j < clause(ante).num_lits(); ++j)
            verify_out <<" " <<  clause(ante).literal(j).s_var();
          verify_out << endl;
         }
       }
    }
    verify_out << "CONF: " << clause(_conflicts[0]).id() << " ==";
    for (unsigned i = 0; i < clause(_conflicts[0]).num_lits(); ++i) {
      int svar = clause(_conflicts[0]).literal(i).s_var();
      verify_out << " " << svar;
    }
    verify_out << endl;
#endif
    return CONFLICT;
  }
  if (_params.verbosity > 1) {
    cout << _assignment_stack[0]->size() << " vars set during preprocess; "
         << endl;
  }
  return NO_CONFLICT;
}

void CSolver::mark_var_unbranchable(int vid) {
  if (variable(vid).is_branchable()) {
    variable(vid).disable_branch();
    if (variable(vid).value() == UNKNOWN)
      --num_free_variables();
  }
}

void CSolver::mark_var_branchable(int vid) {
  CVariable & var = variable(vid);
  if (!var.is_branchable()) {
    var.enable_branch();
    if (var.value() == UNKNOWN) {
      ++num_free_variables();
      if (var.var_score_pos() < _max_score_pos)
        _max_score_pos = var.var_score_pos();
    }
  }
}

ClauseIdx CSolver::add_orig_clause(int * lits, int n_lits, int gid) {
  int cid = add_clause_with_gid(lits, n_lits, gid);
  if (cid >= 0) {
    clause(cid).set_status(ORIGINAL_CL);
    clause(cid).activity() = 0;
  }
  return cid;
}

ClauseIdx CSolver::add_clause_with_gid(int * lits, int n_lits, int gid) {
  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));
  }
  ClauseIdx cid = add_clause(lits, n_lits, gflag);
  if (cid < 0) {
    _stats.is_mem_out = true;
    _stats.outcome = MEM_OUT;
  }
  return cid;
}

ClauseIdx CSolver::add_conflict_clause(int * lits, int n_lits, int gflag) {
  ClauseIdx cid = add_clause(lits, n_lits, gflag);
  if (cid >= 0) {
    clause(cid).set_status(CONFLICT_CL);
    clause(cid).activity() = 0;
  } else {
    _stats.is_mem_out = true;
    _stats.outcome = MEM_OUT;
  }
  return cid;
}

void CSolver::real_solve(void) {
  while (_stats.outcome == UNDETERMINED) {
    run_periodic_functions();
    if (decide_next_branch()) {
      while (deduce() == CONFLICT) {
        int blevel;
        blevel = analyze_conflicts();
        if (blevel < 0) {
          _stats.outcome = UNSATISFIABLE;
          return;
        }
      }
    } else {
      if (_sat_hook != NULL && _sat_hook(this))
        continue;
      _stats.outcome = SATISFIABLE;
      return;
    }
    if (time_out()) {
      _stats.outcome = TIME_OUT;
      return;
    }
    if (_force_terminate) {
      _stats.outcome = ABORTED;
      return;
    }
    if (_stats.is_mem_out) {
      _stats.outcome = MEM_OUT;
       return;
    }
  }
}

int CSolver::solve(void) {
  if (_stats.outcome == UNDETERMINED) {
    init_solve();

    if (preprocess() == CONFLICT)
      _stats.outcome = UNSATISFIABLE;
    else  // the real search
      real_solve();
    cout << endl;
    _stats.finish_cpu_time = get_cpu_time();
  }
  return _stats.outcome;
}

void CSolver::back_track(int blevel) {
  assert(blevel <= dlevel());
  for (int i = dlevel(); i >= blevel; --i) {
    vector<int> & assignments = *_assignment_stack[i];
    for (int j = assignments.size() - 1 ; j >= 0; --j)
      unset_var_value(assignments[j]>>1);
    assignments.clear();
  }
  dlevel() = blevel - 1;
  if (dlevel() < 0 )
    dlevel() = 0;
  ++_stats.num_backtracks;
}

int CSolver::deduce(void) {
  while (!_implication_queue.empty()) {
    const CImplication & imp = _implication_queue.front();
    int lit = imp.lit;
    int vid = lit>>1;
    ClauseIdx cl = imp.antecedent;
    _implication_queue.pop();
    CVariable & var = variable(vid);
    if (var.value() == UNKNOWN) {  // an implication
      set_var_value(vid, !(lit & 0x1), cl, dlevel());
    }
    else if (var.value() == (unsigned)(lit & 0x1)) {
      // a conflict
      // note: literal & 0x1 == 1 means the literal is in negative phase
      // when a conflict occure at not current dlevel, we need to backtrack
      // to resolve the problem.
      // conflict analysis will only work if the conflict occure at
      // the top level (current dlevel)
      _conflicts.push_back(cl);
      break;
    } else {
      // so the variable have been assigned before
      // update its antecedent with a shorter one
      if (var.antecedent() != NULL_CLAUSE &&
          clause(cl).num_lits() < clause(var.antecedent()).num_lits())
        var.antecedent() = cl;
      assert(var.dlevel() <= dlevel());
    }
  }
  // if loop exited because of a conflict, we need to clean implication queue
  while (!_implication_queue.empty())
    _implication_queue.pop();
  return (_conflicts.size() ? CONFLICT : NO_CONFLICT);
}

void CSolver::verify_integrity(void) {
  for (unsigned i = 1; i < variables()->size(); ++i) {
    if (variable(i).value() != UNKNOWN) {
      int pos = variable(i).assgn_stack_pos();
      int value = variable(i).value();
      int dlevel = variable(i).dlevel();
      assert((*_assignment_stack[dlevel])[pos] == (int) (i+i+1-value));
    }
  }
  for (unsigned i = 0; i < clauses()->size(); ++i) {
    if (clause(i).status() == DELETED_CL)
      continue;
    CClause & cl = clause(i);
    int num_0 = 0;
    int num_1 = 0;
    int num_unknown = 0;
    int watched[2];
    int watch_index = 0;
    watched[1] = watched[0] = 0;
    for (unsigned j = 0; j < cl.num_lits(); ++j) {
      CLitPoolElement lit = cl.literal(j);
      int vid = lit.var_index();
      if (variable(vid).value() == UNKNOWN) {
        ++num_unknown;
      } else {
        if (literal_value(lit) == 0)
          ++num_0;
        else
          ++num_1;
      }
      if (lit.is_watched()) {
        watched[watch_index] = lit.s_var();
        ++watch_index;
      }
    }
    if (watch_index == 0) {
      assert(cl.num_lits() == 1);
      continue;
    }
    assert(watch_index == 2);
    for (unsigned j = 0; j < cl.num_lits(); ++j) {
      CLitPoolElement lit = cl.literal(j);
      int vid1 = (watched[0]>>1);
      if (variable(vid1).value() == (unsigned)(watched[0] & 0x1)) {
        if (!lit.is_watched()) {
          assert(literal_value(lit) == 0);
          assert(variable(lit.var_index()).dlevel() <=
                  variable(vid1).dlevel());
        }
      }
      int vid2 = (watched[1]>>1);
      if (variable(vid2).value() == (unsigned)(watched[1] & 0x1)) {
        if (!lit.is_watched()) {
          assert(literal_value(lit) == 0);
          assert(variable(lit.var_index()).dlevel() <=
                  variable(vid1).dlevel());
        }
      }
    }
  }
}

void CSolver::mark_vars(ClauseIdx cl, int var_idx) {
  assert(_resolvents.empty() || var_idx != -1);
#ifdef VERIFY_ON
  _resolvents.push_back(clause(cl).id());
#endif
  for (CLitPoolElement* itr = clause(cl).literals(); (*itr).val() > 0; ++itr) {
    int v = (*itr).var_index();
    if (v == var_idx)
      continue;
    else if (variable(v).dlevel() == dlevel()) {
      if (!variable(v).is_marked()) {
        variable(v).set_marked();
        ++_num_marked;
        if (_mark_increase_score) {
          int tmp = itr->s_var();
          adjust_variable_order(&tmp, 1);
        }
      }
    } else {
      assert(variable(v).dlevel() < dlevel());
      if (variable(v).new_cl_phase() == UNKNOWN) {  // it's not in the new cl
        // We can remove the variable assigned at dlevel 0 if
        // we are nog going to use incremental SAT.
        // if(variable(v).dlevel()){
          ++_num_in_new_cl;
          variable(v).set_new_cl_phase((*itr).var_sign());
          _conflict_lits.push_back((*itr).s_var());
        // }
       } else {
         // if this variable is already in the new clause, it must
         // have the same phase
         assert(variable(v).new_cl_phase() == (*itr).var_sign());
       }
    }
  }
}

int CSolver::analyze_conflicts(void) {
  assert(!_conflicts.empty());
  assert(_conflict_lits.size() == 0);
  assert(_implication_queue.empty());
  assert(_num_marked == 0);
  if (dlevel() == 0) {  // already at level 0. Conflict means unsat.
#ifdef VERIFY_ON
    for (unsigned i = 1; i < variables()->size(); ++i) {
      if (variable(i).value() != UNKNOWN) {
        assert(variable(i).dlevel() <= 0);
        int ante = variable(i).antecedent();
        int ante_id = 0;
        if (ante >= 0) {
          ante_id = clause(ante).id();
          assert(clause(ante).status() != DELETED_CL);
          verify_out << "VAR: " << i
                     << " L: " << variable(i).assgn_stack_pos()
                     << " V: " << variable(i).value()
                     << " A: " << ante_id
                     << " Lits:";
          for (unsigned j = 0; j < clause(ante).num_lits(); ++j)
            verify_out << " " << clause(ante).literal(j).s_var();
          verify_out << endl;
        }
      }
    }
    ClauseIdx shortest;
    shortest = _conflicts.back();
    unsigned len = clause(_conflicts.back()).num_lits();
    while (!_conflicts.empty()) {
      if (clause(_conflicts.back()).num_lits() < len) {
        shortest = _conflicts.back();
        len = clause(_conflicts.back()).num_lits();
      }
      _conflicts.pop_back();
    }
    verify_out << "CONF: " << clause(shortest).id() << " ==";
    for (unsigned i = 0; i < clause(shortest).num_lits(); ++i) {
      int svar = clause(shortest).literal(i).s_var();
      verify_out << " " << svar;
    }
    verify_out << endl;
#endif
    _conflicts.clear();
    back_track(0);
    return -1;
  }
  return  conflict_analysis_firstUIP();
}

// when all the literals involved are in _conflict_lits
// call this function to finish the adding clause and backtrack

int CSolver::finish_add_conf_clause(int gflag) {
  ClauseIdx added_cl = add_conflict_clause(&(*_conflict_lits.begin()),
                                           _conflict_lits.size(), gflag);
  if (added_cl < 0) {  // memory out.
    _stats.is_mem_out = true;
    _conflicts.clear();
    assert(_implication_queue.empty());
    return 1;
  }

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

#ifdef VERIFY_ON
  verify_out << "CL: " <<  clause(added_cl).id() << " <=";
  for (unsigned i = 0; i< _resolvents.size(); ++i)
        verify_out << " " <<  _resolvents[i];
    verify_out << endl;
    _resolvents.clear();
#endif

  adjust_variable_order(&(*_conflict_lits.begin()), _conflict_lits.size());

  if (_params.shrinking.enable) {
    _shrinking_cls.clear();
    if (_stats.shrinking_cls_length != 0) {
      int benefit = _stats.shrinking_cls_length - _conflict_lits.size();
      _stats.shrinking_benefit += benefit;
      _stats.shrinking_cls_length = 0;
      _recent_shrinkings.push(benefit);
      if (_recent_shrinkings.size() > _params.shrinking.window_width) {
        _stats.shrinking_benefit -= _recent_shrinkings.front();
        _recent_shrinkings.pop();
      }
    }
    if (_conflict_lits.size() > _params.shrinking.size) {
      _shrinking_cls.clear();
      for (unsigned i = 0, sz = _conflict_lits.size(); i < sz; ++i) {