代码解读——给定已知赋值文字序列较由求解函数solveLimited传播并处理冲突

Posted 2020-12-17 yuweng1689

在主函数main.cc中

             在化简求解代码段之后：

vec<Lit> dummy;
lbool ret = S.solveLimited(dummy);

在Solver.h文件中

             inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }

在Solver.cc文件中的search函数中有如下使用代码。

 1         //在处理confil==CRef_Undef时
 2          。。。
 3          /*while (decisionLevel() < assumptions.size()){
 4                 // Perform user provided assumption:
 5                 Lit p = assumptions[decisionLevel()];
 6                 if (value(p) == l_True){
 7                     // Dummy decision level:
 8                     newDecisionLevel();
 9                 }else if (value(p) == l_False){
10                     analyzeFinal(~p, conflict);
11                     return l_False;
12                 }else{
13                     next = p;
14                     nextLit = next;  // update on 2020-03-10
15                     break;
16                 }
17             }
18 
19             if (next == lit_Undef)*/
20             。。。

相关函数analyzeFinal

 1 /*_________________________________________________________________________________________________
 2 |
 3 |  analyzeFinal : (p : Lit)  ->  [void]
 4 |  
 5 |  Description:
 6 |    Specialized analysis procedure to express the final conflict in terms of assumptions.
 7 |    Calculates the (possibly empty) set of assumptions that led to the assignment of ‘p‘, and
 8 |    stores the result in ‘out_conflict‘.
 9 |________________________________________________________________________________________________@*/
10 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
11 {
12     out_conflict.clear();
13     out_conflict.push(p);
14 
15     if (decisionLevel() == 0)
16         return;
17 
18     seen[var(p)] = 1;
19 
20     for (int i = trail.size()-1; i >= trail_lim[0]; i--){
21         Var x = var(trail[i]);
22         if (seen[x]){
23             if (reason(x) == CRef_Undef){
24                 assert(level(x) > 0);
25                 out_conflict.push(~trail[i]);
26             }else{
27                 Clause& c = ca[reason(x)];
28                 for (int j = c.size() == 2 ? 0 : 1; j < c.size(); j++)
29                     if (level(var(c[j])) > 0)
30                         seen[var(c[j])] = 1;
31             }
32             seen[x] = 0;
33         }
34     }
35 
36     seen[var(p)] = 0;
37 }