其他分享
首页 > 其他分享> > 子句重复生成相关代码解析

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

作者:互联网

 

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