diff --git a/src/sharer.cpp b/src/sharer.cpp index 696759f..c6577c9 100644 --- a/src/sharer.cpp +++ b/src/sharer.cpp @@ -218,8 +218,10 @@ void sharer::do_clause_sharing() { if(clause_imported[cls[i]->hash_code()]) { std::swap(cls[i], cls[t_size-1]); t_size--; + i--; } } + cls.resize(t_size); //分享当前节点产生的子句 diff --git a/src/solve.cpp b/src/solve.cpp index 42843fe..c936609 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -80,7 +80,7 @@ void light::diversity_workers() { workers[i]->configure("stable", 1); workers[i]->configure("target", 2); workers[i]->configure("phase", 1); - workers[i]->configure("heuristic", 0); + // workers[i]->configure("heuristic", 0); if (i == 2) workers[i]->configure("stable", 0); @@ -103,11 +103,11 @@ void light::diversity_workers() { // workers[i]->configure("walkinitially", 0); workers[i]->configure("target", 1); // workers[i]->configure("phase", 1); - workers[i]->configure("heuristic", 0); + // workers[i]->configure("heuristic", 0); // workers[i]->configure("margin", 1)0; if (i == 0 || i == 1 || i == 7 || i == 8 || i == 11 || i == 15) - workers[i]->configure("heuristic", 1); + // workers[i]->configure("heuristic", 1); if (i == 3 || i == 6 || i == 8 || i == 11 || i == 12 || i == 13) workers[i]->configure("chrono", 0);