位置：
E:\CNKI E-Study\localestudy\Literature\SAT求解器学习_6B1FE1DF69904FE2AEC3542DCF408574\VSIDS paper\VISDS-solvers\vsids-master-1\vsids-master-1\countbridgemvsids\core
代码解读
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\n"), exit(1);
5 FILE* cmty_file = fopen(opt_cmty_file, "r");
6 if (cmty_file == NULL)
7 fprintf(stderr, "could not open file %s\n", (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\n", &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\n", nBridges);
36 printf("Variables : %d\n", 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 ]==============================\n");
53 printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
54 printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
55 printf("===============================================================================\n");
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("==========================================================\n");
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 |
原文地址：https://www.cnblogs.com/yuweng1689/p/12695216.html
时间： 2024-10-01 01:36:01