sat.h

命题逻辑的求解器,2004年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,
    DELETED_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
// of insufficiency in the initial allocation).
void SAT_SetMemLimit(SAT_Manager        mng,