有向无环图节点可见性的使用——蕴含图的切割技巧

 1 decisions: 25;  decision var: -2
 2 the size of trail is 28. : 1 -6 -27 -2 -22 -23 -20 -13 -10 -28 25 29 14 7 -3 18 -4 16 17 -9
                                5 24 11 12 -8 21 -15 26
 3 the size of trail_lim is 2 : 1 3
 4 the implied lit is : -22
 5 the implied clause is: [-22 2 27 ]
 6 the implied lit is : -23
 7 the implied clause is: [-23 22 6 ]
 8 the implied lit is : -20
 9 the implied clause is: [-20 23 -1 ]
10 the implied lit is : -13
11 the implied clause is: [-13 20 2 ]
12 the implied lit is : -10
13 the implied clause is: [-10 20 6 ]
14 the implied lit is : -28
15 the implied clause is: [-28 13 20 ]
16 the implied lit is : 25
17 the implied clause is: [25 10 2 ]
18 the implied lit is : 29
19 the implied clause is: [29 28 27 ]
20 the implied lit is : 14
21 the implied clause is: [14 28 27 ]
22 the implied lit is : 7
23 the implied clause is: [7 -25 ]
24 the implied lit is : -3
25 the implied clause is: [-3 -25 ]
26 the implied lit is : 18
27 the implied clause is: [18 -25 2 ]
28 the implied lit is : -4
29 the implied clause is: [-4 -14 -29 ]
30 the implied lit is : 16
31 the implied clause is: [16 -14 -1 ]
32 the implied lit is : 17
33 the implied clause is: [17 -14 10 ]
34 the implied lit is : -9
35 the implied clause is: [-9 -14 10 ]
36 the implied lit is : 5
37 the implied clause is: [5 -7 28 ]
38 the implied lit is : 24
39 the implied clause is: [24 -7 13 ]
40 the implied lit is : 11
41 the implied clause is: [11 -7 22 ]
42 the implied lit is : 12
43 the implied clause is: [12 -7 23 ]
44 the implied lit is : -8
45 the implied clause is: [-8 -7 9 ]
46 the implied lit is : 21
47 the implied clause is: [21 3 -1 ]
48 the implied lit is : -15
49 the implied clause is: [-15 3 28 ]
50 the implied lit is : 26
51 the implied clause is: [26 -18 -29 ]
52 
53 the conflict index of trail is : 16
54 the conflict liter is : -4
55 the tow clauses get confliction each other-----
56 the conflict reason clause is: [-4 -14 -29 ]
57 the confl clause is: [-21 4 -14 ]
58 
59 the learnt clause is : [ 2  6 ]
60 
61 backtrack_level:1
62 
63 decisions: 26;  decision var: 2
64 the size of trail is 16. : 1 -6 -27 2 -29 -7 28 -23 -25 19 10 -26 -18 -20 -14 24
65 the size of trail_lim is 1 : 1
66 the implied lit is : -29
67 the implied clause is: [-29 -2 6 ]
68 the implied lit is : -7
69 the implied clause is: [-7 -2 -1 ]
70 the implied lit is : 28
71 the implied clause is: [28 29 27 ]
72 the implied lit is : -23
73 the implied clause is: [7 -23 ]
74 the implied lit is : -25
75 the implied clause is: [7 -25 ]
76 the implied lit is : 19
77 the implied clause is: [7 19 ]
78 the implied lit is : 10
79 the implied clause is: [10 7 -2 ]
80 the implied lit is : -26
81 the implied clause is: [-26 -28 23 ]
82 the implied lit is : -18
83 the implied clause is: [-18 23 -2 ]
84 the implied lit is : -20
85 the implied clause is: [-20 23 -1 ]
86 the implied lit is : -14
87 the implied clause is: [-14 23 29 ]
88 the implied lit is : 24
89 the implied clause is: [24 -10 29 ]
90 
91 the conflict index of trail is : 10
92 the conflict liter is : 10
93 the tow clauses get confliction each other-----
94 the conflict reason clause is: [10 7 -2 ]
95 the confl clause is: [20 -10 6 ]
96 
97 the learnt clause is : [ 6 ]
98 
99 backtrack_level:0

 1 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, int& out_lbd)
 2 {
 3     int pathC = 0;
 4     Lit p     = lit_Undef;
 5 
 6     // Generate conflict clause:   
 7     out_learnt.push();      // (leave room for the asserting literal)
 8     int index   = trail.size() - 1;
 9     int nDecisionLevel = level(var(ca[confl][0]));
10     assert(nDecisionLevel == level(var(ca[confl][0])));
11 
12     do{
13         assert(confl != CRef_Undef); // (otherwise should be UIP)
14         Clause& c = ca[confl];
15 
16         // For binary clauses, we don't rearrange literals in propagate(), 
17     // so check and make sure the first is an implied lit.
18         if (p != lit_Undef && c.size() == 2 && value(c[0]) == l_False){
19             assert(value(c[1]) == l_True);
20             Lit tmp = c[0];
21             c[0] = c[1], c[1] = tmp; }
22 
23         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
24             Lit q = c[j];            
25 
26             if (!seen[var(q)] && level(var(q)) > 0){
27                 if (VSIDS){
28                     varBumpActivity(var(q), .5);
29                     add_tmp.push(q);  //收集参与冲突的文字
30                 }else
31                     conflicted[var(q)]++;
32                 seen[var(q)] = 1;
33                 if (level(var(q)) >= nDecisionLevel){
34                     pathC++;
35                 }else
36                     out_learnt.push(q);
37             }        
38         }
39         
40         // Select next clause to look at:
41     do {
42         while (!seen[var(trail[index--])]);
43         p  = trail[index+1];
44     } while (level(var(p)) < nDecisionLevel);
45         
46         confl = reason(var(p));
47         seen[var(p)] = 0;
48         pathC--;
49 
50     }while (pathC > 0);
51     out_learnt[0] = ~p;    
52     
53     
54     out_learnt.copyTo(analyze_toclear);
55 
56     // Simplify conflict clause:
57  
58     // Try further minimization?
59         
60     // Recompute LBD if minimized.
61 
62     // Find correct backtrack level:
63    
64     for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; 
65                          // ('seen[]' is now cleared)
66 }

// pathCs[k] is the number of variables assigned at level k,
// it is initialized to 0 at the begining and reset to 0 after the function execution
bool Solver::collectFirstUIP(CRef confl){
    involved_lits.clear();
    int max_level=1;
    Clause& c = ca[confl]; 
    int minLevel = decisionLevel();
    for(int i=0; i<c.size(); i++) {
        Var v = var(c[i]);
        //        assert(!seen[v]);
        if (level(v)>0) {
            seen[v] = 1;
            var_iLevel_tmp[v] = 1;
            pathCs[level(v)]++;        
            if (minLevel>level(v)) {
                minLevel=level(v);
                assert(minLevel>0);
            }
            //    varBumpActivity(v);
        }
    }

    int limit=trail_lim[minLevel-1];
    for(int i=trail.size()-1; i>=limit; i--) {
        Lit p=trail[i]; Var v=var(p);
        if (seen[v]) {
            int currentDecLevel=level(v);
            //      if (currentDecLevel==decisionLevel())
            //          varBumpActivity(v);
            seen[v]=0;
            if (--pathCs[currentDecLevel]!=0) {
                Clause& rc=ca[reason(v)];
                int reasonVarLevel = var_iLevel_tmp[v] + 1;
                if(reasonVarLevel>max_level) max_level = reasonVarLevel;
                if (rc.size()==2 && value(rc[0])==l_False) {
                    // Special case for binary clauses
                    // The first one has to be SAT
                    assert(value(rc[1]) != l_False);
                    Lit tmp = rc[0];
                    rc[0] =  rc[1], rc[1] = tmp;
                }
                for (int j = 1; j < rc.size(); j++){
                    Lit q = rc[j]; Var v1=var(q);
                    if (level(v1) > 0) {
                        if (minLevel>level(v1)) {
                            minLevel=level(v1); 
                            limit=trail_lim[minLevel-1];     assert(minLevel>0);
                        }
                        if (seen[v1]) {
                            if (var_iLevel_tmp[v1]<reasonVarLevel)
                                var_iLevel_tmp[v1]=reasonVarLevel;
                        }
                        else {
                            var_iLevel_tmp[v1]=reasonVarLevel;
                            //   varBumpActivity(v1);
                            seen[v1] = 1;
                            pathCs[level(v1)]++;               
                        }
                    }
                }
            }
            involved_lits.push(p);
        }
    }
    double inc = var_iLevel_inc;    

    .....

}