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

 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 ...

 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 ...

 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 ...

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 }