SAT_C.h

/*********************************************************************
 Copyright 2000-2003, 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.
*********************************************************************/

#ifndef __SAT_HEADER__
#define __SAT_HEADER__

#define	SAT_Manager void * 	

typedef long long long64; //this is for 32 bit unix machines
//typedef long long64;	    //this is for Windows or 64 bit unix machines


#ifndef _SAT_STATUS_
#define _SAT_STATUS_
enum SAT_StatusT {
    UNDETERMINED,
    UNSATISFIABLE,
    SATISFIABLE,
    TIME_OUT,
    MEM_OUT,
    ABORTED
};
#endif

#ifndef _CLS_STATUS_
#define _CLS_STATUS_
enum CLAUSE_STATUS
{
    ORIGINAL_CL,
    CONFLICT_CL,
    DELETED_CL,
    PROBE_CL,
    UNKNOWN_CL
};
#endif

#ifndef UNKNOWN
#define UNKNOWN 	2
#endif

/*============================================================

This is the header for using the sat solver. A typical flow is 

1. calling SAT_InitManager to get a new manager. You can pre-set 
   the number of variables upfront, or you can add it later by
   SAT_AddVariable.
   Variables are indexed from 1, NOT 0.

2. add clauses by calling SAT_AddClause. Clause is represented by
   an array of integers. Each literal is represented by 
   2 * VarIndex + Sign. The Sign is 0 for positive phased literals,
   and 1 for negative phased literals.
   For example, a clause (3 -5 11 -4 ) should be represented by
   { 6, 11, 22, 9 }
   Note: Each variable can occure no more than once in a clause.
   if a variable occures in both phase, the clause is automatically
   satisfied. If more than one occurance with same phase, they
   should be combined. IT IS YOUR RESPONSIBILITY TO KEEP EACH 
   CLAUSE NON-REDUNDENT, or the solver will not function correctly.

3. zchaff support incremental SAT solving. Clauses can be added
   or deleted from the database after each run. To accomplish 
   this, a clause is associated with a "Group ID". Each clause
   has one Group ID. The group of clauses with the same GID can 
   be deleted from the database by calling SAT_DeleteClauseGroup
   after each run. You need to call SAT_Reset to reset the state
   of the solver before begining a new run. 
   As an example, the first 10 clauses are associated with GID 1, 
   We add another 2 clauses with GID 2. After solving this instance
   with 12 clauses, we may want to delete the last 2 clauses and
   add another 3 clauses. We call SAT_DeleteClauseGroup with GID
   2 and add the three clauses (these three clauses can have any
   GID: either 1 if you don't want to delete them in the future,
   2 if you want to distinguish them from Group 1). Then you should
   call SAT_Reset() to reset the state of the solver, and call
   SAT_Solve() again to solve the new instance (a instance with 
   13 clauses). 
   You should obtain free GID using SAT_AllocClauseGroupID. When
   you call SAT_DeleteClauseGroup, the gid will be freed and can
   be re-used when you call SAT_AllocClauseGroupID() again.
   You can also merge two group of clauses into 1 by calling
   corresponding functions. 

4. Optionally, you may set the time limit and memory limit for
   the solver, note: time and memory limits are not exact.
   Also, you can set other paramenters like clause deletion
   etc. 

5. You can add hook function to do some extra work after 
   a certain number of decisions (branchings). A hook function 
   should accept input of a manager, and has no return value.

6. Calling SAT_Solve to solve the problem. it will return the 
   status of the solver.

7. If the problem is satisfiable, you can call SAT_GetVarAsgnment
   to get a variable assignment which satisfy the problem.

8. You can also get some statistics from the solver, such as 
   run time, mem usage, etc.

9. Release the manager by calling SAT_ReleaseManager.

You need to link the library libsat.a, also, though you can compile
your C program with c compiler when using this sat solver, you 
still need c++ linker to link the library. 

Have fun. 
			The Chaff Team
			(contact lintaoz@ee.princeton.edu
			for any questions or suggestions)
			2003. 5. 2
=============================================================*/


//Following are the main functions for the flow.

//init a manager
SAT_Manager SAT_InitManager(void);

void SAT_SetCacheSize(SAT_Manager mng, unsigned);

void SAT_SetMaxEntry(SAT_Manager mng, unsigned);

void SAT_SetMaxDistance(SAT_Manager	mng, unsigned);

void SAT_SetDynamicHeuristic(SAT_Manager mng, bool);

void SAT_SetApproximation(SAT_Manager mng, bool);

void SAT_SetMaxNumLearnedClause(SAT_Manager mng, unsigned);

void SAT_SetOldestEntry(SAT_Manager mng, unsigned);

void SAT_SetCleanLimit(SAT_Manager mng, unsigned);

void SAT_SetCrossFlag(SAT_Manager mng, bool);

void SAT_SetAdjustFlag(SAT_Manager mng, bool);

long double SAT_SatProb(SAT_Manager mng);

long double SAT_NumSolutions(SAT_Manager mng);

bool SAT_GMP(SAT_Manager mng);

void SAT_SetQuietFlag(SAT_Manager mng, bool);

//get the version of the solver
char * SAT_Version(SAT_Manager mng);

//release a manager
void SAT_ReleaseManager	(SAT_Manager 	mng);

//set the number of variables.
void SAT_SetNumVariables(SAT_Manager mng, 
			 int num_vars);

//add a variable. it will return the new var's index
int SAT_AddVariable	(SAT_Manager 	mng);

//the following functions will allow/disallow the variable to be branched
//user may want to branch only on certain variables (for example, primary 
//inputs of a circuit, if the CNF is generated from circuit).
//By default, all variables are branchable, usually, if a variable is 
//unbranchable, it's value should be determined by all the branchable variables.
//if that's not the case, then these variables may not get an assigned 
//value even if the solver says that the problem is satisfiable. 
//Notice, the solver determines if a problem is satisfiable by trying to assign 
//all the branchable variables. If all such variables can be assigned values
//without causing conflict, then the instance is reported as satisfiable, even
//if the instance is actually unsatisfiable because of unbranchable 
//variables being not dependent on branchable variables. 
void SAT_EnableVarBranch(SAT_Manager 	mng,
			 int 		vid);

void SAT_DisableVarBranch(SAT_Manager 	mng,
			 int 		vid);
//add a clause. a literal is a integer with value 2*V_idx + sign
//gid is the group ID. by default, gid equals 0 . Note: group 0
//clauses can't be deleted.
void SAT_AddClause	(SAT_Manager 	mng, 
			 int * 		clause_lits,
			 int 		num_lits,
			 int		gid);

//delete a clause group and learned clauses depending on them.
void SAT_DeleteClauseGroup (SAT_Manager mng,
			    int		gid);

//This will reset the solver so it will not keep the implications made before
void SAT_Reset(SAT_Manager mng);

//merge the clause group gid1 with gid2, return a new group which 
//contain both groups. 
int SAT_MergeClauseGroup	(SAT_Manager mng,
				 int	gid1,
				 int 	gid2);

//Allocate a free clause group id. will be -1 if no more available.
//current implementation allow 32 deletable group IDs ranging from
//1-32. Group 0 is the permanent group (i.e. can't delete).
int SAT_AllocClauseGroupID (SAT_Manager mng);

//followings are for clause gid manipulation
int SAT_IsSetClauseGroupID( SAT_Manager mng, int cl_idx, int id);
int SAT_SetClauseGroupID( SAT_Manager mng, int cl_idx, int id);
int SAT_ClearClauseGroupID( SAT_Manager mng, int cl_idx, int id);
//clauses belong to volatile group will always be deleted when
//SAT_DeleteClauseGroup is called
int SAT_GetVolatileGroupID (SAT_Manager mng);
//clauses belong to global group will never be deleted
int SAT_GetGlobalGroupID (SAT_Manager mng);


void SAT_SetTimeLimit	(SAT_Manager 	mng ,  
			 float 		runtime); 

//note: memory estimation is very rough, so allow 30% of error
//in both SetMemLimit and EstimateMemUsage. Also, in the run 
//time, the memory usage could be temporarily 50% larger than
//the limit (this occours when program reallocate memory because
//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
double SAT_GetElapsedCPUTime(SAT_Manager mng);
//current cpu time
double SAT_GetCurrentCPUTime(SAT_Manager mng);
//time spent on the whole solving process
double 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_NumDeletedClauses	(SAT_Manager mng);

long64 SAT_NumDeletedLiterals(SAT_Manager mng);

unsigned SAT_NumDecisions	(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