标签：++ 认知 watches first 2020 push cr 观察 size
|
一、观察体系的基本数据结构： ---------------------------------------------------------------------------------------------------------------------------------- 1.基础数据结构 （1）观察体系所在类型模板 //=================================================================================================
// OccLists -- a class for maintaining occurence lists with lazy deletion:
template<class Idx, class Vec, class Deleted>
class OccLists
{
vec<Vec> occs;
vec<char> dirty;
vec<Idx> dirties;
Deleted deleted;
public:
OccLists(const Deleted& d) : deleted(d) {}
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
void cleanAll ();
void clean (const Idx& idx);
void smudge (const Idx& idx){
if (dirty[toInt(idx)] == 0){
dirty[toInt(idx)] = 1;
dirties.push(idx);
}
}
void clear(bool free = true){
occs .clear(free);
dirty .clear(free);
dirties.clear(free);
}
};
template<class Idx, class Vec, class Deleted>
void OccLists<Idx,Vec,Deleted>::cleanAll()
{
for (int i = 0; i < dirties.size(); i++)
// Dirties may contain duplicates so check here if a variable is already cleaned:
if (dirty[toInt(dirties[i])])
clean(dirties[i]);
dirties.clear();
}
template<class Idx, class Vec, class Deleted>
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
{
Vec& vec = occs[toInt(idx)];
int i, j;
for (i = j = 0; i < vec.size(); i++)
if (!deleted(vec[i]))
vec[j++] = vec[i];
vec.shrink(i - j);
dirty[toInt(idx)] = 0;
}
2.求解器类型中内部声明的类型 1 struct Watcher {
2 CRef cref;
3 Lit blocker;
4 Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
5 bool operator==(const Watcher& w) const { return cref == w.cref; }
6 bool operator!=(const Watcher& w) const { return cref != w.cref; }
7 };
8
9 struct WatcherDeleted
10 {
11 const ClauseAllocator& ca;
12 WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
13 bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
14 };
3.求解器数据成员---两个观察体系 OccLists<Lit, vec<Watcher>, WatcherDeleted>
watches_bin, // Watches for binary clauses only.
watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
4.构造函数中---给予初始化 , watches_bin (WatcherDeleted(ca)) , watches (WatcherDeleted(ca))
|
|
|
二、相关函数学习 |
|
1 void Solver::relocAll(ClauseAllocator& to)
2 {
3 // All watchers:
4 //
5 // for (int i = 0; i < watches.size(); i++)
6 watches.cleanAll(); //观察体系cleanAll操作
7 watches_bin.cleanAll();
8 for (int v = 0; v < nVars(); v++)
9 for (int s = 0; s < 2; s++){
10 Lit p = mkLit(v, s);//针对正负文字分别有对应的观察
11 // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
12 vec<Watcher>& ws = watches[p];//注意，虽然已经cleanAll,但是此处依然可以获取文字的观察
13 for (int j = 0; j < ws.size(); j++)
14 ca.reloc(ws[j].cref, to);
15 vec<Watcher>& ws_bin = watches_bin[p];
16 for (int j = 0; j < ws_bin.size(); j++)
17 ca.reloc(ws_bin[j].cref, to);
18 }
19
20 // All reasons:
21 //
22 for (int i = 0; i < trail.size(); i++){
23 Var v = var(trail[i]);
24
25 if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
26 ca.reloc(vardata[v].reason, to);
27 }
28
29 // All learnt:
30 //
31 for (int i = 0; i < learnts_core.size(); i++)
32 ca.reloc(learnts_core[i], to);
33 for (int i = 0; i < learnts_tier2.size(); i++)
34 ca.reloc(learnts_tier2[i], to);
35 for (int i = 0; i < learnts_local.size(); i++)
36 ca.reloc(learnts_local[i], to);
37
38 // All original:
39 //
40 int i, j;
41 for (i = j = 0; i < clauses.size(); i++)
42 if (ca[clauses[i]].mark() != 1){
43 ca.reloc(clauses[i], to);
44 clauses[j++] = clauses[i]; }
45 clauses.shrink(i - j);
46 }
从本函数中可以看到求解器自行管理内存的情况。——管理观察体系（观察、观察元）、传播的reason子句、学习子句集 |
|
1 Var Solver::newVar(bool sign, bool dvar)
2 {
3 int v = nVars();
4 watches_bin.init(mkLit(v, false));
5 watches_bin.init(mkLit(v, true ));
6 watches .init(mkLit(v, false));
7 watches .init(mkLit(v, true ));
8 assigns .push(l_Undef);
9 vardata .push(mkVarData(CRef_Undef, 0));
10 lastConflict.push(0); //Scavel
11 activity_CHB .push(0);
12 activity_VSIDS.push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
13
14 picked.push(0);
15 conflicted.push(0);
16 almost_conflicted.push(0);
17 #ifdef ANTI_EXPLORATION
18 canceled.push(0);
19 #endif
20
21 seen .push(0);
22 seen2 .push(0);
23 polarity .push(sign);
24 decision .push();
25 trail .capacity(v+1);
26 setDecisionVar(v, dvar);
27
28 activity_distance.push(0);
29 var_iLevel.push(0);
30 var_iLevel_tmp.push(0);
31 pathCs.push(0);
32 return v;
33 }
newVar(bool sign, bool dvar)
|
|
// simplify All
//
CRef Solver::simplePropagate()
{
CRef confl = CRef_Undef;
int num_props = 0;
watches.cleanAll();
watches_bin.cleanAll();
while (qhead < trail.size())
{
Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
vec<Watcher>& ws = watches[p];
Watcher *i, *j, *end;
num_props++;
// First, Propagate binary clauses
vec<Watcher>& wbin = watches_bin[p];
for (int k = 0; k<wbin.size(); k++)
{
Lit imp = wbin[k].blocker;
if (value(imp) == l_False)
{
return wbin[k].cref;
}
if (value(imp) == l_Undef)
{
simpleUncheckEnqueue(imp, wbin[k].cref);
}
}
for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;)
{
// Try to avoid inspecting the clause:
Lit blocker = i->blocker;
if (value(blocker) == l_True)
{
*j++ = *i++; continue;
}
// Make sure the false literal is data[1]:
CRef cr = i->cref;
Clause& c = ca[cr];
Lit false_lit = ~p;
if (c[0] == false_lit)
c[0] = c[1], c[1] = false_lit;
assert(c[1] == false_lit);
// i++;
// If 0th watch is true, then clause is already satisfied.
// However, 0th watch is not the blocker, make it blocker using a new watcher w
// why not simply do i->blocker=first in this case?
Lit first = c[0];
// Watcher w = Watcher(cr, first);
if (first != blocker && value(first) == l_True)
{
i->blocker = first;
*j++ = *i++; continue;
}
// Look for new watch:
//if (incremental)
//{ // ----------------- INCREMENTAL MODE
// int choosenPos = -1;
// for (int k = 2; k < c.size(); k++)
// {
// if (value(c[k]) != l_False)
// {
// if (decisionLevel()>assumptions.size())
// {
// choosenPos = k;
// break;
// }
// else
// {
// choosenPos = k;
// if (value(c[k]) == l_True || !isSelector(var(c[k]))) {
// break;
// }
// }
// }
// }
// if (choosenPos != -1)
// {
// // watcher i is abandonned using i++, because cr watches now ~c[k] instead of p
// // the blocker is first in the watcher. However,
// // the blocker in the corresponding watcher in ~first is not c[1]
// Watcher w = Watcher(cr, first); i++;
// c[1] = c[choosenPos]; c[choosenPos] = false_lit;
// watches[~c[1]].push(w);
// goto NextClause;
// }
//}
else
{ // ----------------- DEFAULT MODE (NOT INCREMENTAL)
for (int k = 2; k < c.size(); k++)
{
if (value(c[k]) != l_False)
{
// watcher i is abandonned using i++, because cr watches now ~c[k] instead of p
// the blocker is first in the watcher. However,
// the blocker in the corresponding watcher in ~first is not c[1]
Watcher w = Watcher(cr, first); i++;
c[1] = c[k]; c[k] = false_lit;
watches[~c[1]].push(w);
goto NextClause;
}
}
}
// Did not find watch -- clause is unit under assignment:
i->blocker = first;
*j++ = *i++;
if (value(first) == l_False)
{
confl = cr;
qhead = trail.size();
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
else
{
simpleUncheckEnqueue(first, cr);
}
NextClause:;
}
ws.shrink(i - j);
}
s_propagations += num_props;
return confl;
}
simplePropagate()
|
|
1 void Solver::attachClause(CRef cr) {
2 const Clause& c = ca[cr];
3 assert(c.size() > 1);
4 OccLists<Lit, vec<Watcher>, WatcherDeleted>& ws = c.size() == 2 ? watches_bin : watches;
5 ws[~c[0]].push(Watcher(cr, c[1]));
6 ws[~c[1]].push(Watcher(cr, c[0]));
7 if (c.learnt()) learnts_literals += c.size();
8 else clauses_literals += c.size(); }
9
10
11 void Solver::detachClause(CRef cr, bool strict) {
12 const Clause& c = ca[cr];
13 assert(c.size() > 1);
14 OccLists<Lit, vec<Watcher>, WatcherDeleted>& ws = c.size() == 2 ? watches_bin : watches;
15
16 if (strict){
17 remove(ws[~c[0]], Watcher(cr, c[1]));
18 remove(ws[~c[1]], Watcher(cr, c[0]));
19 }else{
20 // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
21 ws.smudge(~c[0]);
22 ws.smudge(~c[1]);
23 }
24
25 if (c.learnt()) learnts_literals -= c.size();
26 else clauses_literals -= c.size(); }
27
28
29 void Solver::removeClause(CRef cr) {
30 Clause& c = ca[cr];
31
32 if (drup_file){
33 if (c.mark() != 1){
34 #ifdef BIN_DRUP
35 binDRUP('d', c, drup_file);
36 #else
37 fprintf(drup_file, "d ");
38 for (int i = 0; i < c.size(); i++)
39 fprintf(drup_file, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1));
40 fprintf(drup_file, "0\n");
41 #endif
42 }else
43 printf("c Bug. I don't expect this to happen.\n");
44 }
45
46 detachClause(cr);
47 // Don't leave pointers to free'd memory!
48 if (locked(c)){
49 Lit implied = c.size() != 2 ? c[0] : (value(c[0]) == l_True ? c[0] : c[1]);
50 vardata[var(implied)].reason = CRef_Undef; }
51 c.mark(1); //mark为1表明允许释放空间
52 ca.free(cr);
53 }
|
|
1 CRef Solver::propagate()
2 {
3 CRef confl = CRef_Undef;
4 int num_props = 0;
5 watches.cleanAll();
6 watches_bin.cleanAll();
7 //-------------------------------------------------------------------------
8 //设置一个保留多个传播文字的队列,排查决策(或隐含决策)p文字时，将其传播的文字存存下来供排序后再加入到队列
9 vec<Lit> curProLits;
10 vec<CRef> curProCrefs;
11 vec<int> curProLevel;
12 //-------------------------------------------------------------------------
13
14 while (qhead < trail.size()){
15 Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
16 int currLevel = level(var(p));
17 vec<Watcher>& ws = watches[p];
18 Watcher *i, *j, *end;
19 num_props++;
20
21 //---------------------------------------------------------------------
22 //本次排查p开始前清空,用于存储当前已知赋值序列前提下P所能传播的全部文字
23 curProLits.clear();
24 curProCrefs.clear();
25 curProLevel.clear();
26 //---------------------------------------------------------------------
27
28
29 vec<Watcher>& ws_bin = watches_bin[p]; // Propagate binary clauses first.
30 for (int k = 0; k < ws_bin.size(); k++){
31 Lit the_other = ws_bin[k].blocker;
32 if (value(the_other) == l_False){
33 confl = ws_bin[k].cref;
34 #ifdef LOOSE_PROP_STAT
35 return confl;
36 #else
37 goto ExitProp;
38 #endif
39 }else if(value(the_other) == l_Undef)
40 {
41 uncheckedEnqueue(the_other, currLevel, ws_bin[k].cref);
42 #ifdef PRINT_OUT
43 std::cout << "i " << the_other << " l " << currLevel << "\n";
44 #endif
45 }
46 }
47
48
49 for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
50 // Try to avoid inspecting the clause:
51 Lit blocker = i->blocker;
52 if (value(blocker) == l_True){
53 *j++ = *i++; continue; }
54
55 // Make sure the false literal is data[1]:
56 CRef cr = i->cref;
57 Clause& c = ca[cr];
58 Lit false_lit = ~p;
59 if (c[0] == false_lit)
60 c[0] = c[1], c[1] = false_lit;
61 assert(c[1] == false_lit);
62 i++;
63
64 // If 0th watch is true, then clause is already satisfied.
65 Lit first = c[0];
66 Watcher w = Watcher(cr, first);
67 if (first != blocker && value(first) == l_True){
68 *j++ = w; continue; }
69
70 // Look for new watch:
71 for (int k = 2; k < c.size(); k++)
72 if (value(c[k]) != l_False){
73 c[1] = c[k]; c[k] = false_lit;
74 watches[~c[1]].push(w);
75 goto NextClause; }
76
77 // Did not find watch -- clause is unit under assignment:
78 *j++ = w;
79 if (value(first) == l_False){
80 confl = cr;
81 qhead = trail.size();
82 // Copy the remaining watches:
83 while (i < end)
84 *j++ = *i++;
85 }else
86 {
87 if (currLevel == decisionLevel())
88 {
89 //----------------------
90 curProLits.push(first);
91 curProCrefs.push(cr);
92 curProLevel.push(currLevel);
93 //----------------------
94 //uncheckedEnqueue(first, currLevel, cr);
95 #ifdef PRINT_OUT
96 std::cout << "i " << first << " l " << currLevel << "\n";
97 #endif
98 }
99 else
100 {
101 int nMaxLevel = currLevel;
102 int nMaxInd = 1;
103 // pass over all the literals in the clause and find the one with the biggest level
104 for (int nInd = 2; nInd < c.size(); ++nInd)
105 {
106 int nLevel = level(var(c[nInd]));
107 if (nLevel > nMaxLevel)
108 {
109 nMaxLevel = nLevel;
110 nMaxInd = nInd;
111 }
112 }
113
114 if (nMaxInd != 1)
115 {
116 std::swap(c[1], c[nMaxInd]);
117 *j--; // undo last watch
118 watches[~c[1]].push(w);
119 }
120
121 //----------------------
122 //curProLits.push(first);
123 //curProCrefs.push(cr);
124 //curProLevel.push(nMaxLevel);
125 //----------------------
126
127 uncheckedEnqueue(first, nMaxLevel, cr);
128 #ifdef PRINT_OUT
129 std::cout << "i " << first << " l " << nMaxLevel << "\n";
130 #endif
131 }
132 }
133
134 NextClause:;
135 }
136 /*
137 //---------------------------------------------------------------------
138 //尝试将这些传播文字按照出现频率从低到高排序后依次进入trail中
139 //前面赋值变元多,对于出现频率高变元会有更多单元子句形成
140 //暂未实行排序
141 for(int i = 0; i < curProLits.size(); i++)
142 {
143 Lit proLit = curProLits[i];
144 //value(proLit) == l_Undef;
145 CRef proCRef = curProCrefs[i];
146 int proLevel = curProLevel[i];
147 uncheckedEnqueue(proLit, proLevel, proCRef);
148 }
149 //---------------------------------------------------------------------
150 */
151
152 ws.shrink(i - j);
153 }
154
155 ExitProp:;
156 propagations += num_props;
157 simpDB_props -= num_props;
158
159 return confl;
160 }
propagate()
|
|
标签：++,认知,watches,first,2020,push,cr,观察,size 来源： https://www.cnblogs.com/yuweng1689/p/12837421.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。