sat.h

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

#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,
    MARKED_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 [e-mail]
			for any questions or suggestions)
			2004. 3. 10
=============================================================*/


//Following are the main functions for the flow.

//init a manager
SAT_Manager SAT_InitManager(void);

//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 = 0);

//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