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

Posted yuweng1689

tags:

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

位置:

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

 

代码分析


Solver.h

  1 //============================================
  2 // Solver -- the main class:
  3 
  4 class Solver {
  5 public:
  ...
 23 
 24     bool      save_decision_trail;   // Whether to save decision trail
 25     bool      save_learned_clauses;   // Whether to save learned clauses
 26     bool      conflicting_vars_analysis;
 ...
 53     void    writeDecisionVar(Var next);
 54     void    writeLearnedClause(vec<Lit>& out_learnt);
 55     void    updateConflictAnalysis(Var v);
 56     void    updateConflictAnalysis(vec<Lit>& c);
 57 
 58     // Track solver behavior
 59     FILE* decision_trail_file;
 60     FILE* learned_clauses_file;
 ...120 
121     //XXX EXPERIMENT
122     std::vector<int> conflicting_vars_count;
123     std::vector< std::vector<double> > conflicting_vars_graph;
...
255 };
 1 inline void Solver::writeDecisionVar(Var next) {
 2     if (save_decision_trail) {
 3         assert((next != var_Undef) && (next>=0) && (next<=nVars()));
 4         // +1 is necessary because MiniSAT stores variables naming from 0 not 1
 5         //fprintf(decision_trail_file, "%d ", next+1);
 6         fprintf(decision_trail_file, "%d
", next);
 7     }
 8 }
 9 
10 inline void Solver::writeLearnedClause(vec<Lit>& out_learnt) {
11     if (save_learned_clauses) {
12         for(int i = 0; i < out_learnt.size(); i++)
13             fprintf(learned_clauses_file, "%d ", var(out_learnt[i]));
14         fprintf(learned_clauses_file, "
");
15     }
16 }
17 
18 inline void Solver::updateConflictAnalysis(Var v) {
19     if (conflicting_vars_analysis) {
20         // +1 at end is necessary because MiniSAT stores variables naming from 0 not 1
21         conflicting_vars_count[v] += 1;
22     }
23 }
24 
25 inline void Solver::updateConflictAnalysis(vec<Lit>& c) {
26     if (conflicting_vars_analysis) {
27         int l,h;
28         //printf("asdf
");
29         // +1 at end is necessary because MiniSAT stores variables naming from 0 not 1
30         for(int i = 0; i < c.size()-1; i++)
31             for(int j = i + 1; j < c.size(); j++){
32                 if(var(c[i]) < var(c[j])){
33                     l = var(c[i]);
34                     h = var(c[j]);
35                 }
36                 else{
37                     l = var(c[j]);
38                     h = var(c[i]);
39                 }
40                 //printf("%d %d
",l,h);
41                 //XXX probably should change increment to correlate with clause size
42                 conflicting_vars_graph[l][h-l-1] += 1;
43             }
44 
45     }
46 }

Solver.h中新增用于观察性能的代码段

 

Solver.cc

技术图片
 1 lbool Solver::search(int nof_conflicts)
 2 {
 3     assert(ok);
 4     int         backtrack_level;
 5     int         conflictC = 0;
 6     vec<Lit>    learnt_clause;
 7     starts++;
 8 
 9     for (;;){
10         CRef confl = propagate();
11         if (confl != CRef_Undef){
12             // CONFLICT
13             conflicts++; conflictC++;
14             if (decisionLevel() == 0) return l_False;
15 
16             learnt_clause.clear();
17             analyze(confl, learnt_clause, backtrack_level);
18             cancelUntil(backtrack_level);
19 
20             if (learnt_clause.size() == 1){
21                 uncheckedEnqueue(learnt_clause[0]);
22             }else{
23                 CRef cr = ca.alloc(learnt_clause, true);
24                 learnts.push(cr);
25                 attachClause(cr);
26                 claBumpActivity(ca[cr]);
27                 uncheckedEnqueue(learnt_clause[0], cr);
28             }
29 
30             varDecayActivity();
31             claDecayActivity();
32 
33             if (--learntsize_adjust_cnt == 0){
34                 learntsize_adjust_confl *= learntsize_adjust_inc;
35                 learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
36                 max_learnts             *= learntsize_inc;
37 
38                 if (verbosity >= 1)
39                     printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |
", 
40                            (int)conflicts, 
41                            (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
42                            (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
43             }
44 
45         }else{
46             // NO CONFLICT
47             if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
48                 // Reached bound on number of conflicts:
49                 progress_estimate = progressEstimate();
50                 cancelUntil(0);
51                 return l_Undef; }
52 
53             // Simplify the set of problem clauses:
54             if (decisionLevel() == 0 && !simplify())
55                 return l_False;
56 
57             if (learnts.size()-nAssigns() >= max_learnts)
58                 // Reduce the set of learnt clauses:
59                 reduceDB();
60 
61             Lit next = lit_Undef;
62             while (decisionLevel() < assumptions.size()){
63                 // Perform user provided assumption:
64                 Lit p = assumptions[decisionLevel()];
65                 if (value(p) == l_True){
66                     // Dummy decision level:
67                     newDecisionLevel();
68                 }else if (value(p) == l_False){
69                     analyzeFinal(~p, conflict);
70                     return l_False;
71                 }else{
72                     next = p;
73                     break;
74                 }
75             }
76 
77             if (next == lit_Undef){
78                 // New variable decision:
79                 decisions++;
80                 next = pickBranchLit();
81 
82 
83                 if (next == lit_Undef)
84                     // Model found:
85                     return l_True;
86                 else
87                     writeDecisionVar(var(next));
88             }
89 
90             // Increase decision level and enqueue ‘next‘
91             newDecisionLevel();
92             uncheckedEnqueue(next);
93         }
94     }
95 }
lbool Solver::search(int nof_conflicts)

 函数writeDecisionVar(var(next))调用

 技术图片void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel)

发生以下函数调用:

updateConflictAnalysis(var(out_learnt[i]));  updateConflictAnalysis(out_learnt);  writeLearnedClause(out_learnt);

 
1 Solver::~Solver()
2 {
3     if(save_decision_trail)
4         fclose(decision_trail_file);
5 }

备注:    bool   save_decision_trail;   // Whether to save decision trail

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

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

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

z3求解器和求解器给出不同的结果

Xilinx PLL(Virtex-5)

matlab改进遗传算法求解带时间窗的路径优化问题

CMT2380F32模块开发17-ADC例程