sys/src/libsat/misc.c

   1 #include <u.h>
   2 #include <libc.h>
   3 #include <sat.h>
   4 #include "impl.h"
   5
   6 SATSolve *
   7 satnew(void)
   8 {
   9         SATSolve *s;
  10
  11         s = calloc(1, sizeof(SATSolve));
  12         if(s == nil) return nil;
  13         s->bl[0].next = s->bl[0].prev = &s->bl[0];
  14         s->bl[1].next = s->bl[1].prev = &s->bl[1];
  15         s->bl[0].end = (uchar*)&s->bl[0] + SATBLOCKSZ; /* this block is "full" */
  16         s->bl[1].end = (uchar*)&s->bl[1] + SATBLOCKSZ;
  17         s->lastp[0] = &s->cl;
  18         s->lastp[1] = &s->learncl;
  19         s->lastbl = &s->bl[1];
  20         s->randfn = (long(*)(void*)) lrand;
  21
  22         s->goofprob = 0.02 * (1UL<<31);
  23         s->varρ = 1/0.9;
  24         s->clauseρ = 1/0.999;
  25         s->trivlim = 10;
  26         s->purgeΔ = 10000;
  27         s->purgeδ = 100;
  28         s->purgeα = 0.2;
  29         s->flushψ = (1ULL<<32)*0.05;
  30
  31         s->Δactivity = 1;
  32         s->Δclactivity = 1;
  33
  34         return s;
  35 }
  36
  37 void
  38 satfree(SATSolve *s)
  39 {
  40         SATBlock *b, *bb;
  41         int i;
  42
  43         if(s == nil) return;
  44         for(i = 0; i < 2; i++)
  45                 for(b = s->bl[i].next; b != &s->bl[i]; b = bb){
  46                         bb = b->next;
  47                         free(b);
  48                 }
  49         for(i = 0; i < 2 * s->nvar; i++)
  50                 free(s->lit[i].bimp);
  51         free(s->heap);
  52         free(s->trail);
  53         free(s->decbd);
  54         free(s->var);
  55         free(s->lit);
  56         free(s->cflcl);
  57         free(s->fullrcfl);
  58         free(s->fullrlits);
  59         free(s->scrap);
  60         free(s);
  61 }
  62
  63 void
  64 saterror(SATSolve *s, char *msg, ...)
  65 {
  66         char buf[ERRMAX];
  67         va_list va;
  68
  69         va_start(va, msg);
  70         vsnprint(buf, sizeof(buf), msg, va);
  71         va_end(va);
  72         s->scratched = 1;
  73         if(s != nil && s->errfun != nil)
  74                 s->errfun(buf, s->erraux);
  75         sysfatal("%s", buf);
  76 }
  77
  78 int
  79 satval(SATSolve *s, int l)
  80 {
  81         int m, v;
  82
  83         if(s->unsat) return -1;
  84         m = l >> 31;
  85         v = (l + m ^ m) - 1;
  86         if(v < 0 || v >= s->nvar) return -1;
  87         return s->lit[2*v+(m&1)].val;
  88 }
  89
  90 int
  91 satnrand(SATSolve *s, int n)
  92 {
  93         long slop, v;
  94
  95         if(n <= 1) return 0;
  96         slop = 0x7fffffff % n;
  97         do
  98                 v = s->randfn(s->randaux);
  99         while(v <= slop);
 100         return v % n;
 101 }
 102
 103 void *
 104 satrealloc(SATSolve *s, void *v, ulong n)
 105 {
 106         v = realloc(v, n);
 107         if(v == nil)
 108                 saterror(s, "realloc: %r");
 109         setmalloctag(v, getcallerpc(&s));
 110         return v;
 111 }
 112
 113 #define LEFT(x) (2*(x)+1)
 114 #define RIGHT(x) (2*(x)+2)
 115 #define UP(x) ((x)-1>>1)
 116
 117 static SATVar *
 118 heapswap(SATSolve *s, int i, int j)
 119 {
 120         SATVar *r;
 121
 122         if(i == j) return s->heap[i];
 123         r = s->heap[i];
 124         s->heap[i] = s->heap[j];
 125         s->heap[j] = r;
 126         s->heap[i]->heaploc = i;
 127         s->heap[j]->heaploc = j;
 128         return r;
 129 }
 130
 131 static void
 132 heapup(SATSolve *s, int i)
 133 {
 134         int m;
 135
 136         m = i;
 137         for(;;){
 138                 if(LEFT(i) < s->nheap && s->heap[LEFT(i)]->activity > s->heap[m]->activity)
 139                         m = LEFT(i);
 140                 if(RIGHT(i) < s->nheap && s->heap[RIGHT(i)]->activity > s->heap[m]->activity)
 141                         m = RIGHT(i);
 142                 if(i == m) break;
 143                 heapswap(s, m, i);
 144                 i = m;
 145         }
 146 }
 147
 148 static void
 149 heapdown(SATSolve *s, int i)
 150 {
 151         int p;
 152
 153         for(; i > 0 && s->heap[p = UP(i)]->activity < s->heap[i]->activity; i = p)
 154                 heapswap(s, i, p);
 155 }
 156
 157 SATVar *
 158 satheaptake(SATSolve *s)
 159 {
 160         SATVar *r;
 161
 162         assert(s->nheap > 0);
 163         r = heapswap(s, 0, --s->nheap);
 164         heapup(s, 0);
 165         r->heaploc = -1;
 166         return r;
 167 }
 168
 169 void
 170 satheapput(SATSolve *s, SATVar *v)
 171 {
 172         assert(s->nheap < s->nvar);
 173         v->heaploc = s->nheap;
 174         s->heap[s->nheap++] = v;
 175         heapdown(s, s->nheap - 1);
 176 }
 177
 178 void
 179 satreheap(SATSolve *s, SATVar *v)
 180 {
 181         int i;
 182
 183         i = v->heaploc;
 184         if(i < 0) return;
 185         heapup(s, i);
 186         heapdown(s, i);
 187 }
 188
 189 void
 190 satheapreset(SATSolve *s)
 191 {
 192         int i, n, j;
 193
 194         s->heap = satrealloc(s, s->heap, s->nvar * sizeof(SATVar *));
 195         n = s->nvar;
 196         s->nheap = n;
 197         for(i = 0; i < n; i++){
 198                 s->heap[i] = &s->var[i];
 199                 s->heap[i]->heaploc = i;
 200         }
 201         for(i = 0; i < n - 1; i++){
 202                 j = i + satnrand(s, n - i);
 203                 heapswap(s, i, j);
 204                 heapdown(s, i);
 205         }
 206         heapdown(s, n - 1);
 207 }