子句重复生成相关代码解析

2022-09-17 00:32:38 阅读：259 来源： 互联网

标签：tmp duplicates 代码 duplicate ht learnts 子句解析 size

1. 定期管理 ht ——子句重复性所在的哈希表

 1 //lbool Solver::solve_()
 2 ...
 3 
 4 if (dupl_db_size >= dupl_db_size_limit){    
 5     printf("c Duplicate learnts added (Minimization) %i.\n",duplicates_added_minimization);
 6     printf("c Duplicate learnts added (conflicts) %i.\n",duplicates_added_conflicts); 
 7     printf("c Duplicate learnts added (tier2) %i.\n",duplicates_added_tier2);
 8     printf("c Duptime: %i\n",duptime.count());
 9     printf("c Number of conflicts: %i\n",conflicts);
10     printf("c Core size: %i\n",learnts_core.size());
11             
12     uint32_t removed_duplicates = 0;
13     std::vector<std::vector<uint64_t>> tmp;
14     //std::map<int32_t,std::map<uint32_t,std::unordered_map<uint64_t,uint32_t>>>  ht;
15     for (auto & outer_mp: ht){//variables
16         for (auto &inner_mp:outer_mp.second){//sizes
17             for (auto &in_in_mp: inner_mp.second){
18               if (in_in_mp.second >= min_number_of_learnts_copies){
19                  tmp.push_back({
                                    outer_mp.first,
                                    inner_mp.first,
                                    in_in_mp.first,
                                    in_in_mp.second });
20               }
21             }
22          }
23     }
24     removed_duplicates = dupl_db_size-tmp.size(); 
25     ht.clear();
26     for (auto i=0;i<tmp.size();i++){
27         ht[tmp[i][0]][tmp[i][1]][tmp[i][2]]=tmp[i][3];
28     }
29     //ht_old.clear();
30     dupl_db_size_limit*=1.1;
31     dupl_db_size -= removed_duplicates;
32     printf("c removed duplicate db entries %i\n",removed_duplicates);
33 }
34 
35 ...

2. 化简函数中考察当前子句集每一个子句c重复出现次数id，并做相应的处理

 1 //bool Solver::simplifyLearnt_tier2()
 2 ...
 3 
 4                     //duplicate learnts
 5                     int id = 0; 
 6                     
 7                     std::vector<uint32_t> tmp;
 8                     for (int i = 0; i < c.size(); i++)
 9                         tmp.push_back(c[i].x);  // Lit定义文字对应的数据成员 int x;
10                     id = is_duplicate(tmp);
11                      
12                                         
13                     //duplicate learnts 
14 
15                     if (id < min_number_of_learnts_copies+2){
16                         attachClause(cr);
17                         learnts_tier2[cj++] = learnts_tier2[ci];
18                         if (id == min_number_of_learnts_copies+1){
19                             duplicates_added_minimization++;
20                         }
21                         if ((c.lbd() <= core_lbd_cut)||
                                          (id == min_number_of_learnts_copies+1)){
22                         //if (id == min_number_of_learnts_copies+1){
23                             cj--;
24                             learnts_core.push(cr);
25                             c.mark(CORE);
26                         }
27 
28                         c.setSimplified(true);
29                     }
30                 }
31             }
32         }
33     }
34     learnts_tier2.shrink(ci - cj);
35 
36 ...

3. search函数中，考察当新生学习子句c是否重复出现，如果重复出现则在函数is_duplicate(std::vector<uint32_t>&c)中

           it2->second++;  //将该子句重复出现计数值增加1.

 1 //lbool Solver::search(int& nof_conflicts)
 2 ...
 3 
 4            if (learnt_clause.size() == 1){
 5                 uncheckedEnqueue(learnt_clause[0]);
 6             }else{
 7                 CRef cr = ca.alloc(learnt_clause, true);
 8                 ca[cr].set_lbd(lbd);
 9                 //duplicate learnts 
10                 int  id = 0;
11                 if (lbd <= max_lbd_dup){                        
12                     std::vector<uint32_t> tmp;
13                     for (int i = 0; i < learnt_clause.size(); i++)
14                         tmp.push_back(learnt_clause[i].x);
15                     id = is_duplicate(tmp);             
16                     if (id == min_number_of_learnts_copies +1){
17                         duplicates_added_conflicts++;                        
18                     }                    
19                     if (id == min_number_of_learnts_copies){
20                         duplicates_added_tier2++;
21                     }                                        
22                 }
23                 //duplicate learnts
24 
25                 if ((lbd <= core_lbd_cut) || (id == min_number_of_learnts_copies+1)){
26                     learnts_core.push(cr);
27                     ca[cr].mark(CORE);
28                 }else if ((lbd <= 6)||(id == min_number_of_learnts_copies)){
29                     learnts_tier2.push(cr);
30                     ca[cr].mark(TIER2);
31                     ca[cr].touched() = conflicts;
32                 }else{
33                     learnts_local.push(cr);
34                     claBumpActivity(ca[cr]); }
35                 attachClause(cr);
36 
37                 uncheckedEnqueue(learnt_clause[0], backtrack_level, cr);
38 #ifdef PRINT_OUT
39                 std::cout << "new " << ca[cr] << "\n";
40                 std::cout << "ci " << learnt_clause[0] << " l " << backtrack_level << "\n";
41 #endif                
42             }
43 
44 ...

4. 函数 is_duplicate(std::vector<uint32_t>&c) 及其主要数据量ht

1 //Solver.h
2 
3 // duplicate learnts version
4 std::map<int32_t,std::map<uint32_t,std::unordered_map<uint64_t,uint32_t>>>  ht;

// duplicate learnts version

uint32_t min_number_of_learnts_copies;
uint32_t dupl_db_init_size;
uint32_t max_lbd_dup;
std::chrono::microseconds duptime;

// duplicate learnts version

uint64_t duplicates_added_conflicts;
uint64_t duplicates_added_tier2;
uint64_t duplicates_added_minimization;
uint64_t dupl_db_size;

5 // duplicate learnts version 
6 int is_duplicate (std::vector<uint32_t>&c); //returns TRUE if a clause is duplicate 
7 // duplicate learnts version

//size_t dupl_db_size_limit = dupl_db_init_size;

//dupl_db_size_limit*=1.1;

 1 int Solver::is_duplicate(std::vector<uint32_t>&c){
 2     auto time_point_0 = std::chrono::high_resolution_clock::now();
 3     dupl_db_size++;
 4     int res = 0;    
 5     
 6     int sz = c.size();
 7     std::vector<uint32_t> tmp(c);    
 8     sort(tmp.begin(),tmp.end());
 9     
10     uint64_t hash = 0;    
11     
12     for (int i =0; i<sz; i++) {
13         hash ^= tmp[i] + 0x9e3779b9 + (hash << 6) + (hash>> 2); 
14     }    
15     
16     int32_t head = tmp[0];
17     auto it0 = ht.find(head);
18     if (it0 != ht.end()){
19         auto it1=ht[head].find(sz);
20         if (it1 != ht[head].end()){
21             auto it2 = ht[head][sz].find(hash);
22             if (it2 != ht[head][sz].end()){
23                 it2->second++;
24                 res = it2->second;            
25             }
26             else{
27                 ht[head][sz][hash]=1;
28             }
29         }
30         else{            
31             ht[head][sz][hash]=1;
32         }
33     }else{        
34         ht[head][sz][hash]=1;
35     } 
36     auto time_point_1 = std::chrono::high_resolution_clock::now();
37     duptime += std::chrono::duration_cast<std::chrono::microseconds>(
                                                          time_point_1-time_point_0);
38     return res;
39 }

标签：tmp,duplicates,代码,duplicate,ht,learnts,子句,解析,size
来源： https://www.cnblogs.com/yuweng1689/p/16701725.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

ICode9

子句重复生成相关代码解析