zverify_df.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 <sys/time.h>
#include <sys/resource.h>
#include <vector>
#include <set>
#include <iostream>
#include <fstream>
#include <assert.h>

using namespace std;

const int WORD_LEN      = 64000;

const int MEM_LIMIT     = 800000;

const int UNKNOWN       = 2;

int _peak_mem;
bool _dump_core;

double get_cpu_time(void) {
  double res;
  struct rusage usage;
  getrusage(RUSAGE_SELF, &usage);
  res = usage.ru_utime.tv_usec + usage.ru_stime.tv_usec;
  res *= 1e-6;
  res += usage.ru_utime.tv_sec + usage.ru_stime.tv_sec;
  return res;
}

void get_line(ifstream* fs, vector<char>* buf) {
  buf->clear();
  buf->reserve(4096);
  while (!fs->eof()) {
    char ch = fs->get();
    if (ch == '\n' || ch == '\377')
      break;
    if (ch == '\r')
      continue;
    buf->push_back(ch);
  }
  buf->push_back('\0');
  return;
}

int get_token(char * & lp, char * token) {
  char * wp = token;
  while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
    lp++;
  }
  while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
    *(wp++) = *(lp++);
  }
  *wp = '\0';                                 // terminate string
  return wp - token;
}

int get_mem_usage(void) {
  FILE * fp;
  char buffer[128];
  char token[128];
  char filename[128];

  int pid = getpid();
  snprintf(filename, sizeof(filename), "/proc/%i/status", pid);
  if ((fp = fopen(filename, "r")) == NULL) {
    cerr << "Can't open Proc file, are you sure you are using Linux?" << endl;
    exit(1);
  }
  while (!feof(fp)) {
    fgets(buffer, 128, fp);
    char * ptr = buffer;
    get_token(ptr, token);
    if (strcmp(token, "VmSize:") == 0) {
      get_token(ptr, token);
      fclose(fp);
      return atoi(token);
    }
  }
  cerr << "Error in get memeory usage" << endl;
  exit(1);
  return 0;
}

int my_a2i(char * str) {
  int result = 0;
  bool neg = false;
  if (str[0] == '-') {
    neg = true;
    ++str;
  }
  else if (str[0] == '+')
    ++str;
  for (unsigned i = 0; i < strlen(str); ++i) {
    int d = str[i] - '0';
    if (d < 0 || d > 9) {
      cerr << "Abort: Unable to change " << str << " into a number " << endl;
      exit(1);
    }
    result = result * 10 + d;
  }
  if (neg)
    result = -result;
  return result;
}

class CClause {
  public:
    vector<int> literals;
    vector<int> resolvents;
    bool is_involved    : 1;
    bool is_built       : 1;
    bool is_needed      : 1;

    CClause(void) {
      is_involved = false;
      is_built = false;
      is_needed = false;
    }
    ~CClause(void) {}
};

class CVariable {
  public:
    short       value;
    short       in_clause_phase         :4;
    bool        is_needed               :1;
    int         antecedent;
    int         num_lits[2];
    int         level;
    CVariable(void) {
      value = UNKNOWN;
      antecedent = -1;
      in_clause_phase = UNKNOWN;
      num_lits[0] = num_lits[1] = 0;
      level = -1;
      is_needed = false;
    }
};

struct cmp_var_level {
  bool operator() (CVariable * v1, CVariable * v2) {
    if (v1->level > v2->level)
      return true;
    else if (v1->level < v2->level)
      return false;
    else if ( (int)v1 > (int)v2)
      return true;
    return false;
  }
};

class CDatabase {
  private:
    int                 _current_num_clauses;
    int                 _num_init_clauses;
    vector<CVariable>   _variables;
    vector<CClause>     _clauses;
    int                 _conf_id;
    vector<int>         _conf_clause;

  public:
    CDatabase(void) {
      _num_init_clauses = 0;
      _current_num_clauses = 0;
      _conf_id = -1;
    }

    int & num_init_clauses(void) {
      return _num_init_clauses;
    }

    vector<CVariable> & variables(void) {
      return _variables;
    }

    vector<CClause> & clauses(void) {
      return  _clauses;
    }

    void read_cnf(char * filename);
    bool verify(char * filename);
    bool real_verify(void);
    int lit_value(int svar) {
      assert(_variables[svar>>1].value != UNKNOWN);
      return _variables[svar>>1].value ^ (svar & 0x1);
    }
    int add_orig_clause_by_lits(vector<int> lits);
    int add_learned_clause_by_resolvents(vector<int> & resolvents);
    void set_var_number(int nvar);
    void set_init_cls_number(int n) {
      _num_init_clauses = n;
    }
    void construct_learned_clauses(void);
    void recursive_construct_clause(int cl_id);
    void recursive_find_involved(int cl_id);
    int recursive_find_level(int vid);
    void dump(void);
};

void CDatabase::dump(void) {
  cout << "p cnf " << _variables.size() - 1 << " " << _num_init_clauses << endl;
  for (unsigned i = 0; i < _clauses.size(); ++i) {
    for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
      int lit = _clauses[i].literals[j];
      cout << ((lit & 0x1) ? "-" : "") << (lit >> 1) << " ";
    }
    cout << "0" << endl;
  }
}

void CDatabase::set_var_number(int nvar) {
  _variables.resize(nvar + 1);
  for (unsigned i = 0; i < _variables.size(); ++i) {
    _variables[i].value = UNKNOWN;
    _variables[i].in_clause_phase = UNKNOWN;
  }
}

void check_mem_out(void) {
  int mem = get_mem_usage();
  if (mem > MEM_LIMIT) {
    cerr << "Mem out" << endl;
    exit(1);
  }
  if (mem > _peak_mem)
    _peak_mem = mem;
}

int CDatabase::add_orig_clause_by_lits(vector<int> lits) {
  static int line_n = 0;
  ++line_n;
  if (lits.size() == 0) {
    cerr << "Empty Clause Encountered " << endl;
    exit(1);
  }
  int cls_id = _clauses.size();
  _clauses.resize(_clauses.size() + 1);
  vector<int> temp_cls;
  for (unsigned i = 0; i < lits.size(); ++i) {
    int vid = lits[i];
    int phase = 0;
    if (vid < 0) {
      vid = - vid;
      phase = 1;
    }
    if (vid == 0 || vid > (int) _variables.size() - 1) {
      cerr << "Variable index out of range " << endl;
      exit(1);
    }
    if (_variables[vid].in_clause_phase == UNKNOWN) {
      _variables[vid].in_clause_phase = phase;
      temp_cls.push_back(vid + vid + phase);
//    _clauses[cls_id].my_literals.push_back(vid + vid + phase);
      ++_variables[vid].num_lits[phase];
    }
    else if (_variables[vid].in_clause_phase != phase) {
      cerr << "clause " << line_n << endl;
      cerr << "A clause contain both literal and its negate " << endl;
      exit(1);
    }
  }
  _clauses[cls_id].literals.resize(temp_cls.size());
  for (unsigned i = 0; i< temp_cls.size(); ++i) {
    _clauses[cls_id].literals[i]= temp_cls[i];
  }
  _clauses[cls_id].is_built = true;
//      _clauses[cls_id].my_is_built = true;
  for (unsigned i = 0; i< lits.size(); ++i) {
    int vid = lits[i];
    if (vid < 0) vid = -vid;
    _variables[vid].in_clause_phase = UNKNOWN;
  }
  ++_current_num_clauses;
  if (_current_num_clauses%10 == 0)
    check_mem_out();
  return cls_id;
}

int CDatabase::add_learned_clause_by_resolvents(vector<int> & resolvents) {
  int cls_id = _clauses.size();
  _clauses.resize(_clauses.size() + 1);
  _clauses[cls_id].resolvents.resize(resolvents.size());
  for (unsigned i = 0; i< resolvents.size(); ++i)
    _clauses[cls_id].resolvents[i] = resolvents[i];
  _clauses[cls_id].is_built = false;
  return cls_id;
}

void CDatabase::read_cnf(char * filename) {
  cout << "Read in original clauses ... ";
  ifstream in_file(filename);
  if (!in_file) {
    cerr << "Can't open input CNF file " << filename << endl;
    exit(1);
  }
  vector<char> buffer;
  vector<int> literals;
  bool header_encountered = false;
  char token[WORD_LEN];
  while (!in_file.eof()) {
    get_line(&in_file, &buffer);
    char * ptr = &(*buffer.begin());
    if (get_token(ptr, token)) {
      if (strcmp(token, "c") == 0)
        continue;
      else if (strcmp(token, "p") == 0) {
        get_token(ptr, token);
        if (strcmp(token, "cnf") != 0) {
          cerr << "Format Error, p cnf NumVar NumCls " << endl;
          exit(1);
        }
        get_token(ptr, token);
        int nvar = my_a2i(token);
        set_var_number(nvar);
        get_token(ptr, token);
        int ncls = my_a2i(token);
        set_init_cls_number(ncls);
        header_encountered = true;
        continue;
      } else {
        int lit = my_a2i(token);
        if (lit != 0) {
          literals.push_back(lit);
        } else {
          add_orig_clause_by_lits(literals);
          literals.clear();
        }
      }
    }
    while (get_token(ptr, token)) {
      int lit = my_a2i(token);
      if (lit != 0) {
        literals.push_back(lit);
      } else {
        add_orig_clause_by_lits(literals);
        literals.clear();
      }
    }
  }
  if (!literals.empty()) {
    cerr << "Trailing numbers without termination " << endl;
    exit(1);
  }
  if (clauses().size() != (unsigned)num_init_clauses())
    cerr << "WARNING : Clause count inconsistant with the header " << endl;
  cout << num_init_clauses() << " Clauses " << endl;
}

void CDatabase::recursive_find_involved(int cl_id) {
  if (_clauses[cl_id].is_involved == true)
    return;
  _clauses[cl_id].is_involved = true;

  recursive_construct_clause(cl_id);

  int num_1 = 0;
  for (unsigned i = 0; i < _clauses[cl_id].literals.size(); ++i) {
    int lit = _clauses[cl_id].literals[i];
    int vid = (lit>>1);
    int sign = (lit & 0x1);
    assert(_variables[vid].value != UNKNOWN);
    if ((_variables[vid].value == 1 && sign == 0) ||
      (_variables[vid].value == 0 && sign == 1)) {
      if (num_1 == 0) {
        ++num_1;