|
一、观察体系的基本数据结构： ---------------------------------------------------------------------------------------------------------------------------------- 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()
|
|