sys/include/sat.h

   1 #pragma lib "libsat.a"
   2
   3 typedef struct SATParam SATParam;
   4 typedef struct SATClause SATClause;
   5 typedef struct SATSolve SATSolve;
   6 typedef struct SATBlock SATBlock;
   7 typedef struct SATVar SATVar;
   8 typedef struct SATLit SATLit;
   9 typedef struct SATConflict SATConflict;
  10 #pragma incomplete SATClause
  11 #pragma incomplete SATVar
  12 #pragma incomplete SATLit
  13 #pragma incomplete SATConflict
  14
  15 /* user adjustable parameters */
  16 struct SATParam {
  17         void (*errfun)(char *, void *);
  18         void *erraux;
  19         long (*randfn)(void *);
  20         void *randaux;
  21
  22         uint goofprob; /* probability of making a random decision, times 2**31 */
  23         double varρ; /* Δactivity is multiplied by this after a conflict */
  24         double clauseρ; /* Δclactivity is multiplied by this after a conflict */
  25         int trivlim; /* number of extra literals we're willing to tolerate before substituting the trivial clause */
  26         int purgeΔ; /* initial purge interval (number of conflicts before a purge) */
  27         int purgeδ; /* increase in purge interval at purge */
  28         double purgeα; /* α weight factor for purge heuristic */
  29         u32int flushψ; /* agility threshold for restarts */
  30 };
  31
  32 /* each block contains multiple SATClauses consecutively in its data region. each clause is 8 byte aligned and the total size is SATBLOCKSZ (64K) */
  33 struct SATBlock {
  34         SATBlock *next, *prev;
  35         SATClause *last; /* last clause, ==nil for empty blocks */
  36         void *end; /* first byte past the last clause */
  37         uchar data[1];
  38 };
  39
  40 struct SATSolve {
  41         SATParam;
  42
  43         uchar unsat; /* ==1 if unsatisfiable. don't even try to solve. */
  44         uchar scratched; /* <0 if error happened, state undefined */
  45
  46         SATBlock bl[2]; /* two doubly linked list heads: list bl[0] contains user clauses, list bl[1] contains learned clauses */
  47         SATBlock *lastbl; /* the last block we added a learned clause to */
  48         SATClause *cl; /* all clauses are linked together; this is the first user clause */
  49         SATClause *learncl; /* first learned clause */
  50         SATClause **lastp[2]; /* this points towards the last link in each linked list */
  51         int ncl; /* total number of clauses */
  52         int ncl0; /* number of user clauses */
  53         SATVar *var; /* all variables (array with nvar elements) */
  54         SATLit *lit; /* all literals (array with 2*nvar elements) */
  55         int nvar;
  56         int nvaralloc; /* space allocated for variables */
  57         int *trail; /* the trail contains all literals currently assumed true */
  58         int ntrail;
  59         int *decbd; /* decision boundaries. trail[decbd[i]] has the first literal of level i */
  60         int lvl; /* current decision level */
  61         SATVar **heap; /* binary heap with free variables, sorted by activity (nonfree variables are removed lazily and so may also be in it) */
  62         int nheap;
  63
  64         uint *lvlstamp; /* used to "stamp" levels during conflict resolution and purging */
  65         uint stamp; /* current "stamp" counter */
  66
  67         int forptr; /* trail[forptr] is the first literal we haven't explored the implications of yet */
  68         int binptr; /* ditto for binary implications */
  69
  70         int *cflcl; /* during conflict resolution we build the learned clause in here */
  71         int ncflcl;
  72         int cflclalloc; /* space allocated for cflcl */
  73         int cfllvl; /* the maximum level of the literals in cflcl, cflcl[0] excluded */
  74         int cflctr; /* number of unresolved literals during conflict resolution */
  75
  76         double Δactivity; /* activity increment for variables */
  77         double Δclactivity; /* activity increment for clauses */
  78
  79         uvlong conflicts; /* total number of conflicts so far */
  80
  81         uvlong nextpurge; /* purge happens when conflicts >= nextpurge */
  82         uint purgeival; /* increment for nextpurge */
  83         /* during a purge we do a "full run", assigning all variables and recording conflicts rather than resolving them */
  84         SATConflict *fullrcfl; /* conflicts found thus */
  85         int nfullrcfl;
  86         int fullrlvl; /* minimum cfllvl for conflicts found during purging */
  87         int *fullrlits; /* literals implied by conflicts at level fullrlvl */
  88         int nfullrlits;
  89         int rangecnt[256]; /* number of clauses with certain range values */
  90
  91         u64int nextflush; /* flush happens when conflicts >= nextflush */
  92         u32int flushu, flushv, flushθ; /* variables for flush scheduling algorithm */
  93         u32int agility; /* agility is a measure how quickly variables are being flipped. high agility inhibits flushes */
  94
  95         void *scrap; /* auxiliary memory that may need to be freed after a fatal error */
  96 };
  97
  98 SATSolve *satnew(void);
  99 SATSolve *satadd1(SATSolve *, int *, int);
 100 SATSolve *sataddv(SATSolve *, ...);
 101 SATSolve *satrange1(SATSolve *, int *, int, int, int);
 102 SATSolve *satrangev(SATSolve *, int, int, ...);
 103 int satsolve(SATSolve *);
 104 int satmore(SATSolve *);
 105 int satval(SATSolve *, int);
 106 void satfree(SATSolve *);
 107 void satreset(SATSolve *);
 108 int satget(SATSolve *, int, int *, int);
 109 void satvafix(va_list);