传播函数分布在propsearch.h、propsearch.c和proplit.c文件之中
| propsearch.h | |
#ifndef _propsearch_h_INCLUDED #define _propsearch_h_INCLUDED struct kissat; struct clause; struct clause *kissat_search_propagate (struct kissat *); #endif
|
|
| propsearch.c | |
#define INLINE_ASSIGN #include "inline.h" #include "propsearch.h" #include "bump.h" // Keep this 'inlined' file separate: #include "assign.c" #define PROPAGATE_LITERAL search_propagate_literal #define PROPAGATION_TYPE "search" #include "proplit.h" static inline void update_search_propagation_statistics (kissat * solver, unsigned previous_propagated_level) { assert (previous_propagated_level <= solver->propagated); const unsigned propagated = solver->propagated - previous_propagated_level; LOG ("propagation took %" PRIu64 " propagations", propagated); LOG ("propagation took %" PRIu64 " ticks", solver->ticks); ADD (propagations, propagated); ADD (ticks, solver->ticks); ADD (search_propagations, propagated); ADD (search_ticks, solver->ticks); if (solver->stable) { ADD (stable_propagations, propagated); ADD (stable_ticks, solver->ticks); } else { ADD (focused_propagations, propagated); ADD (focused_ticks, solver->ticks); } } static inline void update_consistently_assigned (kissat * solver) { const unsigned assigned = kissat_assigned (solver); if (assigned != solver->consistently_assigned) { LOG ("updating consistently assigned from %u to %u", solver->consistently_assigned, assigned); solver->consistently_assigned = assigned; } else LOG ("keeping consistently assigned %u", assigned); } static clause * search_propagate (kissat * solver) { clause *res = 0; while (!res && solver->propagated < SIZE_STACK (solver->trail)) { const unsigned lit = PEEK_STACK (solver->trail, solver->propagated); res = search_propagate_literal (solver, lit); solver->propagated++; } return res; } clause * kissat_search_propagate (kissat * solver) { assert (!solver->probing); assert (solver->watching); assert (!solver->inconsistent); START (propagate); solver->ticks = 0; const unsigned propagated = solver->propagated; clause *conflict = search_propagate (solver); update_search_propagation_statistics (solver, propagated); update_consistently_assigned (solver); if (conflict) INC (conflicts); STOP (propagate); // CHB if(solver->stable && solver->heuristic==1){ int i = SIZE_STACK (solver->trail) - 1; unsigned lit = i>=0?PEEK_STACK (solver->trail, i):0; while(i>=0 && LEVEL(lit)==solver->level){ lit = PEEK_STACK (solver->trail, i); kissat_bump_chb(solver,IDX(lit), conflict? 1.0 : 0.9); i--; } } if(solver->stable && solver->heuristic==1 && conflict) kissat_decay_chb(solver); return conflict; }
|
|
| proplit.c | |
1 static inline clause * 2 PROPAGATE_LITERAL (kissat * solver, 3 #if defined(HYPER_PROPAGATION) || defined(PROBING_PROPAGATION) 4 const clause * ignore, 5 #endif 6 const unsigned lit) 7 { 8 assert (solver->watching); 9 LOG (PROPAGATION_TYPE " propagating %s", LOGLIT (lit)); 10 assert (VALUE (lit) > 0); 11 assert (EMPTY_STACK (solver->delayed)); 12 13 const word *arena = BEGIN_STACK (solver->arena); 14 assigned *assigned = solver->assigned; 15 value *values = solver->values; 16 17 const unsigned not_lit = NOT (lit); 18 #ifdef HYPER_PROPAGATION 19 const bool hyper = GET_OPTION (hyper); 20 #endif 21 watches *watches = &WATCHES (not_lit); 22 watch *begin_watches = BEGIN_WATCHES (*watches), *q = begin_watches; 23 const watch *end_watches = END_WATCHES (*watches), *p = q; 24 unsigneds *delayed = &solver->delayed; 25 26 uint64_t ticks = kissat_cache_lines (watches->size, sizeof (watch)); 27 28 clause *res = 0; 29 30 while (p != end_watches) 31 { 32 const watch head = *q++ = *p++; 33 const unsigned blocking = head.blocking.lit; 34 assert (VALID_INTERNAL_LITERAL (blocking)); 35 const value blocking_value = values[blocking]; 36 if (head.type.binary) 37 { 38 if (blocking_value > 0) 39 continue; 40 const bool redundant = head.binary.redundant; 41 if (blocking_value < 0) 42 { 43 res = kissat_binary_conflict (solver, redundant, 44 not_lit, blocking); 45 break; 46 } 47 else 48 { 49 assert (!blocking_value); 50 kissat_assign_binary (solver, values, assigned, 51 redundant, blocking, not_lit); 52 } 53 } 54 else 55 { 56 const watch tail = *q++ = *p++; 57 if (blocking_value > 0) 58 continue; 59 const reference ref = tail.raw; 60 assert (ref < SIZE_STACK (solver->arena)); 61 clause *c = (clause *) (arena + ref); 62 #if defined(HYPER_PROPAGATION) || defined(PROBING_PROPAGATION) 63 if (c == ignore) 64 continue; 65 #endif 66 ticks++; 67 if (c->garbage) 68 { 69 q -= 2; 70 continue; 71 } 72 unsigned *lits = BEGIN_LITS (c); 73 const unsigned other = lits[0] ^ lits[1] ^ not_lit; 74 assert (lits[0] != lits[1]); 75 assert (VALID_INTERNAL_LITERAL (other)); 76 assert (not_lit != other); 77 assert (lit != other); 78 const value other_value = values[other]; 79 if (other_value > 0) 80 q[-2].blocking.lit = other; 81 else 82 { 83 const unsigned *end_lits = lits + c->size; 84 unsigned *searched = lits + c->searched; 85 assert (c->lits + 2 <= searched); 86 assert (searched < end_lits); 87 unsigned *r, replacement = INVALID_LIT; 88 value replacement_value = -1; 89 for (r = searched; r != end_lits; r++) 90 { 91 replacement = *r; 92 assert (VALID_INTERNAL_LITERAL (replacement)); 93 replacement_value = values[replacement]; 94 if (replacement_value >= 0) 95 break; 96 } 97 if (replacement_value < 0) 98 { 99 for (r = lits + 2; r != searched; r++) 100 { 101 replacement = *r; 102 assert (VALID_INTERNAL_LITERAL (replacement)); 103 replacement_value = values[replacement]; 104 if (replacement_value >= 0) 105 break; 106 } 107 } 108 109 if (replacement_value >= 0) 110 c->searched = r - c->lits; 111 112 if (replacement_value > 0) 113 { 114 assert (replacement != INVALID_LIT); 115 q[-2].blocking.lit = replacement; 116 } 117 else if (!replacement_value) 118 { 119 assert (replacement != INVALID_LIT); 120 LOGREF (ref, "unwatching %s in", LOGLIT (not_lit)); 121 q -= 2; 122 lits[0] = other; 123 lits[1] = replacement; 124 assert (lits[0] != lits[1]); 125 *r = not_lit; 126 kissat_delay_watching_large (solver, delayed, 127 replacement, other, ref); 128 ticks++; 129 } 130 else if (other_value) 131 { 132 assert (replacement_value < 0); 133 assert (blocking_value < 0); 134 assert (other_value < 0); 135 LOGREF (ref, "conflicting"); 136 res = c; 137 break; 138 } 139 #ifdef HYPER_PROPAGATION 140 else if (hyper) 141 { 142 assert (replacement_value < 0); 143 unsigned dom = kissat_find_dominator (solver, other, c); 144 if (dom != INVALID_LIT) 145 { 146 LOGBINARY (dom, other, "hyper binary resolvent"); 147 148 INC (hyper_binary_resolved); 149 INC (clauses_added); 150 151 INC (hyper_binaries); 152 INC (clauses_redundant); 153 154 CHECK_AND_ADD_BINARY (dom, other); 155 ADD_BINARY_TO_PROOF (dom, other); 156 157 kissat_assign_binary (solver, values, assigned, 158 true, other, dom); 159 160 delay_watching_hyper (solver, delayed, dom, other); 161 delay_watching_hyper (solver, delayed, other, dom); 162 163 kissat_delay_watching_large (solver, delayed, 164 not_lit, other, ref); 165 166 LOGREF (ref, "unwatching %s in", LOGLIT (not_lit)); 167 q -= 2; 168 } 169 else 170 kissat_assign_reference (solver, values, 171 assigned, other, ref, c); 172 } 173 #endif 174 else 175 { 176 assert (replacement_value < 0); 177 kissat_assign_reference (solver, values, 178 assigned, other, ref, c); 179 } 180 } 181 } 182 } 183 solver->ticks += ticks; 184 185 while (p != end_watches) 186 *q++ = *p++; 187 SET_END_OF_WATCHES (*watches, q); 188 189 #ifdef HYPER_PROPAGATION 190 watch_hyper_delayed (solver, delayed); 191 #else 192 kissat_watch_large_delayed (solver, delayed); 193 #endif 194 195 return res; 196 }
|
|