6 /* the solver follows Algorithm C from Knuth's The Art of Computer Programming, Vol. 4, Fascicle 6 */
9 #define verboseforcing 0
10 #define verboseconflict 0
12 #define sanity(s) if(paranoia) satsanity(s)
15 sataddtrail(SATSolve *s, int l)
17 s->trail[s->ntrail++] = l;
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)
24 if(verbosestate) satprintstate(s);
27 /* compute watchlists from scratch */
35 for(l = s->lit; l < s->lit + 2*s->nvar; l++)
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;
45 c->watch[i] = s->lit[c->l[i]].watch;
46 s->lit[c->l[i]].watch = c;
50 /* jump back to decision level d */
52 satbackjump(SATSolve *s, int d)
57 if(s->lvl == d) return;
58 while(s->ntrail > s->decbd[d + 1]){
59 l = s->trail[--s->ntrail];
61 if((v->flags & VARUSER) != 0){ /* don't delete user assignments */
66 s->lit[NOT(l)].val = -1;
67 v->flags = v->flags & ~1 | l & 1;
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);
85 s->decbd = satrealloc(s, s->decbd, (s->nvar + 1) * sizeof(int));
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;
98 s->nextpurge = s->purgeΔ;
99 s->purgeival = s->purgeΔ;
103 s->flushθ = s->flushψ;
112 satcleanup(SATSolve *s, int all)
119 s->lastp[1] = &s->learncl;
122 for(b = s->bl[1].next; b != &s->bl[1]; b = bn){
124 if(b->last != nil && !all) continue;
125 b->next->prev = b->prev;
126 b->prev->next = b->next;
129 s->lastbl = s->bl[1].prev;
140 stampoverflow(SATSolve *s)
144 for(i = 0; i < s->nvar; i++){
151 /* "bump" the variable, i.e. increase its activity score. reduce all score when one exceeds MAXACTIVITY (1e100) */
153 varbump(SATSolve *s, SATVar *v)
155 v->activity += s->Δactivity;
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;
164 s->Δactivity /= MAXACTIVITY;
167 /* ditto for clauses */
169 clausebump(SATSolve *s, SATClause *c)
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;
179 s->Δclactivity /= MAXACTIVITY;
182 /* pick a literal. normally we pick the variable with highest activity from the heap. sometimes we goof and pick a random one. */
184 decision(SATSolve *s)
188 s->decbd[++s->lvl] = s->ntrail;
189 if((uint)s->randfn(s->randaux) < s->goofprob){
190 v = s->heap[satnrand(s, s->nheap)];
198 sataddtrail(s, 2 * (v - s->var) + (v->flags & VARPHASE));
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 */
204 forcing(SATSolve *s, int l, int full)
206 SATClause **cp, *rc, *c, *xp;
210 cp = &s->lit[l].watch;
212 if(verboseforcing) print("forcing literal %d\n", signf(l));
213 while(c = *cp, c != nil){
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;
219 assert(c->l[1] == l);
220 v0 = s->lit[c->l[0]].val;
221 if(v0 > 0) /* the clause is true anyway */
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]));
228 x = c->l[j], c->l[j] = c->l[1], c->l[1] = x;
229 c->watch[1] = s->lit[x].watch;
236 if(rc == nil) rc = c;
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;
249 /* forcing() for binary implications */
251 binforcing(SATSolve *s, int l, int full)
259 if(verboseforcing && lp->nbimp > 0) print("forcing literal %d (binary)\n", signf(l));
260 for(i = 0; i < lp->nbimp; i++){
262 switch(s->lit[m].val){
264 if(verboseforcing) print("inferring %d using binary clause (%d) ∨ %d\n", signf(m), -signf(l), signf(m));
266 s->var[VAR(m)].binreason = NOT(l);
267 s->var[VAR(m)].isbinreason = 1;
270 if(verboseforcing) print("conflict (%d) ∨ (%d)\n", -signf(l), signf(m));
271 if(rc == 0) rc = (uvlong)NOT(l) << 32 | (uint)m;
279 /* check if we can discard the previously learned clause because the current one subsumes it */
281 checkdiscard(SATSolve *s)
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 */
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)
300 /* add the clause we just learned to our collection */
302 learn(SATSolve *s, int notriv)
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;
314 if(s->ncflcl == 1) /* unit clauses are handled by putting them on the trail in conflict() */
316 if(!triv && checkdiscard(s))
317 r = satreplclause(s, s->ncflcl);
319 r = satnewclause(s, s->ncflcl, 1);
321 memcpy(r->l, s->cflcl, s->ncflcl * sizeof(int));
322 for(i = 0; i < 2; i++){
324 r->watch[i] = s->lit[l].watch;
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.
335 redundant(SATSolve *s, int l)
343 /* stupid special case code */
347 if(w->stamp == s->stamp + 2)
349 if(w->stamp < s->stamp && (s->lvlstamp[w->lvl] < s->stamp || !redundant(s, r))){
350 w->stamp = s->stamp + 2;
354 v->stamp = s->stamp + 1;
357 if(v->reason == nil) return 0; /* decision literals are never redundant */
359 for(i = 0; i < c->n; i++){
360 if(c->l[i] == NOT(l)) continue;
361 w = &s->var[VAR(c->l[i])];
363 continue; /* literals at level 0 are redundant */
364 if(w->stamp == s->stamp + 2)
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;
374 v->stamp = s->stamp + 1;
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. */
382 blit(SATSolve *s, int l)
388 if(v->stamp == s->stamp) return;
392 if(verboseconflict) print("stamp %d %s (ctr=%d)\n", signf(l), p == s->lvl ? "and increment" : "and collect", s->cflctr);
398 if(s->ncflcl >= s->cflclalloc){
399 s->cflcl = satrealloc(s, s->cflcl, (s->cflclalloc + CFLCLALLOC) * sizeof(int));
400 s->cflclalloc += CFLCLALLOC;
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);
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). */
419 conflict(SATSolve *s, SATClause *c, uvlong bin, int full)
421 int i, j, l, p, *nl, found;
425 if(verboseconflict) satprintstate(s);
426 /* choose a new unique stamp value */
427 if(s->stamp >= (uint)-3)
433 /* we start by blitting each literal in the conflict clause */
436 for(i = 0; i < c->n; i++)
438 /* if there is only one literal l at the current level, we should have inferred ¬l at a lower level (bug). */
441 print("conflict clause %+Γ\n", c);
442 assert(s->cflctr > 1);
449 print("binary conflict clause %d ∨ %d\n", (int)(bin>>32), (int)bin);
450 assert(s->cflctr > 1);
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;
461 blit(s, v->binreason);
462 else if((r = v->reason) != nil){
464 for(j = 0; j < r->n; j++)
468 /* i should point to the one remaining literal at the current level */
471 nl[0] = NOT(s->trail[i]);
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++){
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)
482 /* watch this literal */
483 l = nl[i], nl[j++] = nl[1], nl[1] = l;
489 /* normal mode: jump back and add to trail right away */
490 satbackjump(s, s->cfllvl);
491 sataddtrail(s, nl[0]);
493 /* purging: record minimum cfllvl and literals at that level */
494 if(s->cfllvl < s->fullrlvl){
495 s->fullrlvl = s->cfllvl;
498 s->fullrlits[s->nfullrlits++] = nl[0];
501 if(!full && r != nil)
502 s->var[VAR(nl[0])].reason = r;
505 print("learned %+Γ\n", r);
507 print("learned %d\n", signf(nl[0]));
508 s->Δactivity *= s->varρ;
509 s->Δclactivity *= s->clauseρ;
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. */
524 while(s->ntrail < s->nvar){
527 while(s->binptr < s->ntrail){
528 l = s->trail[s->binptr++];
529 b = binforcing(s, l, 1);
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;
543 while(s->forptr < s->ntrail){
544 l = s->trail[s->forptr++];
545 c = forcing(s, NOT(l), 1);
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;
558 if(s->binptr < s->ntrail) goto re;
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 α. */
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){
585 for(k = 0; k < c->n; k++){
587 v = s->var[VAR(l)].lvl;
589 if(s->lit[l].val == 1){
594 if(s->lvlstamp[v] < ci){
598 if(s->lvlstamp[v] == ci && s->lit[l].val == 1){
599 s->lvlstamp[v] = ci + 1;
604 r = 16 * (p + s->purgeα * (r - p));
612 /* resolve conflicts found during fullrun() */
614 fullrconflicts(SATSolve *s)
619 s->fullrlvl = s->lvl;
621 for(cfl = &s->fullrcfl[s->nfullrcfl - 1]; cfl >= s->fullrcfl; cfl--){
622 satbackjump(s, CFLLVL(*cfl));
624 conflict(s, nil, cfl->b, 1);
626 conflict(s, cfl->c, 0, 1);
630 for(i = 0; i < s->nfullrlits; i++)
631 sataddtrail(s, s->fullrlits[i]);
636 /* note that nil > *, this simplifies the algorithm by having nil "bubble" to the top */
638 actgt(SATClause *a, SATClause *b)
640 if(b == nil) return 0;
641 if(a == nil) return 1;
642 return a->activity > b->activity || a->activity == b->activity && a > b;
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)
655 judgement(SATSolve *s, int n)
657 int cnt, i, j, htot, m;
658 SATClause *c, **h, *z;
661 for(j = 0; j < 256; j++){
662 cnt += s->rangecnt[j];
665 if(j == 256) return j;
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;
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);
679 z = h[i], h[i] = h[m], h[m] = z;
682 for(i = 0; i < htot; i++)
690 /* during purging we remove permanently false literals from learned clauses.
691 * returns 1 if the clause can be deleted entirely. */
693 cleanupclause(SATSolve *s, SATClause *c)
697 for(i = 0; i < c->n; i++)
698 if(s->lit[c->l[i]].val == 0)
700 if(i == c->n) return 0;
701 for(k = i; i < c->n; i++)
702 if(s->lit[c->l[i]].val != 0)
708 else if(s->lit[c->l[0]].val < 0)
709 sataddtrail(s, c->l[0]);
713 /* delete clauses by overwriting them. don't delete empty blocks; we're going to fill them up soon enough again. */
715 execution(SATSolve *s, int j)
717 SATClause *c, *n, **cp, *p;
723 p = (SATClause*) b->data;
726 for(c = p; c != nil; c = n){
728 if(c->range > j || cleanupclause(s, c))
730 sz = sizeof(SATClause) + (c->n - 1) * sizeof(int);
731 f = (uchar*)b + SATBLOCKSZ - (uchar*)p;
735 assert(b != &s->bl[1]);
736 p = (SATClause *) b->data;
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)
746 p = (void*)((uintptr)p + sz + CLAUSEALIGN - 1 & -CLAUSEALIGN);
751 *s->lastp[0] = s->learncl;
754 f = (uchar*)b + SATBLOCKSZ - (uchar*)p;
756 for(b = b->next; b != &s->bl[1]; b = b->next){
763 thepurge(SATSolve *s)
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)
776 if(nkeep <= 0) return; /* shouldn't happen */
778 if(fullrun(s) < 0){ /* accidentally determined UNSAT during fullrun() */
785 j = judgement(s, nkeep);
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. */
793 theflush(SATSolve *s)
798 /* "reluctant doubling" wizardry to determine when to flush */
799 if((s->flushu & -s->flushu) == s->flushv){
802 s->flushθ = s->flushψ;
805 s->flushθ += s->flushθ >> 4;
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)
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)
823 satsolve(SATSolve *s)
829 if(s == nil) return 1;
830 if(s->scratched) return -1;
831 if(s->nvar == 0) return 1;
836 while(s->binptr < s->ntrail){
837 l = s->trail[s->binptr++];
838 b = binforcing(s, l, 0);
841 if(s->lvl == 0) goto unsat;
842 conflict(s, nil, b, 0);
846 while(s->forptr < s->ntrail){
847 l = s->trail[s->forptr++];
848 c = forcing(s, NOT(l), 0);
851 if(s->lvl == 0) goto unsat;
852 conflict(s, c, 0, 0);
856 if(s->binptr < s->ntrail) goto re;
857 if(s->ntrail == s->nvar) goto out;
858 if(s->conflicts >= s->nextpurge)
860 else if(s->conflicts >= s->nextflush)
873 satreset(SATSolve *s)
877 if(s == nil || s->decbd == nil) return;
880 for(i = 0; i < s->nvar; i++){
881 s->var[i].activity = 0;
882 s->var[i].flags |= VARPHASE;