109 lines
4.6 KiB
C
109 lines
4.6 KiB
C
#pragma lib "libsat.a"
|
||
|
||
typedef struct SATParam SATParam;
|
||
typedef struct SATClause SATClause;
|
||
typedef struct SATSolve SATSolve;
|
||
typedef struct SATBlock SATBlock;
|
||
typedef struct SATVar SATVar;
|
||
typedef struct SATLit SATLit;
|
||
typedef struct SATConflict SATConflict;
|
||
#pragma incomplete SATClause
|
||
#pragma incomplete SATVar
|
||
#pragma incomplete SATLit
|
||
#pragma incomplete SATConflict
|
||
|
||
/* user adjustable parameters */
|
||
struct SATParam {
|
||
void (*errfun)(char *, void *);
|
||
void *erraux;
|
||
long (*randfn)(void *);
|
||
void *randaux;
|
||
|
||
uint goofprob; /* probability of making a random decision, times 2**31 */
|
||
double varρ; /* Δactivity is multiplied by this after a conflict */
|
||
double clauseρ; /* Δclactivity is multiplied by this after a conflict */
|
||
int trivlim; /* number of extra literals we're willing to tolerate before substituting the trivial clause */
|
||
int purgeΔ; /* initial purge interval (number of conflicts before a purge) */
|
||
int purgeδ; /* increase in purge interval at purge */
|
||
double purgeα; /* α weight factor for purge heuristic */
|
||
u32int flushψ; /* agility threshold for restarts */
|
||
};
|
||
|
||
/* each block contains multiple SATClauses consecutively in its data region. each clause is 8 byte aligned and the total size is SATBLOCKSZ (64K) */
|
||
struct SATBlock {
|
||
SATBlock *next, *prev;
|
||
SATClause *last; /* last clause, ==nil for empty blocks */
|
||
void *end; /* first byte past the last clause */
|
||
uchar data[1];
|
||
};
|
||
|
||
struct SATSolve {
|
||
SATParam;
|
||
|
||
uchar unsat; /* ==1 if unsatisfiable. don't even try to solve. */
|
||
uchar scratched; /* <0 if error happened, state undefined */
|
||
|
||
SATBlock bl[2]; /* two doubly linked list heads: list bl[0] contains user clauses, list bl[1] contains learned clauses */
|
||
SATBlock *lastbl; /* the last block we added a learned clause to */
|
||
SATClause *cl; /* all clauses are linked together; this is the first user clause */
|
||
SATClause *learncl; /* first learned clause */
|
||
SATClause **lastp[2]; /* this points towards the last link in each linked list */
|
||
int ncl; /* total number of clauses */
|
||
int ncl0; /* number of user clauses */
|
||
SATVar *var; /* all variables (array with nvar elements) */
|
||
SATLit *lit; /* all literals (array with 2*nvar elements) */
|
||
int nvar;
|
||
int nvaralloc; /* space allocated for variables */
|
||
int *trail; /* the trail contains all literals currently assumed true */
|
||
int ntrail;
|
||
int *decbd; /* decision boundaries. trail[decbd[i]] has the first literal of level i */
|
||
int lvl; /* current decision level */
|
||
SATVar **heap; /* binary heap with free variables, sorted by activity (nonfree variables are removed lazily and so may also be in it) */
|
||
int nheap;
|
||
|
||
uint *lvlstamp; /* used to "stamp" levels during conflict resolution and purging */
|
||
uint stamp; /* current "stamp" counter */
|
||
|
||
int forptr; /* trail[forptr] is the first literal we haven't explored the implications of yet */
|
||
int binptr; /* ditto for binary implications */
|
||
|
||
int *cflcl; /* during conflict resolution we build the learned clause in here */
|
||
int ncflcl;
|
||
int cflclalloc; /* space allocated for cflcl */
|
||
int cfllvl; /* the maximum level of the literals in cflcl, cflcl[0] excluded */
|
||
int cflctr; /* number of unresolved literals during conflict resolution */
|
||
|
||
double Δactivity; /* activity increment for variables */
|
||
double Δclactivity; /* activity increment for clauses */
|
||
|
||
uvlong conflicts; /* total number of conflicts so far */
|
||
|
||
uvlong nextpurge; /* purge happens when conflicts >= nextpurge */
|
||
uint purgeival; /* increment for nextpurge */
|
||
/* during a purge we do a "full run", assigning all variables and recording conflicts rather than resolving them */
|
||
SATConflict *fullrcfl; /* conflicts found thus */
|
||
int nfullrcfl;
|
||
int fullrlvl; /* minimum cfllvl for conflicts found during purging */
|
||
int *fullrlits; /* literals implied by conflicts at level fullrlvl */
|
||
int nfullrlits;
|
||
int rangecnt[256]; /* number of clauses with certain range values */
|
||
|
||
u64int nextflush; /* flush happens when conflicts >= nextflush */
|
||
u32int flushu, flushv, flushθ; /* variables for flush scheduling algorithm */
|
||
u32int agility; /* agility is a measure how quickly variables are being flipped. high agility inhibits flushes */
|
||
|
||
void *scrap; /* auxiliary memory that may need to be freed after a fatal error */
|
||
};
|
||
|
||
SATSolve *satnew(void);
|
||
SATSolve *satadd1(SATSolve *, int *, int);
|
||
SATSolve *sataddv(SATSolve *, ...);
|
||
SATSolve *satrange1(SATSolve *, int *, int, int, int);
|
||
SATSolve *satrangev(SATSolve *, int, int, ...);
|
||
int satsolve(SATSolve *);
|
||
int satmore(SATSolve *);
|
||
int satval(SATSolve *, int);
|
||
void satfree(SATSolve *);
|
||
void satreset(SATSolve *);
|
||
int satget(SATSolve *, int, int *, int);
|
||
void satvafix(va_list);
|