Revert "necessaryAssignment: use every 4 attempts"

Switch the default configuration back to the original setting. This reverts commit 834c74e.
conp-solutions · Apr 4, 2023 · d28c208 · d28c208
1 parent 3539e13
commit d28c208
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
@@ -235,7 +235,7 @@ opt_na_maxCls(_cat, "na-max-cls", "Test at most X binary clauses for necessary a
 static IntOption opt_na_attemptEvery(_cat,
                                      "na-attempt-every",
                                      "Attempt necessary assignment every X-th level 1 decision (0 == off)",
-                                     4,
+                                     0,
                                      IntRange(0, INT32_MAX));
 static IntOption opt_na_recheckInc(_cat,
                                    "na-recheck-every",
@@ -3699,8 +3699,6 @@ void Solver::diversify(int rank, int size)
         init_act = 0;
         use_ccnr = false;
         state_change_time = 1000000000;
-        /* do not use necessary assignment */
-        nAssignment.setAttemptEvery(0);
     }
     if (rank < 3) return;
 
@@ -3709,7 +3707,7 @@ void Solver::diversify(int rank, int size)
     if (rank % 5 == 2) restart = Restart(0);
     if (rank % 5 == 3) restart = Restart(1);
     if (rank % 7 == 3) core_lbd_cut = 4;
-    if (rank % 7 == 6) nAssignment.setAttemptEvery(0);
+    if (rank % 7 == 6) nAssignment.setAttemptEvery(4);
     if (rank % 11 == 4) init_act = 0;
     if (rank % 11 == 7) init_act = 3;
     if (rank % 13 == 8) {