From 72165e4b6fc188ac2ff977c105e966bdb785c3fa Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Thu, 20 Apr 2023 14:57:18 +0800 Subject: [PATCH] =?UTF-8?q?=E4=BF=AE=E5=A4=8D=E4=B8=80=E4=BA=9B=E9=97=AE?= =?UTF-8?q?=E9=A2=98?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/sharer.cpp | 2 ++ src/solve.cpp | 6 +++--- 2 files changed, 5 insertions(+), 3 deletions(-) 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);