necessaryAssignment: use every 4 attempts

Signed-off-by: Norbert Manthey <[email protected]>
conp-solutions · May 11, 2022 · 834c74e · 834c74e
1 parent 660ba90
commit 834c74e
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
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)",
-                                     0,
+                                     4,
                                      IntRange(0, INT32_MAX));
 static IntOption opt_na_recheckInc(_cat,
                                    "na-recheck-every",
@@ -3693,12 +3693,16 @@ void Solver::diversify(int rank, int size)
     if (rank == 1) {
         /* initialize activity as in v3 */
         init_act = 0;
+        /* do not use necessary assignment */
+        nAssignment.setAttemptEvery(0);
     }
     if (rank == 2) {
         /* do not use SLS, and initialize activities as in v3 */
         init_act = 0;
         use_ccnr = false;
         state_change_time = 1000000000;
+        /* do not use necessary assignment */
+        nAssignment.setAttemptEvery(0);
     }
     if (rank < 3) return;
 
@@ -3707,6 +3711,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 % 11 == 4) init_act = 0;
     if (rank % 11 == 7) init_act = 3;
     if (rank % 13 == 8) {

diff --git a/minisat/core/Solver.h b/minisat/core/Solver.h
@@ -713,6 +713,9 @@ class Solver
 
         /// Check decision literal next on level 1 for necessary assignments in its clauses
         bool checkNecessaryAssignment(Lit next, CRef &confl);
+
+        /// allow to set attemptEvery
+        void setAttemptEvery(int attemptEvery) { attempt_every = attemptEvery; }
     };
     NecessaryAssignments nAssignment;