zverify_df.cpp

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

      } else {
        cerr << "Clause " << cl_id << " has more than one value 1 literals "
             << endl;
        exit(1);
      }
    } else {  // literal value 0, so seek its antecedent
      int ante = _variables[vid].antecedent;
      recursive_find_involved(ante);
    }
  }
}

void CDatabase::recursive_construct_clause(int cl_id) {
  CClause & cl = _clauses[cl_id];
  if (cl.is_built == true)
    return;

  assert(cl.resolvents.size() > 1);

  // I have to construct them first because of recursion may
  // mess up with the in_clause_signs.
  for (unsigned i = 0; i < cl.resolvents.size(); ++i) {
    _clauses[cl.resolvents[i]].is_needed = true;
    recursive_construct_clause(cl.resolvents[i]);
  }

//      cout << "Constructing clause " << cl_id << endl;
  vector<int> literals;

  // initialize
  int cl1 = cl.resolvents[0];
  assert(_clauses[cl1].is_built);
  for (unsigned i = 0; i < _clauses[cl1].literals.size(); ++i) {
    int lit = _clauses[cl1].literals[i];
    int vid = (lit >> 0x1);
    int sign = (lit & 0x1);
    assert(_variables[vid].in_clause_phase == UNKNOWN);
    _variables[vid].in_clause_phase = sign;
    literals.push_back(lit);
  }

  for (unsigned i = 1; i < cl.resolvents.size(); ++i) {
    int distance = 0;
    int cl1 = cl.resolvents[i];
    assert(_clauses[cl1].is_built);
    for (unsigned j = 0; j < _clauses[cl1].literals.size(); ++j) {
      int lit = _clauses[cl1].literals[j];
      int vid = (lit >> 0x1);
      int sign = (lit & 0x1);
      if (_variables[vid].in_clause_phase == UNKNOWN) {
        _variables[vid].in_clause_phase = sign;
        literals.push_back(lit);
      }
      else if (_variables[vid].in_clause_phase != sign) {
        // distance 1 literal
        ++distance;
        _variables[vid].in_clause_phase = UNKNOWN;
      }
    }
    if (distance != 1) {
      cerr << "Resolve between two clauses with distance larger than 1" << endl;
      cerr << "The resulting clause is " << cl_id << endl;
      cerr << "Starting clause is " << cl.resolvents[0] << endl;
      cerr << "One of the clause involved is " << cl1 << endl;
      exit(1);
    }
  }
  vector<int> temp_cls;
  for (unsigned i = 0; i < literals.size(); ++i) {
    int lit = literals[i];
    int vid = (lit >> 0x1);
    int sign = (lit & 0x1);
    if (_variables[vid].in_clause_phase == UNKNOWN)
      continue;
    assert(_variables[vid].in_clause_phase == sign);
    _variables[vid].in_clause_phase = UNKNOWN;
    temp_cls.push_back(lit);
  }
  cl.literals.resize(temp_cls.size());
  for (unsigned i = 0; i < temp_cls.size(); ++i)
    cl.literals[i] = temp_cls[i];

//      ::sort(cl.literals.begin(), cl.literals.end());
//      assert(cl.literals.size()== cl.my_literals.size());
//      for (unsigned i=0; i< cl.literals.size(); ++i)
//        assert(cl.literals[i] == cl.my_literals[i]);
  cl.is_built = true;
  ++_current_num_clauses;
  if (_current_num_clauses%10 == 0)
    check_mem_out();
}

int CDatabase::recursive_find_level(int vid) {
  int ante = _variables[vid].antecedent;
  assert(_variables[vid].value != UNKNOWN);
  assert(_variables[vid].antecedent != -1);
  assert(_clauses[ante].is_involved);
  if (_variables[vid].level != -1)
    return _variables[vid].level;
  int level = -1;
  for (unsigned i = 0; i <_clauses[ante].literals.size(); ++i) {
    int v = (_clauses[ante].literals[i] >> 1);
    int s = (_clauses[ante].literals[i] & 0x1);
    if (v == vid) {
      assert(_variables[v].value != s);
      continue;
    } else {
      assert(_variables[v].value == s);
      int l = recursive_find_level(v);
      if (level < l )
        level = l;
    }
  }
  _variables[vid].level = level + 1;
  return level + 1;
}

bool CDatabase::real_verify(void) {
  // 1. If a variable is assigned value at dlevel 0,
  // either it's pure or it has an antecedent
  for (unsigned i = 1; i < _variables.size(); ++i) {
    if (_variables[i].value != UNKNOWN && _variables[i].antecedent == -1) {
      if ((_variables[i].num_lits[0] == 0 && _variables[i].value == 0) ||
        (_variables[i].num_lits[1] == 0 && _variables[i].value == 1)) {
//      cout << "Variable " << i << " is assigned " << _variables[i].value
//      << " because it is pure literal. " << endl;
      } else {
        cerr << "Don't know why variable " << i << " is assigned "
             << _variables[i].value << " for no reasons" << endl;
        exit(1);
      }
    }
  }
  // 2. Construct the final conflicting clause if needed and find all
  // the clauses that are involved in making it conflicting
  cout << "Begin constructing all involved clauses " << endl;
  _clauses[_conf_id].is_needed = true;
  recursive_find_involved(_conf_id);
  int count = 0;
  for (unsigned i = num_init_clauses(); i< _clauses.size(); ++i)
    if (_clauses[i].is_built)
      ++count;
  cout << "Num. Learned Clause:\t\t\t" << _clauses.size() - num_init_clauses()
       << endl
       << "Num. Clause Built:\t\t\t" << count << endl
       << "Constructed all involved clauses " << endl;

  // 2.5. Verify the literals in the CONF clause
  // comments this out if it gives error because you give the wrong
  // CONF clause literals.
  assert(_clauses[_conf_id].is_built);
  assert(_clauses[_conf_id].is_involved);
  bool _found;
  for (unsigned i = 0; i <_conf_clause.size(); ++i) {
    _found = false;
    for (unsigned j = 0; j <_clauses[_conf_id].literals.size(); ++j) {
      if (_conf_clause[i] == _clauses[_conf_id].literals[j]) {
        _found = true;
        break;
      }
    }
    if (!_found) {
      cerr << "The conflict clause in trace can't be verified! " << endl;
      cerr << "Literal " << _conf_clause[i] << " is not found." << endl;
    }
  }
  cout << "Conflict clause verification finished." << endl;

  // 3. Levelize the variables that are decided at dlevel 0
  cout << "Levelize variables...";
  for (unsigned i = 1; i < _variables.size(); ++i) {
    int cl_id = _variables[i].antecedent;
    if (_variables[i].value != UNKNOWN &&  cl_id != -1) {
      if (_clauses[cl_id].is_involved) {
//        int level = recursive_find_level(i);
//        cout << "Var: " << i << " level " << level << endl;
      }
    }
  }
  cout << "finished"<< endl;
  // 4. Can we construct an empty clause?
  cout << "Begin Resolution..." ;
  set<CVariable *, cmp_var_level> clause_lits;
  for (unsigned i = 0; i< _clauses[_conf_id].literals.size(); ++i) {
    assert(lit_value(_clauses[_conf_id].literals[i]) == 0);
    int vid = (_clauses[_conf_id].literals[i] >> 1);
    clause_lits.insert(&_variables[vid]);
  }
  assert(clause_lits.size() == _clauses[_conf_id].literals.size());

  while (!clause_lits.empty()) {
//    for (set<CVariable *, cmp_var_level>::iterator itr = clause_lits.begin();
//         itr != clause_lits.end(); ++itr) {
//      int vid = (*itr) - &_variables[0];
//      cout << vid << "(" << (*itr)->level << ") ";
//    }
//    cout << endl;

    int vid = (*clause_lits.begin() - &_variables[0]);
    int ante = _variables[vid].antecedent;
    if (ante == -1) {
      cerr << "Variable " << vid << " has an NULL antecedent ";
      exit(1);
    }
    _clauses[ante].is_needed = true;
    clause_lits.erase(clause_lits.begin());
    _variables[vid].in_clause_phase = 1;
    CClause & cl = _clauses[ante];
    int distance = 0;
    for (unsigned i = 0; i< cl.literals.size(); ++i) {
      int l = cl.literals[i];
      int v = (l>>1);
      assert(_variables[v].value != UNKNOWN);
      if (lit_value(l) == 1) {
        if (vid != v) {
          cerr << "The antecedent of the variable is not really an antecedent "
               << endl;
          exit(1);
        }
        else
          ++distance;
      }
      else
        clause_lits.insert(&_variables[v]);
    }
    assert(distance == 1);
  }
  cout << " Empty clause generated." << endl;
  cout << "Mem Usage :\t\t\t\t" << get_mem_usage()<< endl;
  int needed_cls_count = 0;
  int needed_var_count = 0;
  for (int i = 0; i < num_init_clauses(); ++i) {
    if (_clauses[i].is_needed == true) {
      ++needed_cls_count;
      for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
        int vid = (_clauses[i].literals[j] >> 1);
        if (_variables[vid].is_needed == false) {
          ++needed_var_count;
          _variables[vid].is_needed = true;
        }
      }
    }
  }
  cout << "Original Num. Clauses:\t\t\t" << num_init_clauses() << endl;
  cout << "Needed Clauses to Construct Empty:\t"<< needed_cls_count << endl;
  cout << "Total Variable count:\t\t\t" << _variables.size()-1 << endl;
  cout << "Variables involved in Empty:\t\t" << needed_var_count << endl;

  for (unsigned i = 0; i< _clauses.size(); ++i) {
    if (_clauses[i].is_built)
      assert(_clauses[i].is_needed || i < (unsigned)num_init_clauses());
  }
  if (_dump_core == true) {
    cout << "Unsat Core dumped:\t\t\tunsat_core.cnf" << endl;
    ofstream dump("unsat_core.cnf");
    dump << "c Variables Not Involved: ";
    unsigned int k = 0;
    for (unsigned i = 1; i < _variables.size(); ++i) {
      if (_variables[i].is_needed == false) {
        if (k%20 == 0)
          dump << endl << "c ";
        ++k;
        dump << i << " ";
      }
    }
    dump << endl;
    dump << "p cnf " << _variables.size()-1 << " " << needed_cls_count << endl;
    for (int i = 0; i < num_init_clauses(); ++i) {
      if (_clauses[i].is_needed) {
        dump << "c Original Cls ID: " << i << endl;
        for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
          dump << ((_clauses[i].literals[j] & 0x1)?" -":" ")
               << (_clauses[i].literals[j] >> 1);
        }
        dump << " 0" << endl;
      }
    }
  }
  return true;
}

bool CDatabase::verify(char * filename) {
  vector<char> buffer;
  char token[WORD_LEN];

  ifstream in_file(filename);
  if (!in_file) {
    cerr << "Can't open input CNF file " << filename << endl;
    exit(1);
  }

  while (!in_file.eof()) {
    get_line(&in_file, &buffer);
    char * ptr = &(*buffer.begin());
    get_token(ptr, token);
    if (strcmp(token, "CL:") == 0) {
      vector<int> resolvents;

      get_token(ptr, token);
      int cl_id = my_a2i(token);

      get_token(ptr, token);
      assert(strcmp(token, "<=") == 0);

      while (get_token(ptr, token)) {
        int r = my_a2i(token);
        resolvents.push_back(r);
      }
      int c = add_learned_clause_by_resolvents(resolvents);
      assert(c == cl_id);
    }
    else if (strcmp(token, "VAR:") == 0) {
      get_token(ptr, token);
      int vid = my_a2i(token);

      get_token(ptr, token);
      assert(strcmp(token, "L:") == 0);
      get_token(ptr, token);  // skip the level

      get_token(ptr, token);
      assert(strcmp(token, "V:") == 0);
      get_token(ptr, token);
      int value = my_a2i(token);
      assert(value == 1 || value == 0);

      get_token(ptr, token);
      assert(strcmp(token, "A:") == 0);
      get_token(ptr, token);
      int ante = my_a2i(token);

      get_token(ptr, token);
      assert(strcmp(token, "Lits:") == 0);

      _variables[vid].value = value;
      _variables[vid].antecedent = ante;
    }
    else if (strcmp(token, "CONF:") == 0) {
      get_token(ptr, token);
      _conf_id = my_a2i(token);

      get_token(ptr, token);
      assert(strcmp(token, "==") == 0);

      while (get_token(ptr, token)) {
        int lit = my_a2i(token);
        assert(lit > 0);
        assert((lit>>1) < (int)_variables.size());
        _conf_clause.push_back(lit);
      }
    }
  }
  if (_conf_id == -1) {
    cerr << "No final conflicting clause defined " << endl;
    exit(1);
  }
  cout << "Mem Usage After Readin file:\t\t" << get_mem_usage() << endl;
  return real_verify();
}

int main(int argc, char** argv) {
  cout << "ZVerify SAT Solver Verifier" << endl;
  cout << "Copyright Princeton University, 2003-2004. All Right Reseverd."
       << endl;
  if (argc != 3 && argc !=4) {
    cerr << "Usage: " << argv[0] << " CNF_File Dump_File [-core]" << endl
       << "-core: dump the unsat core " << endl;
    cerr << endl;
    exit(1);
  }
  if (argc == 3) {
    _dump_core = false;
  } else {
    assert(argc == 4);
    if (strcmp(argv[3], "-core") != 0) {
      cerr << "Must use -core as the third parameter" << endl;
      exit(1);
    }
    _dump_core = true;
  }
  cout << "COMMAND LINE: ";
  for (int i = 0; i < argc; ++i)
    cout << argv[i] << " ";
  cout << endl;

  _peak_mem = get_mem_usage();
  CDatabase dbase;
  double begin_time = get_cpu_time();
  dbase.read_cnf(argv[1]);
  if (dbase.verify(argv[2]) == true) {
    double end_time = get_cpu_time();
    cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl;
    cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl;
    cout << "Verification Successful " << endl;
  } else {
    cout << "Failed to verify the result " << endl;
  }
  return 0;
}