sys/src/libsat/satsolve.c

   1 #include <u.h>
   2 #include <libc.h>
   3 #include <sat.h>
   4 #include "impl.h"
   5
   6 /* the solver follows Algorithm C from Knuth's The Art of Computer Programming, Vol. 4, Fascicle 6 */
   7
   8 #define verbosestate 0
   9 #define verboseforcing 0
  10 #define verboseconflict 0
  11 #define paranoia 0
  12 #define sanity(s) if(paranoia) satsanity(s)
  13
  14 void
  15 sataddtrail(SATSolve *s, int l)
  16 {
  17         s->trail[s->ntrail++] = l;
  18         s->lit[l].val = 1;
  19         s->lit[NOT(l)].val = 0;
  20         s->var[VAR(l)].lvl = s->lvl;
  21         s->agility -= s->agility >> 13;
  22         if(((s->var[VAR(l)].flags ^ l) & 1) != 0)
  23                 s->agility += 1<<19;
  24         if(verbosestate) satprintstate(s);
  25 }
  26
  27 /* compute watchlists from scratch */
  28 static void
  29 rewatch(SATSolve *s)
  30 {
  31         SATLit *l;
  32         SATClause *c;
  33         int i, j, x;
  34
  35         for(l = s->lit; l < s->lit + 2*s->nvar; l++)
  36                 l->watch = nil;
  37         for(c = s->cl; c != nil; c = c->next)
  38                 for(i = 0; i < 2; i++){
  39                         if(s->lit[c->l[i]].val == 0)
  40                                 for(j = 2; j < c->n; j++)
  41                                         if(s->lit[c->l[j]].val != 0){
  42                                                 x = c->l[i], c->l[i] = c->l[j], c->l[j] = x;
  43                                                 break;
  44                                         }
  45                         c->watch[i] = s->lit[c->l[i]].watch;
  46                         s->lit[c->l[i]].watch = c;
  47                 }
  48 }
  49
  50 /* jump back to decision level d */
  51 void
  52 satbackjump(SATSolve *s, int d)
  53 {
  54         int l;
  55         SATVar *v;
  56
  57         if(s->lvl == d) return;
  58         while(s->ntrail > s->decbd[d + 1]){
  59                 l = s->trail[--s->ntrail];
  60                 v = &s->var[VAR(l)];
  61                 if((v->flags & VARUSER) != 0){ /* don't delete user assignments */
  62                         s->ntrail++;
  63                         break;
  64                 }
  65                 s->lit[l].val = -1;
  66                 s->lit[NOT(l)].val = -1;
  67                 v->flags = v->flags & ~1 | l & 1;
  68                 v->lvl = -1;
  69                 v->reason = nil;
  70                 v->isbinreason = 0;
  71                 if(v->heaploc < 0)
  72                         satheapput(s, v);
  73         }
  74         s->lvl = d;
  75         if(s->forptr > s->ntrail) s->forptr = s->ntrail;
  76         if(s->binptr > s->ntrail) s->binptr = s->ntrail;
  77         if(verbosestate) satprintstate(s);
  78 }
  79
  80 static void
  81 solvinit(SATSolve *s)
  82 {
  83         satdebuginit(s);
  84         satheapreset(s);
  85         s->decbd = satrealloc(s, s->decbd, (s->nvar + 1) * sizeof(int));
  86         s->decbd[0] = 0;
  87         s->trail = satrealloc(s, s->trail, sizeof(int) * s->nvar);
  88         s->fullrlits = satrealloc(s, s->fullrlits, sizeof(int) * s->nvar);
  89         s->lvlstamp = satrealloc(s, s->lvlstamp, sizeof(int) * s->nvar);
  90         memset(s->lvlstamp, 0, sizeof(int) * s->nvar);
  91         if(s->cflclalloc == 0){
  92                 s->cflcl = satrealloc(s, s->cflcl, CFLCLALLOC * sizeof(int));
  93                 s->cflclalloc = CFLCLALLOC;
  94         }
  95         rewatch(s);
  96
  97         s->conflicts = 0;
  98         s->nextpurge = s->purgeΔ;
  99         s->purgeival = s->purgeΔ;
 100         s->nextflush = 1;
 101         s->flushu = 1;
 102         s->flushv = 1;
 103         s->flushθ = s->flushψ;
 104         s->agility = 0;
 105
 106         satbackjump(s, 0);
 107         s->forptr = 0;
 108         s->binptr = 0;
 109 }
 110
 111 void
 112 satcleanup(SATSolve *s, int all)
 113 {
 114         SATBlock *b, *bn;
 115
 116         if(all){
 117                 *s->lastp[0] = nil;
 118                 s->learncl = nil;
 119                 s->lastp[1] = &s->learncl;
 120                 s->ncl = s->ncl0;
 121         }
 122         for(b = s->bl[1].next; b != &s->bl[1]; b = bn){
 123                 bn = b->next;
 124                 if(b->last != nil && !all) continue;
 125                 b->next->prev = b->prev;
 126                 b->prev->next = b->next;
 127                 free(b);
 128         }
 129         s->lastbl = s->bl[1].prev;
 130         free(s->fullrlits);
 131         s->fullrlits = nil;
 132         free(s->lvlstamp);
 133         s->lvlstamp = nil;
 134         free(s->cflcl);
 135         s->cflcl = nil;
 136         s->cflclalloc = 0;
 137 }
 138
 139 static void
 140 stampoverflow(SATSolve *s)
 141 {
 142         int i;
 143
 144         for(i = 0; i < s->nvar; i++){
 145                 s->var[i].stamp = 0;
 146                 s->lvlstamp[i] = 0;
 147         }
 148         s->stamp = -2;
 149 }
 150
 151 /* "bump" the variable, i.e. increase its activity score. reduce all score when one exceeds MAXACTIVITY (1e100) */
 152 static void
 153 varbump(SATSolve *s, SATVar *v)
 154 {
 155         v->activity += s->Δactivity;
 156         satreheap(s, v);
 157         if(v->activity < MAXACTIVITY) return;
 158         for(v = s->var; v < s->var + s->nvar; v++)
 159                 if(v->activity != 0){
 160                         v->activity /= MAXACTIVITY;
 161                         if(v->activity < ε)
 162                                 v->activity = ε;
 163                 }
 164         s->Δactivity /= MAXACTIVITY;
 165 }
 166
 167 /* ditto for clauses */
 168 static void
 169 clausebump(SATSolve *s, SATClause *c)
 170 {
 171         c->activity += s->Δclactivity;
 172         if(c->activity < MAXACTIVITY) return;
 173         for(c = s->cl; c != nil; c = c->next)
 174                 if(c->activity != 0){
 175                         c->activity /= MAXACTIVITY;
 176                         if(c->activity < ε)
 177                                 c->activity = ε;
 178                 }
 179         s->Δclactivity /= MAXACTIVITY;
 180 }
 181
 182 /* pick a literal. normally we pick the variable with highest activity from the heap. sometimes we goof and pick a random one. */
 183 static void
 184 decision(SATSolve *s)
 185 {
 186         SATVar *v;
 187
 188         s->decbd[++s->lvl] = s->ntrail;
 189         if((uint)s->randfn(s->randaux) < s->goofprob){
 190                 v = s->heap[satnrand(s, s->nheap)];
 191                 if(v->lvl < 0)
 192                         goto gotv;
 193         }
 194         do
 195                 v = satheaptake(s);
 196         while(v->lvl >= 0);
 197 gotv:
 198         sataddtrail(s, 2 * (v - s->var) + (v->flags & VARPHASE));
 199 }
 200
 201 /* go through the watchlist of a literal that just turned out false. */
 202 /* full == 1 records the first conflict and goes on rather than aborting immediately */
 203 static SATClause *
 204 forcing(SATSolve *s, int l, int full)
 205 {
 206         SATClause **cp, *rc, *c, *xp;
 207         int v0;
 208         int x, j;
 209
 210         cp = &s->lit[l].watch;
 211         rc = nil;
 212         if(verboseforcing) print("forcing literal %d\n", signf(l));
 213         while(c = *cp, c != nil){
 214                 if(l == c->l[0]){
 215                         /* this swap implies that the reason r for a literal l always has r->l[0]==l */
 216                         x = c->l[1], c->l[1] = c->l[0], c->l[0] = x;
 217                         xp = c->watch[1], c->watch[1] = c->watch[0], c->watch[0] = xp;
 218                 }
 219                 assert(c->l[1] == l);
 220                 v0 = s->lit[c->l[0]].val;
 221                 if(v0 > 0) /* the clause is true anyway */
 222                         goto next;
 223                 for(j = 2; j < c->n; j++)
 224                         if(s->lit[c->l[j]].val != 0){
 225                                 /* found another literal to watch for this clause */
 226                                 if(verboseforcing) print("moving clause %+Γ onto watchlist %d\n", c, signf(c->l[j]));
 227                                 *cp = c->watch[1];
 228                                 x = c->l[j], c->l[j] = c->l[1], c->l[1] = x;
 229                                 c->watch[1] = s->lit[x].watch;
 230                                 s->lit[x].watch = c;
 231                                 goto cont;
 232                         }
 233                 if(v0 == 0){
 234                         /* conflict */
 235                         if(!full) return c;
 236                         if(rc == nil) rc = c;
 237                         goto next;
 238                 }
 239                 if(verboseforcing) print("inferring %d using clause %+Γ\n", signf(c->l[0]), c);
 240                 sataddtrail(s, c->l[0]);
 241                 s->var[VAR(c->l[0])].reason = c;
 242         next:
 243                 cp = &c->watch[1];
 244         cont: ;
 245         }
 246         return rc;
 247 }
 248
 249 /* forcing() for binary implications */
 250 static uvlong
 251 binforcing(SATSolve *s, int l, int full)
 252 {
 253         SATLit *lp;
 254         int i, m;
 255         uvlong rc;
 256
 257         lp = &s->lit[l];
 258         rc = 0;
 259         if(verboseforcing && lp->nbimp > 0) print("forcing literal %d (binary)\n", signf(l));
 260         for(i = 0; i < lp->nbimp; i++){
 261                 m = lp->bimp[i];
 262                 switch(s->lit[m].val){
 263                 case -1:
 264                         if(verboseforcing) print("inferring %d using binary clause (%d) ∨ %d\n", signf(m), -signf(l), signf(m));
 265                         sataddtrail(s, m);
 266                         s->var[VAR(m)].binreason = NOT(l);
 267                         s->var[VAR(m)].isbinreason = 1;
 268                         break;
 269                 case 0:
 270                         if(verboseforcing) print("conflict (%d) ∨ (%d)\n", -signf(l), signf(m));
 271                         if(rc == 0) rc = (uvlong)NOT(l) << 32 | (uint)m;
 272                         if(!full) return rc;
 273                         break;
 274                 }
 275         }
 276         return rc;
 277 }
 278
 279 /* check if we can discard the previously learned clause because the current one subsumes it */
 280 static int
 281 checkdiscard(SATSolve *s)
 282 {
 283         SATClause *c;
 284         SATVar *v;
 285         int q, j;
 286
 287         if(s->lastp[1] == &s->learncl) return 0;
 288         c = (SATClause*) ((uchar*) s->lastp[1] - (uchar*) &((SATClause*)0)->next);
 289         if(s->lit[c->l[0]].val >= 0) return 0; /* clause is a reason, hands off */
 290         q = s->ncflcl;
 291         for(j = c->n - 1; q > 0 && j >= q; j--){
 292                 v = &s->var[VAR(c->l[j])];
 293                 /* check if literal is in the current clause */
 294                 if(c->l[j] == s->cflcl[0] || (uint)v->lvl <= s->cfllvl && v->stamp == s->stamp)
 295                         q--;
 296         }
 297         return q == 0;
 298 }
 299
 300 /* add the clause we just learned to our collection */
 301 static SATClause *
 302 learn(SATSolve *s, int notriv)
 303 {
 304         SATClause *r;
 305         int i, l, triv;
 306
 307         /* clauses that are too complicated are not worth it. learn the trivial clause (all decisions negated) instead */
 308         if(triv = !notriv && s->ncflcl > s->lvl + s->trivlim){
 309                 assert(s->lvl + 1 <= s->cflclalloc);
 310                 for(i = 1; i <= s->lvl; i++)
 311                         s->cflcl[i] = NOT(s->trail[s->decbd[s->lvl + 1 - i]]);
 312                 s->ncflcl = s->lvl + 1;
 313         }
 314         if(s->ncflcl == 1) /* unit clauses are handled by putting them on the trail in conflict() */
 315                 return nil;
 316         if(!triv && checkdiscard(s))
 317                 r = satreplclause(s, s->ncflcl);
 318         else
 319                 r = satnewclause(s, s->ncflcl, 1);
 320         r->n = s->ncflcl;
 321         memcpy(r->l, s->cflcl, s->ncflcl * sizeof(int));
 322         for(i = 0; i < 2; i++){
 323                 l = r->l[i];
 324                 r->watch[i] = s->lit[l].watch;
 325                 s->lit[l].watch = r;
 326         }
 327         return r;
 328 }
 329
 330 /* recursive procedure to determine if a literal is redundant.
 331  * to avoid repeated work, each known redundant literal is stamped with stamp+1
 332  * and each known nonredundant literal is stamped with stamp+2.
 333  */
 334 static int
 335 redundant(SATSolve *s, int l)
 336 {
 337         SATVar *v, *w;
 338         SATClause *c;
 339         int i, r;
 340
 341         v = &s->var[VAR(l)];
 342         if(v->isbinreason){
 343                 /* stupid special case code */
 344                 r = v->binreason;
 345                 w = &s->var[VAR(r)];
 346                 if(w->lvl != 0){
 347                         if(w->stamp == s->stamp + 2)
 348                                 return 0;
 349                         if(w->stamp < s->stamp && (s->lvlstamp[w->lvl] < s->stamp || !redundant(s, r))){
 350                                 w->stamp = s->stamp + 2;
 351                                 return 0;
 352                         }
 353                 }
 354                 v->stamp = s->stamp + 1;
 355                 return 1;
 356         }
 357         if(v->reason == nil) return 0; /* decision literals are never redundant */
 358         c = v->reason;
 359         for(i = 0; i < c->n; i++){
 360                 if(c->l[i] == NOT(l)) continue;
 361                 w = &s->var[VAR(c->l[i])];
 362                 if(w->lvl == 0)
 363                         continue; /* literals at level 0 are redundant */
 364                 if(w->stamp == s->stamp + 2)
 365                         return 0;
 366                 /* if the literal is not in the clause or known redundant, check if it is redundant */
 367                 /* we can skip the check if the level is not stamped: */
 368                 /* if there are no literals at the same level in the clause, it must be nonredundant */
 369                 if(w->stamp < s->stamp && (s->lvlstamp[w->lvl] < s->stamp || !redundant(s, c->l[i]))){
 370                         w->stamp = s->stamp + 2;
 371                         return 0;
 372                 }
 373         }
 374         v->stamp = s->stamp + 1;
 375         return 1;
 376 }
 377
 378 /* "blitting" a literal means to either add it to the conflict clause
 379  * (if v->lvl < s->lvl) or to increment the counter of literals to be
 380  * resolved, plus some bookkeeping.  */
 381 static void
 382 blit(SATSolve *s, int l)
 383 {
 384         SATVar *v;
 385         int p;
 386
 387         v = &s->var[VAR(l)];
 388         if(v->stamp == s->stamp) return;
 389         v->stamp = s->stamp;
 390         p = v->lvl;
 391         if(p == 0) return;
 392         if(verboseconflict) print("stamp %d %s (ctr=%d)\n", signf(l), p == s->lvl ? "and increment" : "and collect", s->cflctr);
 393         varbump(s, v);
 394         if(p == s->lvl){
 395                 s->cflctr++;
 396                 return;
 397         }
 398         if(s->ncflcl >= s->cflclalloc){
 399                 s->cflcl = satrealloc(s, s->cflcl, (s->cflclalloc + CFLCLALLOC) * sizeof(int));
 400                 s->cflclalloc += CFLCLALLOC;
 401         }
 402         s->cflcl[s->ncflcl++] = l;
 403         if(p > s->cfllvl) s->cfllvl = p;
 404         /* lvlstamp[p] == stamp if there is exactly one literal and ==stamp+1 if there is more than one literal on level p */
 405         if(s->lvlstamp[p] <= s->stamp)
 406                 s->lvlstamp[p] = s->stamp + (s->lvlstamp[p] == s->stamp);
 407 }
 408
 409 /* to resolve a conflict, we start with the conflict clause and use
 410  * resolution (a ∨ b and ¬a ∨ c imply b ∨ c) with the reasons for the
 411  * literals to remove all but one literal at the current level.  this
 412  * gives a new "learned" clause with all literals false and we jump back
 413  * to the second-highest level in it.  at this point, the clause implies
 414  * the one remaining literal and we can continue.
 415  * to do this quickly, rather than explicitly apply resolution, we keep a
 416  * counter of literals at the highest level (unresolved literals) and an
 417  * array with all other literals (which will become the learned clause). */
 418 static void
 419 conflict(SATSolve *s, SATClause *c, uvlong bin, int full)
 420 {
 421         int i, j, l, p, *nl, found;
 422         SATVar *v;
 423         SATClause *r;
 424
 425         if(verboseconflict) satprintstate(s);
 426         /* choose a new unique stamp value */
 427         if(s->stamp >= (uint)-3)
 428                 stampoverflow(s);
 429         s->stamp += 3;
 430         s->ncflcl = 1;
 431         s->cflctr = 0;
 432         s->cfllvl = 0;
 433         /* we start by blitting each literal in the conflict clause */
 434         if(c != nil){
 435                 clausebump(s, c);
 436                 for(i = 0; i < c->n; i++)
 437                         blit(s, c->l[i]);
 438                 /* if there is only one literal l at the current level, we should have inferred ¬l at a lower level (bug). */
 439                 if(s->cflctr <= 1){
 440                         satprintstate(s);
 441                         print("conflict clause %+Γ\n", c);
 442                         assert(s->cflctr > 1);
 443                 }
 444         }else{
 445                 blit(s, bin);
 446                 blit(s, bin>>32);
 447                 if(s->cflctr <= 1){
 448                         satprintstate(s);
 449                         print("binary conflict clause %d ∨ %d\n", (int)(bin>>32), (int)bin);
 450                         assert(s->cflctr > 1);
 451                 }
 452         }
 453         /* now we go backwards through the trail, decrementing the unresolved literal counter at each stamped literal */
 454         /* and blitting the literals in their reason */
 455         for(i = s->ntrail; --i >= 0; ){
 456                 v = &s->var[VAR(s->trail[i])];
 457                 if(v->stamp != s->stamp) continue;
 458                 if(verboseconflict) print("trail literal %d\n", signf(s->trail[i]));
 459                 if(--s->cflctr == 0) break;
 460                 if(v->isbinreason)
 461                         blit(s, v->binreason);
 462                 else if((r = v->reason) != nil){
 463                         clausebump(s, r);
 464                         for(j = 0; j < r->n; j++)
 465                                 blit(s, r->l[j]);
 466                 }
 467         }
 468         /* i should point to the one remaining literal at the current level */
 469         assert(i >= 0);
 470         nl = s->cflcl;
 471         nl[0] = NOT(s->trail[i]);
 472         found = 0;
 473         /* delete redundant literals. note we must watch a literal at cfllvl, so put it in l[1]. */
 474         for(i = 1, j = 1; i < s->ncflcl; i++){
 475                 l = nl[i];
 476                 p = s->var[VAR(nl[i])].lvl;
 477                 /* lvlstamp[p] != s->stamp + 1 => only one literal at level p => must be nonredundant */
 478                 if(s->lvlstamp[p] != s->stamp + 1 || !redundant(s, l))
 479                         if(found || p < s->cfllvl)
 480                                 nl[j++] = nl[i];
 481                         else{
 482                                 /* watch this literal */
 483                                 l = nl[i], nl[j++] = nl[1], nl[1] = l;
 484                                 found = 1;
 485                         }
 486         }
 487         s->ncflcl = j;
 488         if(!full){
 489                 /* normal mode: jump back and add to trail right away */
 490                 satbackjump(s, s->cfllvl);
 491                 sataddtrail(s, nl[0]);
 492         }else{
 493                 /* purging: record minimum cfllvl and literals at that level */
 494                 if(s->cfllvl < s->fullrlvl){
 495                         s->fullrlvl = s->cfllvl;
 496                         s->nfullrlits = 0;
 497                 }
 498                 s->fullrlits[s->nfullrlits++] = nl[0];
 499         }
 500         r = learn(s, full);
 501         if(!full && r != nil)
 502                 s->var[VAR(nl[0])].reason = r;
 503         if(verboseconflict)
 504                 if(r != nil)
 505                         print("learned %+Γ\n", r);
 506                 else
 507                         print("learned %d\n", signf(nl[0]));
 508         s->Δactivity *= s->varρ;
 509         s->Δclactivity *= s->clauseρ;
 510         s->conflicts++;
 511 }
 512
 513 /* to purge, we need a fullrun that assigns values to all variables.
 514  * during this we record the first conflict at each level, to be resolved
 515  * later.  otherwise this is just a copy of the main loop which never
 516  * purges or flushes. */
 517 static int
 518 fullrun(SATSolve *s)
 519 {
 520         int l;
 521         uvlong b;
 522         SATClause *c;
 523
 524         while(s->ntrail < s->nvar){
 525                 decision(s);
 526         re:
 527                 while(s->binptr < s->ntrail){
 528                         l = s->trail[s->binptr++];
 529                         b = binforcing(s, l, 1);
 530                         if(b != 0){
 531                                 if(s->lvl == 0){
 532                                         s->unsat = 1;
 533                                         return -1;
 534                                 }
 535                                 if(s->nfullrcfl == 0 || s->lvl > CFLLVL(s->fullrcfl[s->nfullrcfl-1])){
 536                                         s->fullrcfl = satrealloc(s, s->fullrcfl, sizeof(SATConflict) * (s->nfullrcfl + 1));
 537                                         s->fullrcfl[s->nfullrcfl].lvl = 1<<31 | s->lvl;
 538                                         s->fullrcfl[s->nfullrcfl++].b = b;
 539                                 }
 540                         }
 541                         sanity(s);
 542                 }
 543                 while(s->forptr < s->ntrail){
 544                         l = s->trail[s->forptr++];
 545                         c = forcing(s, NOT(l), 1);
 546                         if(c != nil){
 547                                 if(s->lvl == 0){
 548                                         s->unsat = 1;
 549                                         return -1;
 550                                 }
 551                                 if(s->nfullrcfl == 0 || s->lvl > CFLLVL(s->fullrcfl[s->nfullrcfl-1])){
 552                                         s->fullrcfl = satrealloc(s, s->fullrcfl, sizeof(SATConflict) * (s->nfullrcfl + 1));
 553                                         s->fullrcfl[s->nfullrcfl].lvl = s->lvl;
 554                                         s->fullrcfl[s->nfullrcfl++].c = c;
 555                                 }
 556                         }
 557                 }
 558                 if(s->binptr < s->ntrail) goto re;
 559         }
 560         return 0;
 561 }
 562
 563 /* assign range scores to all clauses.
 564  * p == number of levels that have positive literals in the clause.
 565  * r == number of levels that have literals in the clause.
 566  * range == min(floor(16 * (p + α (r - p))), 255) with magic constant α. */
 567 static void
 568 ranges(SATSolve *s)
 569 {
 570         SATClause *c;
 571         int p, r, k, l, v;
 572         uint ci;
 573
 574         ci = 2;
 575         memset(s->lvlstamp, 0, sizeof(int) * s->nvar);
 576         memset(s->rangecnt, 0, sizeof(s->rangecnt));
 577         for(c = s->learncl; c != nil; c = c->next, ci += 2){
 578                 if(!s->var[VAR(c->l[0])].binreason && s->var[VAR(c->l[0])].reason == c){
 579                         c->range = 0;
 580                         s->rangecnt[0]++;
 581                         continue;
 582                 }
 583                 p = 0;
 584                 r = 0;
 585                 for(k = 0; k < c->n; k++){
 586                         l = c->l[k];
 587                         v = s->var[VAR(l)].lvl;
 588                         if(v == 0){
 589                                 if(s->lit[l].val == 1){
 590                                         c->range = 256;
 591                                         goto next;
 592                                 }
 593                         }else{
 594                                 if(s->lvlstamp[v] < ci){
 595                                         s->lvlstamp[v] = ci;
 596                                         r++;
 597                                 }
 598                                 if(s->lvlstamp[v] == ci && s->lit[l].val == 1){
 599                                         s->lvlstamp[v] = ci + 1;
 600                                         p++;
 601                                 }
 602                         }
 603                 }
 604                 r = 16 * (p + s->purgeα * (r - p));
 605                 if(r > 255) r = 255;
 606                 c->range = r;
 607                 s->rangecnt[r]++;
 608         next: ;
 609         }
 610 }
 611
 612 /* resolve conflicts found during fullrun() */
 613 static void
 614 fullrconflicts(SATSolve *s)
 615 {
 616         SATConflict *cfl;
 617         int i;
 618
 619         s->fullrlvl = s->lvl;
 620         s->nfullrlits = 0;
 621         for(cfl = &s->fullrcfl[s->nfullrcfl - 1]; cfl >= s->fullrcfl; cfl--){
 622                 satbackjump(s, CFLLVL(*cfl));
 623                 if(cfl->lvl < 0)
 624                         conflict(s, nil, cfl->b, 1);
 625                 else
 626                         conflict(s, cfl->c, 0, 1);
 627         }
 628         satbackjump(s, 0);
 629         if(s->fullrlvl == 0)
 630                 for(i = 0; i < s->nfullrlits; i++)
 631                         sataddtrail(s, s->fullrlits[i]);
 632         free(s->fullrcfl);
 633         s->fullrcfl = nil;
 634 }
 635
 636 /* note that nil > *, this simplifies the algorithm by having nil "bubble" to the top */
 637 static int
 638 actgt(SATClause *a, SATClause *b)
 639 {
 640         if(b == nil) return 0;
 641         if(a == nil) return 1;
 642         return a->activity > b->activity || a->activity == b->activity && a > b;
 643 }
 644
 645 /* select n clauses to keep
 646  * first we find the upper limit j on the range score
 647  * to get the exact number, we move htot clauses from j to j+1
 648  * to this end, we put them in a max-heap of size htot, sorted by activity,
 649  * continually replacing the largest element if we find a less active clause.
 650  * the heap starts out filled with nil and the nil are replaced during the first
 651  * htot iterations. */
 652 #define LEFT(i) (2*(i)+1)
 653 #define RIGHT(i) (2*(i)+2)
 654 static int
 655 judgement(SATSolve *s, int n)
 656 {
 657         int cnt, i, j, htot, m;
 658         SATClause *c, **h, *z;
 659
 660         cnt = 0;
 661         for(j = 0; j < 256; j++){
 662                 cnt += s->rangecnt[j];
 663                 if(cnt >= n) break;
 664         }
 665         if(j == 256) return j;
 666         if(cnt > n){
 667                 htot = cnt - n;
 668                 h = satrealloc(s, nil, sizeof(SATClause *) * htot);
 669                 memset(h, 0, sizeof(SATClause *) * htot);
 670                 for(c = s->learncl; c != nil; c = c->next){
 671                         if(c->range != j || actgt(c, h[0])) continue;
 672                         h[0] = c;
 673                         m = 0;
 674                         for(;;){
 675                                 i = m;
 676                                 if(LEFT(i) < htot && actgt(h[LEFT(i)], h[m])) m = LEFT(i);
 677                                 if(RIGHT(i) < htot && actgt(h[RIGHT(i)], h[m])) m = RIGHT(i);
 678                                 if(i == m) break;
 679                                 z = h[i], h[i] = h[m], h[m] = z;
 680                         }
 681                 }
 682                 for(i = 0; i < htot; i++)
 683                         if(h[i] != nil)
 684                                 h[i]->range = j + 1;
 685                 free(h);
 686         }
 687         return j;
 688 }
 689
 690 /* during purging we remove permanently false literals from learned clauses.
 691  * returns 1 if the clause can be deleted entirely. */
 692 static int
 693 cleanupclause(SATSolve *s, SATClause *c)
 694 {
 695         int i, k;
 696
 697         for(i = 0; i < c->n; i++)
 698                 if(s->lit[c->l[i]].val == 0)
 699                         break;
 700         if(i == c->n) return 0;
 701         for(k = i; i < c->n; i++)
 702                 if(s->lit[c->l[i]].val != 0)
 703                         c->l[k++] = c->l[i];
 704         c->n = k;
 705         if(k > 1) return 0;
 706         if(k == 0)
 707                 s->unsat = 1;
 708         else if(s->lit[c->l[0]].val < 0)
 709                 sataddtrail(s, c->l[0]);
 710         return 1;
 711 }
 712
 713 /* delete clauses by overwriting them. don't delete empty blocks; we're going to fill them up soon enough again. */
 714 static void
 715 execution(SATSolve *s, int j)
 716 {
 717         SATClause *c, *n, **cp, *p;
 718         SATBlock *b;
 719         SATVar *v0;
 720         int f, sz;
 721
 722         b = s->bl[1].next;
 723         p = (SATClause*) b->data;
 724         s->ncl = s->ncl0;
 725         cp = &s->learncl;
 726         for(c = p; c != nil; c = n){
 727                 n = c->next;
 728                 if(c->range > j || cleanupclause(s, c))
 729                         continue;
 730                 sz = sizeof(SATClause) + (c->n - 1) * sizeof(int);
 731                 f = (uchar*)b + SATBLOCKSZ - (uchar*)p;
 732                 if(f < sz){
 733                         memset(p, 0, f);
 734                         b = b->next;
 735                         assert(b != &s->bl[1]);
 736                         p = (SATClause *) b->data;
 737                 }
 738                 b->last = p;
 739                 /* update reason field of the first variable (if applicable) */
 740                 v0 = &s->var[VAR(c->l[0])];
 741                 if(!v0->isbinreason && v0->reason == c)
 742                         v0->reason = p;
 743                 memmove(p, c, sz);
 744                 *cp = p;
 745                 cp = &p->next;
 746                 p = (void*)((uintptr)p + sz + CLAUSEALIGN - 1 & -CLAUSEALIGN);
 747                 b->end = p;
 748                 s->ncl++;
 749         }
 750         *cp = nil;
 751         *s->lastp[0] = s->learncl;
 752         s->lastp[1] = cp;
 753         s->lastbl = b;
 754         f = (uchar*)b + SATBLOCKSZ - (uchar*)p;
 755         memset(p, 0, f);
 756         for(b = b->next; b != &s->bl[1]; b = b->next){
 757                 b->last = nil;
 758                 b->end = b->data;
 759         }
 760 }
 761
 762 static void
 763 thepurge(SATSolve *s)
 764 {
 765         int nkeep, i, j;
 766         SATVar *v;
 767
 768         s->purgeival += s->purgeδ;
 769         s->nextpurge = s->conflicts + s->purgeival;
 770         nkeep = (s->ncl - s->ncl0) / 2;
 771         for(i = 0; i < s->ntrail; i++){
 772                 v = &s->var[VAR(s->trail[i])];
 773                 if(!v->isbinreason && v->reason != nil)
 774                         nkeep++;
 775         }
 776         if(nkeep <= 0) return; /* shouldn't happen */
 777         s->nfullrcfl = 0;
 778         if(fullrun(s) < 0){ /* accidentally determined UNSAT during fullrun() */
 779                 free(s->fullrcfl);
 780                 s->fullrcfl = nil;
 781                 return;
 782         }
 783         ranges(s);
 784         fullrconflicts(s);
 785         j = judgement(s, nkeep);
 786         execution(s, j);
 787         rewatch(s);
 788 }
 789
 790 /* to avoid getting stuck, flushing backs up the trail to remove low activity variables.
 791  * don't worry about throwing out high activity ones, they'll get readded quickly. */
 792 static void
 793 theflush(SATSolve *s)
 794 {
 795         double actk;
 796         int dd, l;
 797
 798         /* "reluctant doubling" wizardry to determine when to flush */
 799         if((s->flushu & -s->flushu) == s->flushv){
 800                 s->flushu++;
 801                 s->flushv = 1;
 802                 s->flushθ = s->flushψ;
 803         }else{
 804                 s->flushv *= 2;
 805                 s->flushθ += s->flushθ >> 4;
 806         }
 807         s->nextflush = s->conflicts + s->flushv;
 808         if(s->agility > s->flushθ) return; /* don't flush when we're too busy */
 809         /* clean up the heap so that a free variable is at the top */
 810         while(s->nheap > 0 && s->heap[0]->lvl >= 0)
 811                 satheaptake(s);
 812         if(s->nheap == 0) return; /* shouldn't happen */
 813         actk = s->heap[0]->activity;
 814         for(dd = 0; dd < s->lvl; dd++){
 815                 l = s->trail[s->decbd[dd+1]];
 816                 if(s->var[VAR(l)].activity < actk)
 817                         break;
 818         }
 819         satbackjump(s, dd);
 820 }
 821
 822 int
 823 satsolve(SATSolve *s)
 824 {
 825         int l;
 826         SATClause *c;
 827         uvlong b;
 828
 829         if(s == nil) return 1;
 830         if(s->scratched) return -1;
 831         if(s->nvar == 0) return 1;
 832         solvinit(s);
 833
 834         while(!s->unsat){
 835         re:
 836                 while(s->binptr < s->ntrail){
 837                         l = s->trail[s->binptr++];
 838                         b = binforcing(s, l, 0);
 839                         sanity(s);
 840                         if(b != 0){
 841                                 if(s->lvl == 0) goto unsat;
 842                                 conflict(s, nil, b, 0);
 843                                 sanity(s);
 844                         }
 845                 }
 846                 while(s->forptr < s->ntrail){
 847                         l = s->trail[s->forptr++];
 848                         c = forcing(s, NOT(l), 0);
 849                         sanity(s);
 850                         if(c != nil){
 851                                 if(s->lvl == 0) goto unsat;
 852                                 conflict(s, c, 0, 0);
 853                                 sanity(s);
 854                         }
 855                 }
 856                 if(s->binptr < s->ntrail) goto re;
 857                 if(s->ntrail == s->nvar) goto out;
 858                 if(s->conflicts >= s->nextpurge)
 859                         thepurge(s);
 860                 else if(s->conflicts >= s->nextflush)
 861                         theflush(s);
 862                 else
 863                         decision(s);
 864         }
 865 unsat:
 866         s->unsat = 1;
 867 out:
 868         satcleanup(s, 0);
 869         return !s->unsat;
 870 }
 871
 872 void
 873 satreset(SATSolve *s)
 874 {
 875         int i;
 876
 877         if(s == nil || s->decbd == nil) return;
 878         satbackjump(s, -1);
 879         s->lvl = 0;
 880         for(i = 0; i < s->nvar; i++){
 881                 s->var[i].activity = 0;
 882                 s->var[i].flags |= VARPHASE;
 883         }
 884         satcleanup(s, 1);
 885         s->Δactivity = 1;
 886         s->Δclactivity = 1;
 887 }