zminimal.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 <iostream>
#include <fstream>
#include <cstdlib>
#include <cstdio>
#include <set>
#include <vector>

using namespace std;

#include "SAT.h"

const int MAX_LINE_LENGTH       = 65536;
const int MAX_WORD_LENGTH       = 64;

void read_cnf_omit(SAT_Manager mng, char * filename, vector<int> & omit) {
  char line_buffer[MAX_LINE_LENGTH];
  char word_buffer[MAX_WORD_LENGTH];
  set<int> clause_vars;
  set<int> clause_lits;
  unsigned omit_idx = 0;
  int line_num = 0;
  ifstream inp(filename, ios::in);
  if (!inp) {
    cerr << "Can't open input file" << endl;
    exit(1);
  }
  int cl_id = -1;
  while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
    ++line_num;
    if (line_buffer[0] == 'c') {
      continue;
    }
    else if (line_buffer[0] == 'p') {
      int var_num;
      int cl_num;
      int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
      if (arg < 2) {
        cerr << "Unable to read number of variables and clauses"
             << "at line " << line_num << endl;
        exit(3);
      }
      SAT_SetNumVariables(mng, var_num);  // first element not used.
    } else {                             // Clause definition or continuation
      char *lp = line_buffer;
      do {
        char *wp = word_buffer;
        while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
          lp++;
        }
        while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
          *(wp++) = *(lp++);
        }
        *wp = '\0';                                 // terminate string

        if (strlen(word_buffer) != 0) {     // check if number is there
          int var_idx = atoi(word_buffer);
          int sign = 0;

          if (var_idx != 0) {
            if (var_idx < 0) {
              var_idx = -var_idx;
              sign = 1;
            }
            clause_vars.insert(var_idx);
            clause_lits.insert((var_idx << 1) + sign);
          } else {
            // add this clause
            ++cl_id;
            if (omit_idx < omit.size()-1 && omit[omit_idx] < cl_id )
              ++omit_idx;
            if (omit_idx < omit.size()) {
              if (omit[omit_idx] == cl_id) {
                clause_lits.clear();
                clause_vars.clear();
              }
            }
            if (clause_vars.size() != 0 &&
                clause_vars.size() == clause_lits.size()) {
              vector <int> temp;
              for (set<int>::iterator itr = clause_lits.begin();
                   itr != clause_lits.end(); ++itr) {
                temp.push_back(*itr);
              }
              SAT_AddClause(mng, & temp.begin()[0], temp.size() );
            }
            clause_lits.clear();
            clause_vars.clear();
          }
        }
      }
      while (*lp);
    }
  }
  if (!inp.eof()) {
    cerr << "Input line " << line_num << " too long. Unable to continue..."
         << endl;
    exit(2);
  }

  if (clause_lits.size() && clause_vars.size() == clause_lits.size()) {
    vector <int> temp;
    for (set<int>::iterator itr = clause_lits.begin();
         itr != clause_lits.end(); ++itr) {
      temp.push_back(*itr);
    }
    SAT_AddClause(mng, & temp.begin()[0], temp.size() );
  }
  clause_lits.clear();
  clause_vars.clear();
}

int get_num_clause(char * filename) {
  char line_buffer[MAX_LINE_LENGTH];
  ifstream inp(filename, ios::in);
  if (!inp) {
    cerr << "Can't open input file" << endl;
    exit(1);
  }
  while (inp.getline(line_buffer, MAX_LINE_LENGTH)) {
    if (inp.fail()) {
      cerr << "Too large an input line. Unable to continue..." << endl;
      exit(2);
    }
    if (line_buffer[0] == 'p') {
      int var_num;
      int cl_num;
      int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num);
      if (arg < 2) {
        cerr << "Unable to read number of variables and clauses" << endl;
        exit(3);
      }
      return cl_num;
    }
  }
  cerr << "Can't find the header in CNF:  p cnf NumVar NumCls " << endl;
  exit(1);
  return 0;
}

void handle_result(SAT_Manager mng, int outcome, char * filename) {
  char * result = "UNKNOWN";
  switch (outcome) {
    case SATISFIABLE:
      cout << "Instance satisfiable" << endl;
      // following lines will print out a solution if a solution exist
      for (unsigned i = 1, sz = SAT_NumVariables(mng); i <= sz; ++i) {
        switch (SAT_GetVarAsgnment(mng, i)) {
          case -1:
            cout << "(" << i<< ")";
            break;
          case 0:
            cout << "-" << i;
            break;
          case 1:
            cout << i;
            break;
          default:
            cerr << "Unknown variable value state"<< endl;
            exit(4);
        }
        cout << " ";
      }
      result  = "SAT";
      cout << endl;
      break;
    case UNSATISFIABLE:
      result  = "UNSAT";
      cout << "Instance unsatisfiable" << endl;
      break;
    case TIME_OUT:
      result  = "ABORT : TIME OUT";
      cout << "Time out, unable to determine the outcome of the instance";
      cout << endl;
      break;
    case MEM_OUT:
      result  = "ABORT : MEM OUT";
      cout << "Memory out, unable to determine the outcome of the instance";
      cout << endl;
      break;
    default:
      cerr << "Unknown outcome" << endl;
      exit(5);
  }
  cout << "Max Decision Level\t\t\t" << SAT_MaxDLevel(mng) << endl;
  cout << "Num. of Decisions\t\t\t" << SAT_NumDecisions(mng) << endl;
  cout << "Num. of Variables\t\t\t" << SAT_NumVariables(mng) << endl;
  cout << "Original Num Clauses\t\t\t" << SAT_InitNumClauses(mng) << endl;
  cout << "Original Num Literals\t\t\t" << SAT_InitNumLiterals(mng) << endl;
  cout << "Added Conflict Clauses\t\t\t" << SAT_NumAddedClauses(mng) -
                                            SAT_InitNumClauses(mng)<< endl;
  cout << "Added Conflict Literals\t\t\t" << SAT_NumAddedLiterals(mng) -
                                             SAT_InitNumLiterals(mng) << endl;
  cout << "Deleted Unrelevant clause\t\t" << SAT_NumDeletedClauses(mng) <<endl;
  cout << "Deleted Unrelevant literals\t\t" <<SAT_NumDeletedLiterals(mng) <<endl;
  cout << "Number of Implication\t\t\t" << SAT_NumImplications(mng)<< endl;

  // other statistics comes here
  cout << "Total Run Time\t\t\t\t" << SAT_GetCPUTime(mng) << endl << endl;
  cout  << result << endl;
}

void output_status(SAT_Manager mng) {
  cout << "Dec: " << SAT_NumDecisions(mng) << "\t ";
  cout << "AddCl: " << SAT_NumAddedClauses(mng) << "\t";
  cout << "AddLit: " << SAT_NumAddedLiterals(mng) << "\t";
  cout << "DelCl: " << SAT_NumDeletedClauses(mng) << "\t";
  cout << "DelLit: " << SAT_NumDeletedLiterals(mng) << "\t";
  cout << "NumImp: " << SAT_NumImplications(mng) << "\t";
  cout << "AveBubbleMove: " << SAT_AverageBubbleMove(mng) << "\t";
  // other statistics comes here
  cout << "RunTime:" << SAT_GetElapsedCPUTime(mng) << endl;
}

void verify_solution(SAT_Manager mng) {
  int num_verified = 0;
  for (int cl_idx = SAT_GetFirstClause (mng); cl_idx >= 0;
       cl_idx = SAT_GetNextClause(mng, cl_idx)) {
    int len = SAT_GetClauseNumLits(mng, cl_idx);
    int * lits = new int[len+1];
    SAT_GetClauseLits(mng, cl_idx, lits);
    int i;
    for (i = 0; i < len; ++i) {
      int v_idx = lits[i] >> 1;
      int sign = lits[i] & 0x1;
      int var_value = SAT_GetVarAsgnment(mng, v_idx);
      if ((var_value == 1 && sign == 0) ||
          (var_value == 0 && sign == 1))
        break;
    }
    if (i >= len) {
      cerr << "Verify Satisfiable solution failed, please "
           << "file a bug report, thanks. " << endl;
      exit(6);
    }
    delete [] lits;
      ++num_verified;
  }
  cout << num_verified << " Clauses are true, Verify Solution successful. ";
}

int main(int argc, char ** argv) {
  if (argc != 2) {
    cerr << "ZMinimal: Find Minimal Core. " << endl;
    cerr << "Copyright 2003-2004, Princeton University" << endl << endl;
    cerr << "Usage: "<< argv[0] << " cnf_file " << endl;
    return 2;
  }
  vector<int> omit;
  int num_cls = get_num_clause(argv[1]);
  cout << "Total : " << num_cls << " passes";
  for (int i = 0; i < num_cls; ++i) {
    if (i % 50 == 0)
      cout << endl << i << ":\t";
    if (i % 10 == 0)
      cout << " ";
    cout.flush();
    SAT_Manager mng = SAT_InitManager();
    omit.push_back(i);
    read_cnf_omit(mng, argv[1], omit);
    int result = SAT_Solve(mng);
    if (result != SATISFIABLE) {
      cout << "*" ;
    } else {
      cout << "-";
      omit.pop_back();
    }
    cout.flush();
    SAT_ReleaseManager(mng);
  }
  cout << endl;
  cout << "Instance Cls: " << num_cls << "  MinCore Cls: "
       << num_cls - omit.size() << " Diff: " << omit.size() << endl;
  cout << "Unneeded clauses are: ";
  for (unsigned i = 0; i < omit.size(); ++i) {
    if (i % 20 == 0)
      cout << endl;
    cout << omit[i] << " ";
  }
  cout << endl;
  return 0;
}