二元子句归结的c++代码分析

 1 // Try further learnt clause minimization by means of binary clause resolution.
 2 bool Solver::binResMinimize(vec<Lit>& out_learnt)
 3 {
 4     // Preparation: remember which false variables we have in 'out_learnt'.
 5     counter++;
 6     for (int i = 1; i < out_learnt.size(); i++)
 7         seen2[var(out_learnt[i])] = counter;
 8 
 9     // Get the list of binary clauses containing 'out_learnt[0]'.
10     const vec<Watcher>& ws = watches_bin[~out_learnt[0]];
11 
12     int to_remove = 0;
13     for (int i = 0; i < ws.size(); i++){
14         Lit the_other = ws[i].blocker;
15         // Does 'the_other' appear negatively in 'out_learnt'?
16         if (seen2[var(the_other)] == counter && value(the_other) == l_True){
17             to_remove++;
18             seen2[var(the_other)] = counter - 1; // Remember to remove this variable.
19         }
20     }
21 
22     // Shrink.
23     if (to_remove > 0){
24         int last = out_learnt.size() - 1;
25         for (int i = 1; i < out_learnt.size() - to_remove; i++)
26             if (seen2[var(out_learnt[i])] != counter)
27                 out_learnt[i--] = out_learnt[last--];
28         out_learnt.shrink(to_remove);
29     }
30     return to_remove != 0;
31 }