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