sat_c.h

命题逻辑的求解器,2004年SAT竞赛第一名的求解器

                     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);

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

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

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

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

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

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

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

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

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

#endif