sat.h

这是一种很好的SAT解析器。通过它

//of insufficiency in the initial allocation). 
void SAT_SetMemLimit	(SAT_Manager 	mng, 
			 int 		num_bytes);


int SAT_Solve 	(SAT_Manager 	mng);
//enum SAT_StatusT
//Get a variable's assignment. -1 means UNKNOWN or undicided
int SAT_GetVarAsgnment	(SAT_Manager	mng,
			 int 		v_idx);

//this is used for randomness in decision making
void SAT_SetRandomness	(SAT_Manager	mng,
			 int 		n);
//if the seed < 0, solver will use the day timer to
//get a "psuedo real random" seed.
void SAT_SetRandSeed	(SAT_Manager	mng,
			 int		seed);

//add a hookfunction. This function will be called
//every "interval" of decisions. You can add more than
//one such hook functions. i.e. call SAT_AddHookFun more
//than once. 
void SAT_AddHookFun   		(SAT_Manager	mng, 
				 void(*fun)(void *), 
				 int	interval);

/* =======================================================
This function is for users who want to customize their own
decision making strategy. 

What you can do is add a hook function with interval of 1, 
that function will be called before every decision. Inside
this hook function, use SAT_MakeDecision to make decision
with variable "vid" and "sign". sign = 1 means value of 
the variable be 0. 

If there are no free variable left, problem is satisfied,
call SAT_MakeDecision with vid = 0 && sign = 0 will cause 
solver exit with status "SATISFIABLE".

Here is an example:

void my_own_decision (SAT_Manager mng)
{
int n_var = SAT_NumVariables(mng);
int i;
for (i=1; i<n_var; ++i) {
  if (SAT_GetVarAsgnment(mng, i)==UNKNOWN){
    SAT_MakeDecision(mng, i, 1); //make decision with value 0;
    break;
  }
}
if (i >= n_var) //every var got an assignment, no free var left 
  SAT_MakeDecision (mng, 0, 0);
}
======================================================== */
void SAT_MakeDecision	(SAT_Manager	mng,
			 int		vid,
			 int		sign);

//Following are statistics collecting functions
int SAT_EstimateMemUsage(SAT_Manager mng);
//time elapsed from last call of GetElapsedCPUTime
float SAT_GetElapsedCPUTime(SAT_Manager mng);
//current cpu time
float SAT_GetCurrentCPUTime(SAT_Manager mng);
//time spent on the whole solving process
float SAT_GetCPUTime	(SAT_Manager mng);

int SAT_NumLiterals	(SAT_Manager mng);

int SAT_NumClauses	(SAT_Manager mng);

int SAT_NumVariables	(SAT_Manager mng);

int SAT_InitNumLiterals	(SAT_Manager mng);

int SAT_InitNumClauses	(SAT_Manager mng);

long64 SAT_NumAddedLiterals(SAT_Manager mng);

int SAT_NumAddedClauses	(SAT_Manager mng);

int SAT_NumShrinkings (SAT_Manager mng);

int SAT_NumDeletedClauses	(SAT_Manager mng);

int SAT_NumDelOrigCls	(SAT_Manager mng);

long64 SAT_NumDeletedLiterals(SAT_Manager mng);

int SAT_NumDecisions	(SAT_Manager mng);
int SAT_NumDecisionsStackConf	(SAT_Manager mng);
int SAT_NumDecisionsVsids	(SAT_Manager mng);
int SAT_NumDecisionsShrinking	(SAT_Manager mng);


int SAT_Random_Seed		(SAT_Manager mng);

long64 SAT_NumImplications	(SAT_Manager mng);

int SAT_MaxDLevel	(SAT_Manager mng);

float SAT_AverageBubbleMove	(SAT_Manager mng);
//Following function will allow you to traverse all the
//clauses and literals. Clause is represented by a index.
//The original clauses' indice are not changed during the
//whole process, while added clauses may get deleted, so
//a certain index may not always represent the same 
//clause, also, a index may not always be valid.
int SAT_GetFirstClause	(SAT_Manager mng);

//GetClauseType will get the clause's type. it can be
//ORIGINAL_CL, CONFLICT_CL, PROBE_CL
int SAT_GetClauseType (SAT_Manager mng, int cl_idx);

//if there are no more clauses left, return value is -1.
//the organization is like :
//index 0 ... InitNumClauses - 1 are the original clauses
//after that, they are added clauses.
int SAT_GetNextClause	(SAT_Manager mng, int cl_idx);

int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx);

//the lits array should have been pre-allocated enough memory
//to store all the lits of a clause. Use SAT_GetClauseNumLits to find
//out before-hand how much memory is required.
void SAT_GetClauseLits	(SAT_Manager mng, int cl_idx,  int * lits);

//Following functions dictate the run time behavior
//Don't mess with them unless you know what you are doing
void SAT_EnableConfClsDeletion(SAT_Manager mng);
void SAT_DisableConfClsDeletion(SAT_Manager mng);
void SAT_SetClsDeletionInterval(SAT_Manager mng, int freq);

void SAT_SetMaxUnrelevance(SAT_Manager mng, int n);
void SAT_SetMinClsLenForDelete(SAT_Manager mng, int n);
void SAT_SetMaxConfClsLenAllowed(SAT_Manager mng, int n);

//  void SAT_AllowMultipleConflicts(SAT_Manager mng);
//  void SAT_AllowMultipleConfCls(SAT_Manager mng);
//  void SAT_SetLitPoolCompactRatio(SAT_Manager mng, float ratio);
//  void SAT_SetLitPoolExpantionRatio(SAT_Manager mng, float ration);

//this function cleans all learned clauses in the database.
//it can be called if you incrementally solving many instances and 
//the learned clauses occupy too much memory. By calling 
//this function, it essentially equal to a fresh restart, i.e. throw
//away the learned clauses obtained so far. 
void SAT_CleanUpDatabase (SAT_Manager mng);

//Followings are functions to facilitate the translation from 
//Circuit to a CNF representation. It will automatically generate
//the necessary clauses to represent the gates.
//Note: The input convension are the same as in AddClause,
//      e.g. 2 * Vid + Sign
//NOTE: You need to make sure that the signals (a, b, c, o etc) are
//distinctive. I.e. the two inputs to a AND2 gate are different
//signals. Otherwise, the solver may behave incorrectly. Don't 
//add a gate that has signal a and a' as inputs. You should do 
//these kinds of special case simplifications by yourself. 


void SAT_GenClsAnd2	(SAT_Manager mng, 
			 int a,
			 int b,
			 int o,
			 int gid = 0);

void SAT_GenClsAndN	(SAT_Manager mng, 
			 int * inputs,
			 int num_inputs,
			 int o, 
			 int gid = 0);

void SAT_GenClsOr2	(SAT_Manager mng, 
			 int a,
			 int b,
			 int o, 
			 int gid = 0 );

void SAT_GenClsOrN	(SAT_Manager mng, 
			 int * inputs,
			 int num_inputs,
			 int o, 
			 int gid = 0 );

void SAT_GenClsNand2	(SAT_Manager mng, 
			 int a,
			 int b,
			 int o,
			 int gid = 0 );

void SAT_GenClsNandN	(SAT_Manager mng, 
			 int * inputs,
			 int num_inputs,
			 int o,
			 int gid = 0 );

void SAT_GenClsNor2	(SAT_Manager mng, 
			 int a,
			 int b,
			 int o, 
			 int gid = 0 );

void SAT_GenClsNorN	(SAT_Manager mng, 
			 int * inputs,
			 int num_inputs,
			 int o,
			 int gid = 0);

void SAT_GenClsXor	(SAT_Manager mng, 
			 int a,
			 int b,
			 int o,
			 int gid = 0 );

void SAT_GenClsNot	(SAT_Manager mng, 
			 int a,
			 int o,
			 int gid = 0);


#endif