zminimal.cpp

这是一种很好的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>

#include "SAT.h"

using namespace std;

#define MAX_LINE_LENGTH    65536
#define 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())) { //yeah, can add this clause
			    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);
    }
//    assert (clause_vars.size() == 0); 	//some benchmark has no 0 in the last clause
    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 satisfiablility of the instance";
	cout << endl;
	break;
    case MEM_OUT:
	result  = "ABORT : MEM OUT"; 
	cout << "Memory out, unable to determine the satisfiablility 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:\t" << filename << " " << result << " RunTime: " << SAT_GetCPUTime(mng)<< 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 Univ." << 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;
}