main.cpp

多核环境下运行了可满足性分析的工具软件

/********************************************************************************************
MiraXT -- Copyright (c) 2007, Tobias Schubert, Matthew Lewis, Natalia Kalinnik, Bernd Becker 

Permission is hereby granted, free of charge, to any person obtaining a copy of this 
software and associated documentation files (the "Software"), to deal in the Software 
without restriction, including without limitation the rights to use, copy, modify, merge, 
publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons 
to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING 
BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
********************************************************************************************/

// Include header files.
#include <fstream>                
#include <sys/time.h>      
#include <pthread.h>
#include <zlib.h>
#include <iostream>
#include "../Simp/SimpSolver.h"

// Global variables.
int   numThreads;                   // Number of threads.
int   numLiterals;                  // Number of variables.
int   numClausesOrig;               // Original number of clauses.
int   numClauses;                   // Number of clauses after performing MiniSat2's preprocessing.
char* CNFFile;                      // Name of the benchmark instance to be solved.

namespace mira 
{
#include "defines.h"
#include "gettime.cpp"
#include "vector.hpp"
#include "clausedb.cpp"
#include "controlstructure.cpp"
#include "decisionqueue.cpp"
#include "vsids.cpp"
#include "thread.cpp"
#include "thread_startup.cpp"
#include "thread_decisionstack.cpp"
#include "thread_decide.cpp"
#include "thread_cleanclausedb.cpp"
#include "thread_bcp.cpp"
#include "thread_ca.cpp"
#include "thread_activity.cpp"
#include "thread_addclauses.cpp"
#include "thread_preprocessing.cpp"
#include "verify.cpp"
#include "statistics.cpp"
}

// Include MiniSat2's CNF loader.
#include "gzloader.cpp"

// The main MiraXTmini routine.
int main(int argc, char** argv)
{
  // Variables.
  long long startTime, endTime;
  int ExitCode = 0; 

  // Wrong number of arguments?
  if (argc < 3) 
    { 
      // Error message.
      fprintf(stdout,"c MiraXTSimp <cnf> <threads>\n");
      fprintf(stdout,"s UNKNOWN\n");

      // Exit code 0: UNKNOWN.
      return 0; 
    }
  
  // Get first "timestamp".
  startTime = mira::getTime();
  
  // Initialization.
  minisat::SimpSolver Preprocessor;

  // Get the name of the problem instance to be solved.
  CNFFile = argv[1];  

  // Get the number of threads per client node.
  numThreads = atoi(argv[2]); if (numThreads < 1) {numThreads = 1;}

  // Setup a new global clause database that can be used by all threads.
  mira::clauseDB* theClauseDB = new mira::clauseDB(numThreads);

  // Read CNF file.
  gzFile CNFgz = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
  if (CNFgz == NULL)
    {
      // Something went wrong.
      fprintf(stdout,"c CNF File Error\n");      
      fprintf(stdout,"s UNKNOWN\n");

      // Delete clause database.
      delete theClauseDB; 
      
      // Exit code 0: UNKNOWN.
      return 0; 
    }
  parse_DIMACS(CNFgz, Preprocessor);
  gzclose(CNFgz);

  // Simplify the benchmark problem by processing unit clauses.
  if (!Preprocessor.simplify())
    {
      mira::printStatsBeforeSearch();
      endTime = mira::getTime();
      mira::printStatsAfterSearch("unsat",endTime-startTime);

      // Exit code 20: UNSATISFIABLE.
      return 20;
    }

  // Perform MiniSat2's preprocessing.
  bool resultMiniSatPP = Preprocessor.eliminate(true);
  numLiterals          = Preprocessor.nVars();
  numClauses           = Preprocessor.nClauses();

  // Benchmark instance not proven to be unsatisfiable by the preprocessor?
  if (resultMiniSatPP)
    {
      // Transfer the remaining clause database to MiraXTmini's database.
      if (!transferClauses(theClauseDB, Preprocessor)|| theClauseDB->masterBaseClauseVec.size() < 2)
	{
	  // Something went wrong.
	  fprintf(stdout,"c CNF Transfer Error\n");      
	  fprintf(stdout,"s UNKNOWN\n");

	  // Delete clause database.
	  delete theClauseDB; 

	  // Exit code 0: UNKNOWN.
	  return 0; 
	}
      
      // Print some statistics.
      mira::printStatsBeforeSearch();
      
      // Update the "end-of-database-pointer" of the clause database in order 
      // to know where the set of clauses of the original CNF file ends.
      theClauseDB->setCEIBase();
      
      // Initialize the control structure, managing the search process done by all involved threads.
      mira::ControlStructure* controlInfo = new mira::ControlStructure(numThreads, theClauseDB, startTime);
      
      // Initialize the decision queue, handling unchecked subproblems.
      mira::DecisionQueue* theDecisionQueue = new mira::DecisionQueue(numThreads, controlInfo);
      
      // Initialize the threads and combine the thread's data types 
      // with the global control structure and the decision queue.
      mira::ThreadData myThreads[numThreads];
      for (int i=0; i<numThreads; i++)
	{ 
	  myThreads[i].threadNum           = i; 
	  myThreads[i].threadControl       = controlInfo; 
	  myThreads[i].threadDecisionQueue = theDecisionQueue; 
	}
      
      // Define some thread parameters.
      pthread_attr_t attr;
      pthread_attr_init(&attr);
      pthread_attr_setstacksize(&attr, 65536);
      pthread_t threadID[numThreads];
      
      // Start all threads.
      for (int i=0; i<numThreads; i++) 
	{ pthread_create(&(threadID[i]),&attr,mira::startThreads,(void*)(&myThreads[i])); }
      
      // Wait until all threads are finished.
      for (int i=0; i<numThreads; i++) { pthread_join(threadID[i], NULL); }
      
      // Get second "timestamp".
      endTime = mira::getTime();
      
      // Result?
      if (controlInfo->SAT) 
	{ 
	  // Print some statistics.
	  mira::printStatsAfterSearch("sat",endTime-startTime);
	  
	  // Set ExitCode to SATISFIABLE.
	  ExitCode = 10;

	  // Verify MiraXTmini's satisfying variable assignment.
	  verifySolution(theClauseDB, controlInfo); 

	  // Extend the model and verify the entire satisfying variable assignment.
	  int* model = controlInfo->Solution;
	  Preprocessor.extendModel(model);
	  Preprocessor.verifyModel(model,CNFFile);

	  // Print satisfying assignment. 
	  fprintf(stdout,"v");
	  for (int L=1; L<numLiterals+1; L++) 
	    {
	      if ((model[L] & 1) == 1)
		{
		  fprintf(stdout," -%d",model[L] >> 1); 
		}
	      else
		{
		  fprintf(stdout," %d",model[L] >> 1);
		}
	    }
	  fprintf(stdout," 0\n");	  
	}
      else 
	{
	  // Benchmark unsatisfiable or running out of time?
	  if ((endTime - startTime) < mira::maxTime) 
	    { 
	      // Print some statistics.
	      mira::printStatsAfterSearch("unsat",endTime-startTime);

	      // Set ExitCode to UNSATISFIABLE.
	      ExitCode = 20;
	    }
	  else 
	    { 
	      // Print some statistics.
	      mira::printStatsAfterSearch("aborted",endTime-startTime);
	    }
	}
      
      // Delete the allocated memory blocks and return.   
      delete theDecisionQueue;
      delete controlInfo;
      delete theClauseDB; 
    }
  else 
    {
      mira::printStatsBeforeSearch();
      endTime = mira::getTime();
      mira::printStatsAfterSearch("unsat",endTime-startTime);

      // Set ExitCode to UNSATISFIABLE.
      ExitCode = 20;
    }

  // Return to OS.
  return ExitCode;
}