1 /* minisat.c */
2
3 /* Modified by Andrew Makhorin <mao@gnu.org>, August 2011 */
4 /* May 2017: Changes were made to provide 64-bit portability; thanks to
5 * Chris Matrakidis <cmatraki@gmail.com> for patch */
6
7 /***********************************************************************
8 * MiniSat -- Copyright (c) 2005, Niklas Sorensson
9 * http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
10 *
11 * Permission is hereby granted, free of charge, to any person
12 * obtaining a copy of this software and associated documentation files
13 * (the "Software"), to deal in the Software without restriction,
14 * including without limitation the rights to use, copy, modify, merge,
15 * publish, distribute, sublicense, and/or sell copies of the Software,
16 * and to permit persons to whom the Software is furnished to do so,
17 * subject to the following conditions:
18 *
19 * The above copyright notice and this permission notice shall be
20 * included in all copies or substantial portions of the Software.
21 *
22 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
23 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
24 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
25 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
26 * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
27 * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
28 * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
29 * SOFTWARE.
30 ***********************************************************************/
31 /* Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko */
32
33 #include "env.h"
34 #include "minisat.h"
35
36 #if 1 /* by mao */
ymalloc(int size)37 static void *ymalloc(int size)
38 { void *ptr;
39 xassert(size > 0);
40 ptr = malloc(size);
41 if (ptr == NULL)
42 xerror("MiniSat: no memory available\n");
43 return ptr;
44 }
45
yrealloc(void * ptr,int size)46 static void *yrealloc(void *ptr, int size)
47 { xassert(size > 0);
48 if (ptr == NULL)
49 ptr = malloc(size);
50 else
51 ptr = realloc(ptr, size);
52 if (ptr == NULL)
53 xerror("MiniSat: no memory available\n");
54 return ptr;
55 }
56
yfree(void * ptr)57 static void yfree(void *ptr)
58 { xassert(ptr != NULL);
59 free(ptr);
60 return;
61 }
62
63 #define assert xassert
64 #define printf xprintf
65 #define fflush(f) /* nop */
66 #define malloc ymalloc
67 #define realloc yrealloc
68 #define free yfree
69 #define inline /* empty */
70 #endif
71
72 /*====================================================================*/
73 /* Debug: */
74
75 #if 0
76 #define VERBOSEDEBUG 1
77 #endif
78
79 /* For derivation output (verbosity level 2) */
80 #define L_IND "%-*d"
81 #define L_ind solver_dlevel(s)*3+3,solver_dlevel(s)
82 #define L_LIT "%sx%d"
83 #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
84
85 #if 0 /* by mao */
86 /* Just like 'assert()' but expression will be evaluated in the release
87 version as well. */
88 static inline void check(int expr) { assert(expr); }
89 #endif
90
91 #if 0 /* by mao */
92 static void printlits(lit* begin, lit* end)
93 {
94 int i;
95 for (i = 0; i < end - begin; i++)
96 printf(L_LIT" ",L_lit(begin[i]));
97 }
98 #endif
99
100 /*====================================================================*/
101 /* Random numbers: */
102
103 /* Returns a random float 0 <= x < 1. Seed must never be 0. */
drand(double * seed)104 static inline double drand(double* seed) {
105 int q;
106 *seed *= 1389796;
107 q = (int)(*seed / 2147483647);
108 *seed -= (double)q * 2147483647;
109 return *seed / 2147483647; }
110
111 /* Returns a random integer 0 <= x < size. Seed must never be 0. */
irand(double * seed,int size)112 static inline int irand(double* seed, int size) {
113 return (int)(drand(seed) * size); }
114
115 /*====================================================================*/
116 /* Predeclarations: */
117
118 static void sort(void** array, int size,
119 int(*comp)(const void *, const void *));
120
121 /*====================================================================*/
122 /* Clause datatype + minor functions: */
123
124 #if 0 /* by mao; see minisat.h */
125 struct clause_t
126 {
127 int size_learnt;
128 lit lits[0];
129 };
130 #endif
131
132 #define clause_size(c) ((c)->size_learnt >> 1)
133
134 #define clause_begin(c) ((c)->lits)
135
136 #define clause_learnt(c) ((c)->size_learnt & 1)
137
138 #define clause_activity(c) \
139 (*((float*)&(c)->lits[(c)->size_learnt>>1]))
140
141 #define clause_setactivity(c, a) \
142 (void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a))
143
144 /*====================================================================*/
145 /* Encode literals in clause pointers: */
146
147 #if 0 /* 8/I-2017 by cmatraki (64-bit portability) */
148 #define clause_from_lit(l) \
149 (clause*)((unsigned long)(l) + (unsigned long)(l) + 1)
150
151 #define clause_is_lit(c) \
152 ((unsigned long)(c) & 1)
153
154 #define clause_read_lit(c) \
155 (lit)((unsigned long)(c) >> 1)
156 #else
157 #define clause_from_lit(l) \
158 (clause*)((size_t)(l) + (size_t)(l) + 1)
159
160 #define clause_is_lit(c) \
161 ((size_t)(c) & 1)
162
163 #define clause_read_lit(c) \
164 (lit)((size_t)(c) >> 1)
165 #endif
166
167 /*====================================================================*/
168 /* Simple helpers: */
169
170 #define solver_dlevel(s) \
171 (int)veci_size(&(s)->trail_lim)
172
173 #define solver_read_wlist(s, l) \
174 (vecp *)(&(s)->wlists[l])
175
vecp_remove(vecp * v,void * e)176 static inline void vecp_remove(vecp* v, void* e)
177 {
178 void** ws = vecp_begin(v);
179 int j = 0;
180
181 for (; ws[j] != e ; j++);
182 assert(j < vecp_size(v));
183 for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
184 vecp_resize(v,vecp_size(v)-1);
185 }
186
187 /*====================================================================*/
188 /* Variable order functions: */
189
order_update(solver * s,int v)190 static inline void order_update(solver* s, int v)
191 { /* updateorder */
192 int* orderpos = s->orderpos;
193 double* activity = s->activity;
194 int* heap = veci_begin(&s->order);
195 int i = orderpos[v];
196 int x = heap[i];
197 int parent = (i - 1) / 2;
198
199 assert(s->orderpos[v] != -1);
200
201 while (i != 0 && activity[x] > activity[heap[parent]]){
202 heap[i] = heap[parent];
203 orderpos[heap[i]] = i;
204 i = parent;
205 parent = (i - 1) / 2;
206 }
207 heap[i] = x;
208 orderpos[x] = i;
209 }
210
211 #define order_assigned(s, v) /* nop */
212
order_unassigned(solver * s,int v)213 static inline void order_unassigned(solver* s, int v)
214 { /* undoorder */
215 int* orderpos = s->orderpos;
216 if (orderpos[v] == -1){
217 orderpos[v] = veci_size(&s->order);
218 veci_push(&s->order,v);
219 order_update(s,v);
220 }
221 }
222
order_select(solver * s,float random_var_freq)223 static int order_select(solver* s, float random_var_freq)
224 { /* selectvar */
225 int* heap;
226 double* activity;
227 int* orderpos;
228
229 lbool* values = s->assigns;
230
231 /* Random decision: */
232 if (drand(&s->random_seed) < random_var_freq){
233 int next = irand(&s->random_seed,s->size);
234 assert(next >= 0 && next < s->size);
235 if (values[next] == l_Undef)
236 return next;
237 }
238
239 /* Activity based decision: */
240
241 heap = veci_begin(&s->order);
242 activity = s->activity;
243 orderpos = s->orderpos;
244
245 while (veci_size(&s->order) > 0){
246 int next = heap[0];
247 int size = veci_size(&s->order)-1;
248 int x = heap[size];
249
250 veci_resize(&s->order,size);
251
252 orderpos[next] = -1;
253
254 if (size > 0){
255 double act = activity[x];
256
257 int i = 0;
258 int child = 1;
259
260 while (child < size){
261 if (child+1 < size
262 && activity[heap[child]] < activity[heap[child+1]])
263 child++;
264
265 assert(child < size);
266
267 if (act >= activity[heap[child]])
268 break;
269
270 heap[i] = heap[child];
271 orderpos[heap[i]] = i;
272 i = child;
273 child = 2 * child + 1;
274 }
275 heap[i] = x;
276 orderpos[heap[i]] = i;
277 }
278
279 if (values[next] == l_Undef)
280 return next;
281 }
282
283 return var_Undef;
284 }
285
286 /*====================================================================*/
287 /* Activity functions: */
288
act_var_rescale(solver * s)289 static inline void act_var_rescale(solver* s) {
290 double* activity = s->activity;
291 int i;
292 for (i = 0; i < s->size; i++)
293 activity[i] *= 1e-100;
294 s->var_inc *= 1e-100;
295 }
296
act_var_bump(solver * s,int v)297 static inline void act_var_bump(solver* s, int v) {
298 double* activity = s->activity;
299 if ((activity[v] += s->var_inc) > 1e100)
300 act_var_rescale(s);
301
302 /* printf("bump %d %f\n", v-1, activity[v]); */
303
304 if (s->orderpos[v] != -1)
305 order_update(s,v);
306
307 }
308
act_var_decay(solver * s)309 static inline void act_var_decay(solver* s)
310 { s->var_inc *= s->var_decay; }
311
act_clause_rescale(solver * s)312 static inline void act_clause_rescale(solver* s) {
313 clause** cs = (clause**)vecp_begin(&s->learnts);
314 int i;
315 for (i = 0; i < vecp_size(&s->learnts); i++){
316 float a = clause_activity(cs[i]);
317 clause_setactivity(cs[i], a * (float)1e-20);
318 }
319 s->cla_inc *= (float)1e-20;
320 }
321
act_clause_bump(solver * s,clause * c)322 static inline void act_clause_bump(solver* s, clause *c) {
323 float a = clause_activity(c) + s->cla_inc;
324 clause_setactivity(c,a);
325 if (a > 1e20) act_clause_rescale(s);
326 }
327
act_clause_decay(solver * s)328 static inline void act_clause_decay(solver* s)
329 { s->cla_inc *= s->cla_decay; }
330
331 /*====================================================================*/
332 /* Clause functions: */
333
334 /* pre: size > 1 && no variable occurs twice
335 */
clause_new(solver * s,lit * begin,lit * end,int learnt)336 static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
337 {
338 int size;
339 clause* c;
340 int i;
341
342 assert(end - begin > 1);
343 assert(learnt >= 0 && learnt < 2);
344 size = end - begin;
345 c = (clause*)malloc(sizeof(clause)
346 + sizeof(lit) * size + learnt * sizeof(float));
347 c->size_learnt = (size << 1) | learnt;
348 #if 1 /* by mao & cmatraki; non-portable check that is a fundamental \
349 * assumption of minisat code: bit 0 is used as a flag (zero \
350 * for pointer, one for shifted int) so allocated memory should \
351 * be at least 16-bit aligned */
352 assert(((size_t)c & 1) == 0);
353 #endif
354
355 for (i = 0; i < size; i++)
356 c->lits[i] = begin[i];
357
358 if (learnt)
359 *((float*)&c->lits[size]) = 0.0;
360
361 assert(begin[0] >= 0);
362 assert(begin[0] < s->size*2);
363 assert(begin[1] >= 0);
364 assert(begin[1] < s->size*2);
365
366 assert(lit_neg(begin[0]) < s->size*2);
367 assert(lit_neg(begin[1]) < s->size*2);
368
369 /* vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c); */
370 /* vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c); */
371
372 vecp_push(solver_read_wlist(s,lit_neg(begin[0])),
373 (void*)(size > 2 ? c : clause_from_lit(begin[1])));
374 vecp_push(solver_read_wlist(s,lit_neg(begin[1])),
375 (void*)(size > 2 ? c : clause_from_lit(begin[0])));
376
377 return c;
378 }
379
clause_remove(solver * s,clause * c)380 static void clause_remove(solver* s, clause* c)
381 {
382 lit* lits = clause_begin(c);
383 assert(lit_neg(lits[0]) < s->size*2);
384 assert(lit_neg(lits[1]) < s->size*2);
385
386 /* vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c); */
387 /* vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c); */
388
389 assert(lits[0] < s->size*2);
390 vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),
391 (void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
392 vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),
393 (void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
394
395 if (clause_learnt(c)){
396 s->stats.learnts--;
397 s->stats.learnts_literals -= clause_size(c);
398 }else{
399 s->stats.clauses--;
400 s->stats.clauses_literals -= clause_size(c);
401 }
402
403 free(c);
404 }
405
clause_simplify(solver * s,clause * c)406 static lbool clause_simplify(solver* s, clause* c)
407 {
408 lit* lits = clause_begin(c);
409 lbool* values = s->assigns;
410 int i;
411
412 assert(solver_dlevel(s) == 0);
413
414 for (i = 0; i < clause_size(c); i++){
415 lbool sig = !lit_sign(lits[i]); sig += sig - 1;
416 if (values[lit_var(lits[i])] == sig)
417 return l_True;
418 }
419 return l_False;
420 }
421
422 /*====================================================================*/
423 /* Minor (solver) functions: */
424
solver_setnvars(solver * s,int n)425 void solver_setnvars(solver* s,int n)
426 {
427 int var;
428
429 if (s->cap < n){
430
431 while (s->cap < n) s->cap = s->cap*2+1;
432
433 s->wlists = (vecp*) realloc(s->wlists,
434 sizeof(vecp)*s->cap*2);
435 s->activity = (double*) realloc(s->activity,
436 sizeof(double)*s->cap);
437 s->assigns = (lbool*) realloc(s->assigns,
438 sizeof(lbool)*s->cap);
439 s->orderpos = (int*) realloc(s->orderpos,
440 sizeof(int)*s->cap);
441 s->reasons = (clause**)realloc(s->reasons,
442 sizeof(clause*)*s->cap);
443 s->levels = (int*) realloc(s->levels,
444 sizeof(int)*s->cap);
445 s->tags = (lbool*) realloc(s->tags,
446 sizeof(lbool)*s->cap);
447 s->trail = (lit*) realloc(s->trail,
448 sizeof(lit)*s->cap);
449 }
450
451 for (var = s->size; var < n; var++){
452 vecp_new(&s->wlists[2*var]);
453 vecp_new(&s->wlists[2*var+1]);
454 s->activity [var] = 0;
455 s->assigns [var] = l_Undef;
456 s->orderpos [var] = veci_size(&s->order);
457 s->reasons [var] = (clause*)0;
458 s->levels [var] = 0;
459 s->tags [var] = l_Undef;
460
461 /* does not hold because variables enqueued at top level will
462 not be reinserted in the heap
463 assert(veci_size(&s->order) == var);
464 */
465 veci_push(&s->order,var);
466 order_update(s, var);
467 }
468
469 s->size = n > s->size ? n : s->size;
470 }
471
enqueue(solver * s,lit l,clause * from)472 static inline bool enqueue(solver* s, lit l, clause* from)
473 {
474 lbool* values = s->assigns;
475 int v = lit_var(l);
476 lbool val = values[v];
477 lbool sig;
478 #ifdef VERBOSEDEBUG
479 printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
480 #endif
481
482 /* lbool */ sig = !lit_sign(l); sig += sig - 1;
483 if (val != l_Undef){
484 return val == sig;
485 }else{
486 /* New fact -- store it. */
487 int* levels;
488 clause** reasons;
489 #ifdef VERBOSEDEBUG
490 printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
491 #endif
492 /* int* */ levels = s->levels;
493 /* clause** */ reasons = s->reasons;
494
495 values [v] = sig;
496 levels [v] = solver_dlevel(s);
497 reasons[v] = from;
498 s->trail[s->qtail++] = l;
499
500 order_assigned(s, v);
501 return true;
502 }
503 }
504
assume(solver * s,lit l)505 static inline void assume(solver* s, lit l){
506 assert(s->qtail == s->qhead);
507 assert(s->assigns[lit_var(l)] == l_Undef);
508 #ifdef VERBOSEDEBUG
509 printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
510 #endif
511 veci_push(&s->trail_lim,s->qtail);
512 enqueue(s,l,(clause*)0);
513 }
514
solver_canceluntil(solver * s,int level)515 static inline void solver_canceluntil(solver* s, int level) {
516 lit* trail;
517 lbool* values;
518 clause** reasons;
519 int bound;
520 int c;
521
522 if (solver_dlevel(s) <= level)
523 return;
524
525 trail = s->trail;
526 values = s->assigns;
527 reasons = s->reasons;
528 bound = (veci_begin(&s->trail_lim))[level];
529
530 for (c = s->qtail-1; c >= bound; c--) {
531 int x = lit_var(trail[c]);
532 values [x] = l_Undef;
533 reasons[x] = (clause*)0;
534 }
535
536 for (c = s->qhead-1; c >= bound; c--)
537 order_unassigned(s,lit_var(trail[c]));
538
539 s->qhead = s->qtail = bound;
540 veci_resize(&s->trail_lim,level);
541 }
542
solver_record(solver * s,veci * cls)543 static void solver_record(solver* s, veci* cls)
544 {
545 lit* begin = veci_begin(cls);
546 lit* end = begin + veci_size(cls);
547 clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1)
548 : (clause*)0;
549 enqueue(s,*begin,c);
550
551 assert(veci_size(cls) > 0);
552
553 if (c != 0) {
554 vecp_push(&s->learnts,c);
555 act_clause_bump(s,c);
556 s->stats.learnts++;
557 s->stats.learnts_literals += veci_size(cls);
558 }
559 }
560
solver_progress(solver * s)561 static double solver_progress(solver* s)
562 {
563 lbool* values = s->assigns;
564 int* levels = s->levels;
565 int i;
566
567 double progress = 0;
568 double F = 1.0 / s->size;
569 for (i = 0; i < s->size; i++)
570 if (values[i] != l_Undef)
571 progress += pow(F, levels[i]);
572 return progress / s->size;
573 }
574
575 /*====================================================================*/
576 /* Major methods: */
577
solver_lit_removable(solver * s,lit l,int minl)578 static bool solver_lit_removable(solver* s, lit l, int minl)
579 {
580 lbool* tags = s->tags;
581 clause** reasons = s->reasons;
582 int* levels = s->levels;
583 int top = veci_size(&s->tagged);
584
585 assert(lit_var(l) >= 0 && lit_var(l) < s->size);
586 assert(reasons[lit_var(l)] != 0);
587 veci_resize(&s->stack,0);
588 veci_push(&s->stack,lit_var(l));
589
590 while (veci_size(&s->stack) > 0){
591 clause* c;
592 int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
593 assert(v >= 0 && v < s->size);
594 veci_resize(&s->stack,veci_size(&s->stack)-1);
595 assert(reasons[v] != 0);
596 c = reasons[v];
597
598 if (clause_is_lit(c)){
599 int v = lit_var(clause_read_lit(c));
600 if (tags[v] == l_Undef && levels[v] != 0){
601 if (reasons[v] != 0
602 && ((1 << (levels[v] & 31)) & minl)){
603 veci_push(&s->stack,v);
604 tags[v] = l_True;
605 veci_push(&s->tagged,v);
606 }else{
607 int* tagged = veci_begin(&s->tagged);
608 int j;
609 for (j = top; j < veci_size(&s->tagged); j++)
610 tags[tagged[j]] = l_Undef;
611 veci_resize(&s->tagged,top);
612 return false;
613 }
614 }
615 }else{
616 lit* lits = clause_begin(c);
617 int i, j;
618
619 for (i = 1; i < clause_size(c); i++){
620 int v = lit_var(lits[i]);
621 if (tags[v] == l_Undef && levels[v] != 0){
622 if (reasons[v] != 0
623 && ((1 << (levels[v] & 31)) & minl)){
624
625 veci_push(&s->stack,lit_var(lits[i]));
626 tags[v] = l_True;
627 veci_push(&s->tagged,v);
628 }else{
629 int* tagged = veci_begin(&s->tagged);
630 for (j = top; j < veci_size(&s->tagged); j++)
631 tags[tagged[j]] = l_Undef;
632 veci_resize(&s->tagged,top);
633 return false;
634 }
635 }
636 }
637 }
638 }
639
640 return true;
641 }
642
solver_analyze(solver * s,clause * c,veci * learnt)643 static void solver_analyze(solver* s, clause* c, veci* learnt)
644 {
645 lit* trail = s->trail;
646 lbool* tags = s->tags;
647 clause** reasons = s->reasons;
648 int* levels = s->levels;
649 int cnt = 0;
650 lit p = lit_Undef;
651 int ind = s->qtail-1;
652 lit* lits;
653 int i, j, minl;
654 int* tagged;
655
656 veci_push(learnt,lit_Undef);
657
658 do{
659 assert(c != 0);
660
661 if (clause_is_lit(c)){
662 lit q = clause_read_lit(c);
663 assert(lit_var(q) >= 0 && lit_var(q) < s->size);
664 if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
665 tags[lit_var(q)] = l_True;
666 veci_push(&s->tagged,lit_var(q));
667 act_var_bump(s,lit_var(q));
668 if (levels[lit_var(q)] == solver_dlevel(s))
669 cnt++;
670 else
671 veci_push(learnt,q);
672 }
673 }else{
674
675 if (clause_learnt(c))
676 act_clause_bump(s,c);
677
678 lits = clause_begin(c);
679 /* printlits(lits,lits+clause_size(c)); printf("\n"); */
680 for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
681 lit q = lits[j];
682 assert(lit_var(q) >= 0 && lit_var(q) < s->size);
683 if (tags[lit_var(q)] == l_Undef
684 && levels[lit_var(q)] > 0){
685 tags[lit_var(q)] = l_True;
686 veci_push(&s->tagged,lit_var(q));
687 act_var_bump(s,lit_var(q));
688 if (levels[lit_var(q)] == solver_dlevel(s))
689 cnt++;
690 else
691 veci_push(learnt,q);
692 }
693 }
694 }
695
696 while (tags[lit_var(trail[ind--])] == l_Undef);
697
698 p = trail[ind+1];
699 c = reasons[lit_var(p)];
700 cnt--;
701
702 }while (cnt > 0);
703
704 *veci_begin(learnt) = lit_neg(p);
705
706 lits = veci_begin(learnt);
707 minl = 0;
708 for (i = 1; i < veci_size(learnt); i++){
709 int lev = levels[lit_var(lits[i])];
710 minl |= 1 << (lev & 31);
711 }
712
713 /* simplify (full) */
714 for (i = j = 1; i < veci_size(learnt); i++){
715 if (reasons[lit_var(lits[i])] == 0
716 || !solver_lit_removable(s,lits[i],minl))
717 lits[j++] = lits[i];
718 }
719
720 /* update size of learnt + statistics */
721 s->stats.max_literals += veci_size(learnt);
722 veci_resize(learnt,j);
723 s->stats.tot_literals += j;
724
725 /* clear tags */
726 tagged = veci_begin(&s->tagged);
727 for (i = 0; i < veci_size(&s->tagged); i++)
728 tags[tagged[i]] = l_Undef;
729 veci_resize(&s->tagged,0);
730
731 #ifdef DEBUG
732 for (i = 0; i < s->size; i++)
733 assert(tags[i] == l_Undef);
734 #endif
735
736 #ifdef VERBOSEDEBUG
737 printf(L_IND"Learnt {", L_ind);
738 for (i = 0; i < veci_size(learnt); i++)
739 printf(" "L_LIT, L_lit(lits[i]));
740 #endif
741 if (veci_size(learnt) > 1){
742 int max_i = 1;
743 int max = levels[lit_var(lits[1])];
744 lit tmp;
745
746 for (i = 2; i < veci_size(learnt); i++)
747 if (levels[lit_var(lits[i])] > max){
748 max = levels[lit_var(lits[i])];
749 max_i = i;
750 }
751
752 tmp = lits[1];
753 lits[1] = lits[max_i];
754 lits[max_i] = tmp;
755 }
756 #ifdef VERBOSEDEBUG
757 {
758 int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
759 printf(" } at level %d\n", lev);
760 }
761 #endif
762 }
763
solver_propagate(solver * s)764 clause* solver_propagate(solver* s)
765 {
766 lbool* values = s->assigns;
767 clause* confl = (clause*)0;
768 lit* lits;
769
770 /* printf("solver_propagate\n"); */
771 while (confl == 0 && s->qtail - s->qhead > 0){
772 lit p = s->trail[s->qhead++];
773 vecp* ws = solver_read_wlist(s,p);
774 clause **begin = (clause**)vecp_begin(ws);
775 clause **end = begin + vecp_size(ws);
776 clause **i, **j;
777
778 s->stats.propagations++;
779 s->simpdb_props--;
780
781 /* printf("checking lit %d: "L_LIT"\n", veci_size(ws),
782 L_lit(p)); */
783 for (i = j = begin; i < end; ){
784 if (clause_is_lit(*i)){
785 *j++ = *i;
786 if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
787 confl = s->binary;
788 (clause_begin(confl))[1] = lit_neg(p);
789 (clause_begin(confl))[0] = clause_read_lit(*i++);
790
791 /* Copy the remaining watches: */
792 while (i < end)
793 *j++ = *i++;
794 }
795 }else{
796 lit false_lit;
797 lbool sig;
798
799 lits = clause_begin(*i);
800
801 /* Make sure the false literal is data[1]: */
802 false_lit = lit_neg(p);
803 if (lits[0] == false_lit){
804 lits[0] = lits[1];
805 lits[1] = false_lit;
806 }
807 assert(lits[1] == false_lit);
808 /* printf("checking clause: ");
809 printlits(lits, lits+clause_size(*i));
810 printf("\n"); */
811
812 /* If 0th watch is true, then clause is already
813 satisfied. */
814 sig = !lit_sign(lits[0]); sig += sig - 1;
815 if (values[lit_var(lits[0])] == sig){
816 *j++ = *i;
817 }else{
818 /* Look for new watch: */
819 lit* stop = lits + clause_size(*i);
820 lit* k;
821 for (k = lits + 2; k < stop; k++){
822 lbool sig = lit_sign(*k); sig += sig - 1;
823 if (values[lit_var(*k)] != sig){
824 lits[1] = *k;
825 *k = false_lit;
826 vecp_push(solver_read_wlist(s,
827 lit_neg(lits[1])),*i);
828 goto next; }
829 }
830
831 *j++ = *i;
832 /* Clause is unit under assignment: */
833 if (!enqueue(s,lits[0], *i)){
834 confl = *i++;
835 /* Copy the remaining watches: */
836 while (i < end)
837 *j++ = *i++;
838 }
839 }
840 }
841 next:
842 i++;
843 }
844
845 s->stats.inspects += j - (clause**)vecp_begin(ws);
846 vecp_resize(ws,j - (clause**)vecp_begin(ws));
847 }
848
849 return confl;
850 }
851
clause_cmp(const void * x,const void * y)852 static inline int clause_cmp (const void* x, const void* y) {
853 return clause_size((clause*)x) > 2
854 && (clause_size((clause*)y) == 2
855 || clause_activity((clause*)x)
856 < clause_activity((clause*)y)) ? -1 : 1; }
857
solver_reducedb(solver * s)858 void solver_reducedb(solver* s)
859 {
860 int i, j;
861 double extra_lim = s->cla_inc / vecp_size(&s->learnts);
862 /* Remove any clause below this activity */
863 clause** learnts = (clause**)vecp_begin(&s->learnts);
864 clause** reasons = s->reasons;
865
866 sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), clause_cmp);
867
868 for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
869 if (clause_size(learnts[i]) > 2
870 && reasons[lit_var(*clause_begin(learnts[i]))]
871 != learnts[i])
872 clause_remove(s,learnts[i]);
873 else
874 learnts[j++] = learnts[i];
875 }
876 for (; i < vecp_size(&s->learnts); i++){
877 if (clause_size(learnts[i]) > 2
878 && reasons[lit_var(*clause_begin(learnts[i]))]
879 != learnts[i]
880 && clause_activity(learnts[i]) < extra_lim)
881 clause_remove(s,learnts[i]);
882 else
883 learnts[j++] = learnts[i];
884 }
885
886 /* printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); */
887
888 vecp_resize(&s->learnts,j);
889 }
890
solver_search(solver * s,int nof_conflicts,int nof_learnts)891 static lbool solver_search(solver* s, int nof_conflicts,
892 int nof_learnts)
893 {
894 int* levels = s->levels;
895 double var_decay = 0.95;
896 double clause_decay = 0.999;
897 double random_var_freq = 0.02;
898
899 int conflictC = 0;
900 veci learnt_clause;
901
902 assert(s->root_level == solver_dlevel(s));
903
904 s->stats.starts++;
905 s->var_decay = (float)(1 / var_decay );
906 s->cla_decay = (float)(1 / clause_decay);
907 veci_resize(&s->model,0);
908 veci_new(&learnt_clause);
909
910 for (;;){
911 clause* confl = solver_propagate(s);
912 if (confl != 0){
913 /* CONFLICT */
914 int blevel;
915
916 #ifdef VERBOSEDEBUG
917 printf(L_IND"**CONFLICT**\n", L_ind);
918 #endif
919 s->stats.conflicts++; conflictC++;
920 if (solver_dlevel(s) == s->root_level){
921 veci_delete(&learnt_clause);
922 return l_False;
923 }
924
925 veci_resize(&learnt_clause,0);
926 solver_analyze(s, confl, &learnt_clause);
927 blevel = veci_size(&learnt_clause) > 1
928 ? levels[lit_var(veci_begin(&learnt_clause)[1])]
929 : s->root_level;
930 blevel = s->root_level > blevel ? s->root_level : blevel;
931 solver_canceluntil(s,blevel);
932 solver_record(s,&learnt_clause);
933 act_var_decay(s);
934 act_clause_decay(s);
935
936 }else{
937 /* NO CONFLICT */
938 int next;
939
940 if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
941 /* Reached bound on number of conflicts: */
942 s->progress_estimate = solver_progress(s);
943 solver_canceluntil(s,s->root_level);
944 veci_delete(&learnt_clause);
945 return l_Undef; }
946
947 if (solver_dlevel(s) == 0)
948 /* Simplify the set of problem clauses: */
949 solver_simplify(s);
950
951 if (nof_learnts >= 0
952 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
953 /* Reduce the set of learnt clauses: */
954 solver_reducedb(s);
955
956 /* New variable decision: */
957 s->stats.decisions++;
958 next = order_select(s,(float)random_var_freq);
959
960 if (next == var_Undef){
961 /* Model found: */
962 lbool* values = s->assigns;
963 int i;
964 for (i = 0; i < s->size; i++)
965 veci_push(&s->model,(int)values[i]);
966 solver_canceluntil(s,s->root_level);
967 veci_delete(&learnt_clause);
968
969 /*
970 veci apa; veci_new(&apa);
971 for (i = 0; i < s->size; i++)
972 veci_push(&apa,(int)(s->model.ptr[i] == l_True
973 ? toLit(i) : lit_neg(toLit(i))));
974 printf("model: ");
975 printlits((lit*)apa.ptr,
976 (lit*)apa.ptr + veci_size(&apa)); printf("\n");
977 veci_delete(&apa);
978 */
979
980 return l_True;
981 }
982
983 assume(s,lit_neg(toLit(next)));
984 }
985 }
986
987 #if 0 /* by mao; unreachable code */
988 return l_Undef; /* cannot happen */
989 #endif
990 }
991
992 /*====================================================================*/
993 /* External solver functions: */
994
solver_new(void)995 solver* solver_new(void)
996 {
997 solver* s = (solver*)malloc(sizeof(solver));
998
999 /* initialize vectors */
1000 vecp_new(&s->clauses);
1001 vecp_new(&s->learnts);
1002 veci_new(&s->order);
1003 veci_new(&s->trail_lim);
1004 veci_new(&s->tagged);
1005 veci_new(&s->stack);
1006 veci_new(&s->model);
1007
1008 /* initialize arrays */
1009 s->wlists = 0;
1010 s->activity = 0;
1011 s->assigns = 0;
1012 s->orderpos = 0;
1013 s->reasons = 0;
1014 s->levels = 0;
1015 s->tags = 0;
1016 s->trail = 0;
1017
1018 /* initialize other vars */
1019 s->size = 0;
1020 s->cap = 0;
1021 s->qhead = 0;
1022 s->qtail = 0;
1023 s->cla_inc = 1;
1024 s->cla_decay = 1;
1025 s->var_inc = 1;
1026 s->var_decay = 1;
1027 s->root_level = 0;
1028 s->simpdb_assigns = 0;
1029 s->simpdb_props = 0;
1030 s->random_seed = 91648253;
1031 s->progress_estimate = 0;
1032 s->binary = (clause*)malloc(sizeof(clause)
1033 + sizeof(lit)*2);
1034 s->binary->size_learnt = (2 << 1);
1035 s->verbosity = 0;
1036
1037 s->stats.starts = 0;
1038 s->stats.decisions = 0;
1039 s->stats.propagations = 0;
1040 s->stats.inspects = 0;
1041 s->stats.conflicts = 0;
1042 s->stats.clauses = 0;
1043 s->stats.clauses_literals = 0;
1044 s->stats.learnts = 0;
1045 s->stats.learnts_literals = 0;
1046 s->stats.max_literals = 0;
1047 s->stats.tot_literals = 0;
1048
1049 return s;
1050 }
1051
solver_delete(solver * s)1052 void solver_delete(solver* s)
1053 {
1054 int i;
1055 for (i = 0; i < vecp_size(&s->clauses); i++)
1056 free(vecp_begin(&s->clauses)[i]);
1057
1058 for (i = 0; i < vecp_size(&s->learnts); i++)
1059 free(vecp_begin(&s->learnts)[i]);
1060
1061 /* delete vectors */
1062 vecp_delete(&s->clauses);
1063 vecp_delete(&s->learnts);
1064 veci_delete(&s->order);
1065 veci_delete(&s->trail_lim);
1066 veci_delete(&s->tagged);
1067 veci_delete(&s->stack);
1068 veci_delete(&s->model);
1069 free(s->binary);
1070
1071 /* delete arrays */
1072 if (s->wlists != 0){
1073 int i;
1074 for (i = 0; i < s->size*2; i++)
1075 vecp_delete(&s->wlists[i]);
1076
1077 /* if one is different from null, all are */
1078 free(s->wlists);
1079 free(s->activity );
1080 free(s->assigns );
1081 free(s->orderpos );
1082 free(s->reasons );
1083 free(s->levels );
1084 free(s->trail );
1085 free(s->tags );
1086 }
1087
1088 free(s);
1089 }
1090
solver_addclause(solver * s,lit * begin,lit * end)1091 bool solver_addclause(solver* s, lit* begin, lit* end)
1092 {
1093 lit *i,*j;
1094 int maxvar;
1095 lbool* values;
1096 lit last;
1097
1098 if (begin == end) return false;
1099
1100 /* printlits(begin,end); printf("\n"); */
1101 /* insertion sort */
1102 maxvar = lit_var(*begin);
1103 for (i = begin + 1; i < end; i++){
1104 lit l = *i;
1105 maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
1106 for (j = i; j > begin && *(j-1) > l; j--)
1107 *j = *(j-1);
1108 *j = l;
1109 }
1110 solver_setnvars(s,maxvar+1);
1111
1112 /* printlits(begin,end); printf("\n"); */
1113 values = s->assigns;
1114
1115 /* delete duplicates */
1116 last = lit_Undef;
1117 for (i = j = begin; i < end; i++){
1118 /* printf("lit: "L_LIT", value = %d\n", L_lit(*i),
1119 (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); */
1120 lbool sig = !lit_sign(*i); sig += sig - 1;
1121 if (*i == lit_neg(last) || sig == values[lit_var(*i)])
1122 return true; /* tautology */
1123 else if (*i != last && values[lit_var(*i)] == l_Undef)
1124 last = *j++ = *i;
1125 }
1126
1127 /* printf("final: "); printlits(begin,j); printf("\n"); */
1128
1129 if (j == begin) /* empty clause */
1130 return false;
1131 else if (j - begin == 1) /* unit clause */
1132 return enqueue(s,*begin,(clause*)0);
1133
1134 /* create new clause */
1135 vecp_push(&s->clauses,clause_new(s,begin,j,0));
1136
1137 s->stats.clauses++;
1138 s->stats.clauses_literals += j - begin;
1139
1140 return true;
1141 }
1142
solver_simplify(solver * s)1143 bool solver_simplify(solver* s)
1144 {
1145 clause** reasons;
1146 int type;
1147
1148 assert(solver_dlevel(s) == 0);
1149
1150 if (solver_propagate(s) != 0)
1151 return false;
1152
1153 if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
1154 return true;
1155
1156 reasons = s->reasons;
1157 for (type = 0; type < 2; type++){
1158 vecp* cs = type ? &s->learnts : &s->clauses;
1159 clause** cls = (clause**)vecp_begin(cs);
1160
1161 int i, j;
1162 for (j = i = 0; i < vecp_size(cs); i++){
1163 if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
1164 clause_simplify(s,cls[i]) == l_True)
1165 clause_remove(s,cls[i]);
1166 else
1167 cls[j++] = cls[i];
1168 }
1169 vecp_resize(cs,j);
1170 }
1171
1172 s->simpdb_assigns = s->qhead;
1173 /* (shouldn't depend on 'stats' really, but it will do for now) */
1174 s->simpdb_props = (int)(s->stats.clauses_literals
1175 + s->stats.learnts_literals);
1176
1177 return true;
1178 }
1179
solver_solve(solver * s,lit * begin,lit * end)1180 bool solver_solve(solver* s, lit* begin, lit* end)
1181 {
1182 double nof_conflicts = 100;
1183 double nof_learnts = solver_nclauses(s) / 3;
1184 lbool status = l_Undef;
1185 lbool* values = s->assigns;
1186 lit* i;
1187
1188 /* printf("solve: "); printlits(begin, end); printf("\n"); */
1189 for (i = begin; i < end; i++){
1190 switch (lit_sign(*i) ? -values[lit_var(*i)]
1191 : values[lit_var(*i)]){
1192 case 1: /* l_True: */
1193 break;
1194 case 0: /* l_Undef */
1195 assume(s, *i);
1196 if (solver_propagate(s) == NULL)
1197 break;
1198 /* falltrough */
1199 case -1: /* l_False */
1200 solver_canceluntil(s, 0);
1201 return false;
1202 }
1203 }
1204
1205 s->root_level = solver_dlevel(s);
1206
1207 if (s->verbosity >= 1){
1208 printf("==================================[MINISAT]============"
1209 "=======================\n");
1210 printf("| Conflicts | ORIGINAL | LEARNT "
1211 " | Progress |\n");
1212 printf("| | Clauses Literals | Limit Clauses Litera"
1213 "ls Lit/Cl | |\n");
1214 printf("======================================================="
1215 "=======================\n");
1216 }
1217
1218 while (status == l_Undef){
1219 double Ratio = (s->stats.learnts == 0)? 0.0 :
1220 s->stats.learnts_literals / (double)s->stats.learnts;
1221
1222 if (s->verbosity >= 1){
1223 printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %"
1224 "6.3f %% |\n",
1225 (double)s->stats.conflicts,
1226 (double)s->stats.clauses,
1227 (double)s->stats.clauses_literals,
1228 (double)nof_learnts,
1229 (double)s->stats.learnts,
1230 (double)s->stats.learnts_literals,
1231 Ratio,
1232 s->progress_estimate*100);
1233 fflush(stdout);
1234 }
1235 status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
1236 nof_conflicts *= 1.5;
1237 nof_learnts *= 1.1;
1238 }
1239 if (s->verbosity >= 1)
1240 printf("======================================================="
1241 "=======================\n");
1242
1243 solver_canceluntil(s,0);
1244 return status != l_False;
1245 }
1246
solver_nvars(solver * s)1247 int solver_nvars(solver* s)
1248 {
1249 return s->size;
1250 }
1251
solver_nclauses(solver * s)1252 int solver_nclauses(solver* s)
1253 {
1254 return vecp_size(&s->clauses);
1255 }
1256
solver_nconflicts(solver * s)1257 int solver_nconflicts(solver* s)
1258 {
1259 return (int)s->stats.conflicts;
1260 }
1261
1262 /*====================================================================*/
1263 /* Sorting functions (sigh): */
1264
selectionsort(void ** array,int size,int (* comp)(const void *,const void *))1265 static inline void selectionsort(void** array, int size,
1266 int(*comp)(const void *, const void *))
1267 {
1268 int i, j, best_i;
1269 void* tmp;
1270
1271 for (i = 0; i < size-1; i++){
1272 best_i = i;
1273 for (j = i+1; j < size; j++){
1274 if (comp(array[j], array[best_i]) < 0)
1275 best_i = j;
1276 }
1277 tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
1278 }
1279 }
1280
sortrnd(void ** array,int size,int (* comp)(const void *,const void *),double * seed)1281 static void sortrnd(void** array, int size,
1282 int(*comp)(const void *, const void *),
1283 double* seed)
1284 {
1285 if (size <= 15)
1286 selectionsort(array, size, comp);
1287
1288 else{
1289 void* pivot = array[irand(seed, size)];
1290 void* tmp;
1291 int i = -1;
1292 int j = size;
1293
1294 for(;;){
1295 do i++; while(comp(array[i], pivot)<0);
1296 do j--; while(comp(pivot, array[j])<0);
1297
1298 if (i >= j) break;
1299
1300 tmp = array[i]; array[i] = array[j]; array[j] = tmp;
1301 }
1302
1303 sortrnd(array , i , comp, seed);
1304 sortrnd(&array[i], size-i, comp, seed);
1305 }
1306 }
1307
sort(void ** array,int size,int (* comp)(const void *,const void *))1308 static void sort(void** array, int size,
1309 int(*comp)(const void *, const void *))
1310 {
1311 double seed = 91648253;
1312 sortrnd(array,size,comp,&seed);
1313 }
1314
1315 /* eof */
1316