lemon-project-template-glpk

comparison deps/glpk/src/minisat/minisat.c @ 9:33de93886c88

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