最早使用cmt的minisat改进版求解器3——vsids-master-1countbridgemvsids

Posted yuweng1689

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了最早使用cmt的minisat改进版求解器3——vsids-master-1countbridgemvsids相关的知识,希望对你有一定的参考价值。

位置:

E:CNKI E-StudylocalestudyLiteratureSAT求解器学习_6B1FE1DF69904FE2AEC3542DCF408574VSIDS paperVISDS-solversvsids-master-1vsids-master-1countbridgemvsidscore

代码解读


 

Solver.h

  1 class Solver {
 ...100 
101     // Statistics: (read-only member variable)
102     //
103     uint64_t solves, starts, decisions, bridge_decisions, rnd_decisions, propagations, conflicts, backjumps;
104     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
105     uint64_t learnt_clause_vars, bridge_learnt_clause_vars, cag_vars, bridge_cag_vars;
...
178 
179     vec<bool> bridges;
...
239 };
 

 

Solver.cpp

 1 Solver::Solver() :
...
33   , learnt_clause_vars (0)
34   , bridge_learnt_clause_vars(0)
35   , cag_vars           (0)
36   , bridge_cag_vars    (0)
...54 {}
技术图片
  1 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
  2 {
  3     int pathC = 0;
  4     Lit p     = lit_Undef;
  5 
  6     // Generate conflict clause:
  7     //
  8     out_learnt.push();      // (leave room for the asserting literal)
  9     int index   = trail.size() - 1;
 10 
 11     do{
 12         assert(confl != CRef_Undef); // (otherwise should be UIP)
 13         Clause& c = ca[confl];
 14 
 15         if (c.learnt())
 16             claBumpActivity(c);
 17 
 18         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
 19             Lit q = c[j];
 20 
 21             if (!seen[var(q)] && level(var(q)) > 0){
 22                 varBumpActivity(var(q));
 23                 if (bridges[var(q)]) {
 24                     bridge_cag_vars++;
 25                 }
 26                 cag_vars++;
 27                 seen[var(q)] = 1;
 28                 if (level(var(q)) >= decisionLevel())
 29                     pathC++;
 30                 else
 31                     out_learnt.push(q);
 32             }
 33         }
 34         
 35         // Select next clause to look at:
 36         while (!seen[var(trail[index--])]);
 37         p     = trail[index+1];
 38         confl = reason(var(p));
 39         seen[var(p)] = 0;
 40         pathC--;
 41 
 42     }while (pathC > 0);
 43     out_learnt[0] = ~p;
 44 
 45     // Simplify conflict clause:
 46     //
 47     int i, j;
 48     out_learnt.copyTo(analyze_toclear);
 49     if (ccmin_mode == 2){
 50         uint32_t abstract_level = 0;
 51         for (i = 1; i < out_learnt.size(); i++)
 52             abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
 53 
 54         for (i = j = 1; i < out_learnt.size(); i++)
 55             if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
 56                 out_learnt[j++] = out_learnt[i];
 57         
 58     }else if (ccmin_mode == 1){
 59         for (i = j = 1; i < out_learnt.size(); i++){
 60             Var x = var(out_learnt[i]);
 61 
 62             if (reason(x) == CRef_Undef)
 63                 out_learnt[j++] = out_learnt[i];
 64             else{
 65                 Clause& c = ca[reason(var(out_learnt[i]))];
 66                 for (int k = 1; k < c.size(); k++)
 67                     if (!seen[var(c[k])] && level(var(c[k])) > 0){
 68                         out_learnt[j++] = out_learnt[i];
 69                         break; }
 70             }
 71         }
 72     }else
 73         i = j = out_learnt.size();
 74 
 75     max_literals += out_learnt.size();
 76     out_learnt.shrink(i - j);
 77     tot_literals += out_learnt.size();
 78 
 79     // Find correct backtrack level:
 80     //
 81     if (out_learnt.size() == 1)
 82         out_btlevel = 0;
 83     else{
 84         int max_i = 1;
 85         // Find the first literal assigned at the next-highest level:
 86         for (int i = 2; i < out_learnt.size(); i++)
 87             if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
 88                 max_i = i;
 89         // Swap-in this literal at index 1:
 90         Lit p             = out_learnt[max_i];
 91         out_learnt[max_i] = out_learnt[1];
 92         out_learnt[1]     = p;
 93         out_btlevel       = level(var(p));
 94     }
 95 
 96     for (int i = 0; i < out_learnt.size(); i++) {
 97         Var v = var(out_learnt[i]);
 98         if (bridges[v]) {
 99             bridge_learnt_clause_vars++;
100         }
101         learnt_clause_vars++;
102     }
103 
104     for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // (‘seen[]‘ is now cleared)
105 }
void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel)

 关注分析函数中的新增统计量:learnt_clause_vars, bridge_learnt_clause_vars, cag_vars, bridge_cag_vars;

 1 lbool Solver::solve_()
 2 {
 3     if (!opt_cmty_file)
 4         fprintf(stderr, "missing community file
"), exit(1);
 5     FILE* cmty_file = fopen(opt_cmty_file, "r");
 6     if (cmty_file == NULL)
 7         fprintf(stderr, "could not open file %s
", (const char*) opt_cmty_file), exit(1);
 8 
 9     vec<int> cmtys (nVars());
10     int v;
11     int cmty;
12     while (fscanf(cmty_file, "%d %d
", &v, &cmty) == 2) {
13         cmtys[v] = cmty;
14     }
15     for (int i = 0; i < nClauses(); i++) {
16         Clause& c = ca[clauses[i]];
17         if (c.size() > 0) {
18             for (int j = 0; j < c.size(); j++) {
19                 Var varJ = var(c[j]);
20                 for (int k = j + 1; k < c.size(); k++) {
21                     Var varK = var(c[k]);
22                     if (cmtys[varJ] != cmtys[varK]) {
23                         bridges[varJ] = true;
24                         bridges[varK] = true;
25                     }
26                 }
27             }
28         }
29     }
30     int nBridges = 0;
31     for (int i = 0; i < bridges.size(); i++) {
32         if (bridges[i]) nBridges++;
33     }
34 
35     printf("Bridges   : %d
", nBridges);
36     printf("Variables : %d
", nVars());
37 
38     fclose(cmty_file);
39 
40     model.clear();
41     conflict.clear();
42     if (!ok) return l_False;
43 
44     solves++;
45 
46     max_learnts               = nClauses() * learntsize_factor;
47     learntsize_adjust_confl   = learntsize_adjust_start_confl;
48     learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
49     lbool   status            = l_Undef;
50 
51     if (verbosity >= 1){
52         printf("============================[ Search Statistics ]==============================
");
53         printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
");
54         printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
");
55         printf("===============================================================================
");
56     }
57 
58     // Search:
59     int curr_restarts = 0;
60     while (status == l_Undef){
61         double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
62         status = search(rest_base * restart_first);
63         if (!withinBudget()) break;
64         curr_restarts++;
65     }
66 
67     if (verbosity >= 1)
68         printf("==========================================================
");
69 
70 
71     if (status == l_True){
72         // Extend & copy model:
73         model.growTo(nVars());
74         for (int i = 0; i < nVars(); i++) model[i] = value(i);
75     }else if (status == l_False && conflict.size() == 0)
76         ok = false;
77 
78     cancelUntil(0);
79     return status;
80 }

重点关注:cmtys     cmty_file    bridges

 
 

以上是关于最早使用cmt的minisat改进版求解器3——vsids-master-1countbridgemvsids的主要内容,如果未能解决你的问题,请参考以下文章

本人研究sat求解器数据信息汇总

本人研究sat求解器数据信息汇总

CMT2380F32模块开发1-硬件

CMT2380F32模块开发1-硬件

CMT2380F32模块开发17-ADC例程

CMT2380F32模块开发17-ADC例程