1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
#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);
|
