其他分享
首页 > 其他分享> > 观察体系-观察-观察元知识概念的再认知2020-5-6

观察体系-观察-观察元知识概念的再认知2020-5-6

作者:互联网

 

 

 

一、观察体系的基本数据结构:

----------------------------------------------------------------------------------------------------------------------------------

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