学习：传播、回溯、重启
|
//propsearch.h中 定义以下引用标识符 #define PROPAGATE_LITERAL search_propagate_literal |
|
|
//proplit.h中给出完整传播函数定义——对于了解文字传播队列非常重要 1 static inline clause *PROPAGATE_LITERAL (kissat *solver,
2 #if defined(PROBING_PROPAGATION)
3 const clause *const ignore,
4 #endif
5 const unsigned lit) {
6 assert (solver->watching);
7 LOG (PROPAGATION_TYPE " propagating %s", LOGLIT (lit));
8 assert (VALUE (lit) > 0);
9 assert (EMPTY_STACK (solver->delayed));
10
11 watches *const all_watches = solver->watches;
12 ward *const arena = BEGIN_STACK (solver->arena);
13 assigned *const assigned = solver->assigned;
14 value *const values = solver->values;
15
16 const unsigned not_lit = NOT (lit);
17
18 assert (not_lit < LITS);
19 watches *watches = all_watches + not_lit;
20
21 watch *const begin_watches = BEGIN_WATCHES (*watches);
22 const watch *const end_watches = END_WATCHES (*watches);
23
24 watch *q = begin_watches;
25 const watch *p = q;
26
27 unsigneds *const delayed = &solver->delayed;
28 assert (EMPTY_STACK (*delayed));
29
30 const size_t size_watches = SIZE_WATCHES (*watches);
31 uint64_t ticks = 1 + kissat_cache_lines (size_watches, sizeof (watch));
32 const unsigned idx = IDX (lit);
33 struct assigned *const a = assigned + idx;
34 const bool probing = solver->probing;
35 const unsigned level = a->level;
36 clause *res = 0;
37
38 while (p != end_watches) {
39 const watch head = *q++ = *p++;
40 const unsigned blocking = head.blocking.lit;
41 assert (VALID_INTERNAL_LITERAL (blocking));
42 const value blocking_value = values[blocking];
43 const bool binary = head.type.binary;
44 watch tail;
45 if (!binary)
46 tail = *q++ = *p++;
47 if (blocking_value > 0)
48 continue;
49 if (binary) {
50 if (blocking_value < 0) {
51 res = kissat_binary_conflict (solver, not_lit, blocking);
52 #ifndef CONTINUE_PROPAGATING_AFTER_CONFLICT
53 break;
54 #endif
55 } else {
56 assert (!blocking_value);
57 kissat_fast_binary_assign (solver, probing, level, values, assigned,
58 blocking, not_lit);
59 ticks++;
60 }
61 } else {
62 const reference ref = tail.raw;
63 assert (ref < SIZE_STACK (solver->arena));
64 clause *const c = (clause *) (arena + ref);
65 ticks++;
66 if (c->garbage) {
67 q -= 2;
68 continue;
69 }
70 unsigned *const lits = BEGIN_LITS (c);
71 const unsigned other = lits[0] ^ lits[1] ^ not_lit;
72 assert (lits[0] != lits[1]);
73 assert (VALID_INTERNAL_LITERAL (other));
74 assert (not_lit != other);
75 assert (lit != other);
76 const value other_value = values[other];
77 if (other_value > 0) {
78 q[-2].blocking.lit = other;
79 continue;
80 }
81 const unsigned *const end_lits = lits + c->size;
82 unsigned *const searched = lits + c->searched;
83 assert (c->lits + 2 <= searched);
84 assert (searched < end_lits);
85 unsigned *r, replacement = INVALID_LIT;
86 value replacement_value = -1;
87 for (r = searched; r != end_lits; r++) {
88 replacement = *r;
89 assert (VALID_INTERNAL_LITERAL (replacement));
90 replacement_value = values[replacement];
91 if (replacement_value >= 0)
92 break;
93 }
94 if (replacement_value < 0) {
95 for (r = lits + 2; r != searched; r++) {
96 replacement = *r;
97 assert (VALID_INTERNAL_LITERAL (replacement));
98 replacement_value = values[replacement];
99 if (replacement_value >= 0)
100 break;
101 }
102 }
103
104 if (replacement_value >= 0) {
105 c->searched = r - lits;
106 assert (replacement != INVALID_LIT);
107 LOGREF3 (ref, "unwatching %s in", LOGLIT (not_lit));
108 q -= 2;
109 lits[0] = other;
110 lits[1] = replacement;
111 assert (lits[0] != lits[1]);
112 *r = not_lit;
113 kissat_delay_watching_large (solver, delayed, replacement, other,
114 ref);
115 ticks++;
116 } else if (other_value) {
117 assert (replacement_value < 0);
118 assert (blocking_value < 0);
119 assert (other_value < 0);
120 #if defined(PROBING_PROPAGATION)
121 if (c == ignore) {
122 LOGREF (ref, "conflicting but ignored");
123 continue;
124 }
125 #endif
126 LOGREF (ref, "conflicting");
127 res = c;
128 #ifndef CONTINUE_PROPAGATING_AFTER_CONFLICT
129 break;
130 #endif
131 } else {
132 assert (replacement_value < 0);
133 #if defined(PROBING_PROPAGATION)
134 if (c == ignore) {
135 LOGREF (ref, "forcing %s but ignored", LOGLIT (other));
136 continue;
137 }
138 #endif
139 kissat_fast_assign_reference (solver, values, assigned, other, ref,
140 c);
141 ticks++;
142 }
143 }
144 }
145 solver->ticks += ticks;
146
147 while (p != end_watches)
148 *q++ = *p++;
149 SET_END_OF_WATCHES (*watches, q);
150
151 kissat_watch_large_delayed (solver, all_watches, delayed);
152
153 return res;
154 }
|
|
|
函数kissat_fast_assign_reference ---------- D:\SAT_study2024\kissat-sc2024-d776b9e1\src\fastassign.h ---------- D:\SAT_study2024\kissat-sc2024-d776b9e1\src\propdense.c ---------- D:\SAT_study2024\kissat-sc2024-d776b9e1\src\proplit.h
//fastassign.h 1 #ifndef _fastassign_h_INCLUDED
2 #define _fastassign_h_INCLUDED
3
4 #define FAST_ASSIGN
5
6 #include "inline.h"
7 #include "inlineassign.h"
8
9 static inline void kissat_fast_binary_assign (
10 kissat *solver, const bool probing, const unsigned level, value *values,
11 assigned *assigned, unsigned lit, unsigned other) {
12 if (GET_OPTION (jumpreasons) && level && solver->classification.bigbig) {
13 unsigned other_idx = IDX (other);
14 struct assigned *a = assigned + other_idx;
15 if (a->binary) {
16 LOGBINARY (lit, other, "jumping %s reason", LOGLIT (lit));
17 INC (jumped_reasons);
18 other = a->reason;
19 }
20 }
21 kissat_fast_assign (solver, probing, level, values, assigned, true, lit,
22 other);
23 LOGBINARY (lit, other, "assign %s reason", LOGLIT (lit));
24 }
25
26 static inline void
27 kissat_fast_assign_reference (kissat *solver, value *values,
28 assigned *assigned, unsigned lit,
29 reference ref, clause *reason) {
30 assert (reason == kissat_dereference_clause (solver, ref));
31 const unsigned level =
32 kissat_assignment_level (solver, values, assigned, lit, reason);
33 assert (level <= solver->level);
34 assert (ref != DECISION_REASON);
35 assert (ref != UNIT_REASON);
36 kissat_fast_assign (solver, solver->probing, level, values, assigned,
37 false, lit, ref);
38 LOGREF (ref, "assign %s reason", LOGLIT (lit));
39 }
40
41 #endif
//inlineassign.h #define kissat_assign kissat_fast_assign
//inlineassign.h完整代码 1 #ifndef _inlineassign_h_INLCUDED
2 #define _inlineassign_h_INLCUDED
3
4 #ifdef FAST_ASSIGN
5 #define kissat_assign kissat_fast_assign
6 #endif
7
8 static inline void kissat_assign (kissat *solver, const bool probing,
9 const unsigned level,
10 #ifdef FAST_ASSIGN
11 value *values, assigned *assigned,
12 #endif
13 bool binary, unsigned lit,
14 unsigned reason) {
15 const unsigned not_lit = NOT (lit);
16
17 watches watches = WATCHES (not_lit);
18 if (!kissat_empty_vector (&watches)) {
19 watch *w = BEGIN_WATCHES (watches);
20 __builtin_prefetch (w, 0, 1);
21 }
22
23 #ifndef FAST_ASSIGN
24 value *values = solver->values;
25 #endif
26 assert (!values[lit]);
27 assert (!values[not_lit]);
28
29 values[lit] = 1;
30 values[not_lit] = -1;
31
32 assert (solver->unassigned > 0);
33 solver->unassigned--;
34
35 if (!level) {
36 kissat_mark_fixed_literal (solver, lit);
37 assert (solver->unflushed < UINT_MAX);
38 solver->unflushed++;
39 if (reason != UNIT_REASON) {
40 CHECK_AND_ADD_UNIT (lit);
41 ADD_UNIT_TO_PROOF (lit);
42 reason = UNIT_REASON;
43 binary = false;
44 }
45 }
46
47 const size_t trail = SIZE_ARRAY (solver->trail);
48 PUSH_ARRAY (solver->trail, lit);
49
50 const unsigned idx = IDX (lit);
51
52 #if !defined(PROBING_PROPAGATION)
53 if (!probing) {
54 const bool negated = NEGATED (lit);
55 const value new_value = BOOL_TO_VALUE (negated);
56 value *saved = &SAVED (idx);
57 *saved = new_value;
58 }
59 #endif
60
61 struct assigned b;
62
63 b.level = level;
64 b.trail = trail;
65
66 b.analyzed = false;
67 b.binary = binary;
68 b.poisoned = false;
69 b.reason = reason;
70 b.removable = false;
71 b.shrinkable = false;
72
73 #ifndef FAST_ASSIGN
74 assigned *assigned = solver->assigned;
75 #endif
76 struct assigned *a = assigned + idx;
77 *a = b;
78 }
79
80 static inline unsigned
81 kissat_assignment_level (kissat *solver, value *values, assigned *assigned,
82 unsigned lit, clause *reason) {
83 unsigned res = 0;
84 for (all_literals_in_clause (other, reason)) {
85 if (other == lit)
86 continue;
87 assert (values[other] < 0), (void) values;
88 const unsigned other_idx = IDX (other);
89 struct assigned *a = assigned + other_idx;
90 const unsigned level = a->level;
91 if (res < level)
92 res = level;
93 }
94 #ifdef NDEBUG
95 (void) solver;
96 #endif
97 return res;
98 }
99
100 #endif
|
|
标签：输出,const,solver,lit,修改,other,assigned,kissat From： https://www.cnblogs.com/yuweng1689/p/18408904