位置：
E:\CNKI E-Study\localestudy\Literature\SAT求解器学习_6B1FE1DF69904FE2AEC3542DCF408574\VSIDS paper\VISDS-solvers\vsids-master-1\vsids-master-1\minisat-performance\core
代码分析
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\n", 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, "\n");
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\n");
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\n",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 %% |\n",
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 |
原文地址：https://www.cnblogs.com/yuweng1689/p/12695078.html
时间： 2024-08-01 11:22:55