sys/src/libsat/impl.h

   1 /* note that internally, literals use a representation different from the API.
   2  * variables are numbered from 0 (not 1) and 2v and 2v+1 correspond to v
   3  * and ¬v, resp.  */
   4 #define VAR(l) ((l)>>1)
   5 #define NOT(l) ((l)^1)
   6
   7 /* l[0] and l[1] are special: they are the watched literals.
   8  * all clauses that have literal l on their watchlist form a linked list starting with s->lit[l].watch
   9  * and watch[i] having the next clause for l[i] */
  10 struct SATClause {
  11         SATClause *next;
  12         SATClause *watch[2];
  13         double activity; /* activity is increased every time a clause is used to resolve a conflict (tiebreaking heuristic during purging) */
  14         int n; /* >= 2 for learned clauses and > 2 for input clauses (binary input clauses are kept in the bimp tables) */
  15         ushort range; /* heuristic used during purging, low range => keep clause (range 0..256) */
  16         int l[1];
  17 };
  18
  19 struct SATLit {
  20         int *bimp; /* array of literals implied by this literal through binary clauses (Binary IMPlications) */
  21         SATClause *watch; /* linked list of watched clauses */
  22         int nbimp;
  23         char val; /* -1 = not assigned, 0 = false, 1 = true */
  24 };
  25
  26 struct SATVar {
  27         double activity; /* activity is increased every time a variable shows up in a conflict */
  28         union {
  29                 SATClause *reason; /* nil for decision and free literals */
  30                 int binreason; /* used when isbinreason == 1: the reason is the clause l ∨ l->binreason */
  31         };
  32         int lvl; /* level at which this variable is defined, or -1 for free variables */
  33         int heaploc; /* location in binary heap or -1 when not in heap */
  34         uint stamp; /* "stamp" value used for conflict resolution etc. */
  35         uchar flags; /* see below */
  36         char isbinreason;
  37 };
  38
  39 enum {
  40         VARPHASE = 1, /* for a free variables, VARPHASE is used as a first guess the next time it is picked */
  41         VARUSER = 0x80, /* user assigned variable (unit clause in input) */
  42 };
  43
  44 /* records conflicts during purging */
  45 struct SATConflict {
  46         union {
  47                 SATClause *c;
  48                 uvlong b;
  49         };
  50         int lvl; /* bit 31 denotes binary conflict */
  51 };
  52 #define CFLLVL(c) ((c).lvl & 0x7fffffff)
  53
  54 enum {
  55         SATBLOCKSZ = 65536,
  56         SATVARALLOC = 64,
  57         CLAUSEALIGN = 8,
  58         CFLCLALLOC = 16,
  59 };
  60
  61 void saterror(SATSolve *, char *, ...);
  62 void sataddtrail(SATSolve *, int);
  63 void satdebuginit(SATSolve *);
  64 void satprintstate(SATSolve *);
  65 void satsanity(SATSolve *);
  66 SATVar *satheaptake(SATSolve *);
  67 void satheapput(SATSolve *, SATVar *);
  68 void satreheap(SATSolve *, SATVar *);
  69 void satheapreset(SATSolve *);
  70 int satnrand(SATSolve *, int);
  71 void *satrealloc(SATSolve *, void *, ulong);
  72 SATClause *satnewclause(SATSolve *, int, int);
  73 SATClause *satreplclause(SATSolve *, int);
  74 void satcleanup(SATSolve *, int);
  75 void satbackjump(SATSolve *, int);
  76
  77 #define signf(l) (((l)<<31>>31|1)*((l)+2>>1))
  78 #pragma varargck type "Γ" SATClause*
  79
  80 #define ε 2.2250738585072014e-308
  81 #define MAXACTIVITY 1e100