feat : implement vsids overflow management

docs/cnf/4-queen-problem.cnf

@@ -0,0 +1,94 @@
+p cnf 16 81
+
+c At least one queen in each row
+  1   2   3   4   0
+  5   6   7   8   0
+  9  10  11  12   0
+ 13  14  15  16   0
+
+c At most one queen in each row
+ -1  -2   0
+ -1  -3   0
+ -1  -4   0
+ -2  -3   0
+ -2  -4   0
+ -3  -4   0
+ -5  -6   0
+ -5  -7   0
+ -5  -8   0
+ -6  -7   0
+ -6  -8   0
+ -7  -8   0
+ -9  -10  0
+ -9  -11  0
+ -9  -12  0
+ -10  -11 0
+ -10  -12 0
+ -11  -12 0
+ -13  -14 0
+ -13  -15 0
+ -13  -16 0
+ -14  -15 0
+ -14  -16 0
+ -15  -16 0
+
+c At least one queen in each column
+ 1  5  9  13  0
+ 2  6  10  14 0
+ 3  7  11  15 0
+ 4  8  12  16 0
+
+c At most one queen in each column
+ -1  -5   0
+ -1  -9   0
+ -1  -13  0
+ -5  -9   0
+ -5  -13  0
+ -9  -13  0
+ -2  -6   0
+ -2  -10  0
+ -2  -14  0
+ -6  -10  0
+ -6  -14  0
+ -10  -14 0
+ -3  -7   0
+ -3  -11  0
+ -3  -15  0
+ -7  -11  0
+ -7  -15  0
+ -11  -15 0
+ -4  -8   0
+ -4  -12  0
+ -4  -16  0
+ -8  -12  0
+ -8  -16  0
+ -12  -16 0
+
+c No queens on same diagonal (top-left to bottom-right)
+ -1  -6   0
+ -1  -11  0
+ -1  -16  0
+ -2  -7   0
+ -2  -12  0
+ -3  -8   0
+ -5  -10  0
+ -10 -15  0
+ -5  -15  0
+ -6  -11  0
+ -6  -16  0
+ -7  -12  0
+ -9  -14  0
+
+c No queens on same diagonal (top-right to bottom-left)
+ -4  -7   0
+ -4  -10  0
+ -4  -13  0
+ -3  -6   0
+ -3  -9   0
+ -2  -5   0
+ -8  -11  0
+ -8  -14  0
+ -7  -10  0
+ -7  -13  0
+ -6  -9   0
+ -12  -15 0

docs/cnf/README.md

@@ -0,0 +1,81 @@
+# CNF
+
+Those are CNF files representing probles that must be runneable from the CLI.
+Those are used for testing purposes and validation of the SAT solver which is part of the fabko solution
+
+## Simple Straightforward formula
+
+This is a simple formula that is used to test the most basic SAT solver.
+
+```cnf
+p cnf 3 2
+1 -3  0	
+2  3 -1  0 
+```
+
+This problem has many solutions and should be solved by the SAT solver even by accident.
+
+## propagation chain
+
+A CNF that resolve itself at the first propagation step.
+
+```cnf
+p cnf 4  4
+-1         0  
+ 1 -2      0
+ 1  2  -3  0
+ 3  4      0
+```
+
+[cnf file](propagation-chain.cnf)
+
+- the first clause is a unit clause that will be propagated,
+- the second clause will be resolved with the first one,
+- and the third clause will be resolved with the second one,
+- and the fourth clause will be resolved with the third one.
+
+## Conflict
+
+A CNF that has a conflict, it is used to test the SAT solver.
+
+```cnf
+p cnf 4 4
+-1  4       0
+-1  2       0
+-1  3       0
+-4 -2       0
+```
+
+This CNF should produce at least one conflict at resolution time.
+
+[cnf file](simple_conflict.cnf)
+
+## 4 queen problem
+
+Simple 4 queen problem that is used to test the SAT solver.
+The problem is to place 4 queens on a 4x4 chessboard such that no two queens threaten each other. This is a problem that
+contains 16 variables. one for each square of the 4x4 chessboard. Each variable represents whether a queen is placed on
+that square or not. The constraints ensure that no two queens are in the same row, column, or diagonal.
+
+There are 2 solutions to this problem, and the CNF file represents one of them.
+
+```txt
+
+cnf to be found in the file (too big to be included here)
+
+result SAT 1  : ~1 2 ~3 ~4 ~5 ~6 ~7 8 9 ~10 ~11 ~12 ~13 ~14 15 ~16
+
+ 0 1 0 0 
+ 0 0 0 1
+ 1 0 0 0
+ 0 0 1 0
+
+ result SAT 2 : ~1 ~2 3 ~4 5 ~6 ~7 ~8 ~9 ~10 ~11 12 ~13 14 ~15 ~16
+
+ 0 0 1 0
+ 1 0 0 0 
+ 0 0 0 1
+ 0 1 0 0
+```
+
+- [cnf file](4-queen-problem.cnf)

docs/cnf/propagation-chain.cnf

@@ -0,0 +1,5 @@
+p cnf 4  4
+    -1         0  
+     1 -2      0
+     1  2  -3  0
+     3  4      0

docs/cnf/simple_conflict.cnf

@@ -0,0 +1,7 @@
+p cnf 4 4
+
+        -1  4       0
+        -1  2       0
+        -1  3       0
+	    -4 -2       0
+

docs/cnf/simple_straight.cnf

@@ -0,0 +1,3 @@
+p cnf 3 2
+1 -3  0	
+2  3 -1  0

docs/cnf/test.cnf

@@ -0,0 +1,7 @@
+p cnf 4 4
+
+        -1  4       0
+        -1  2       0
+        -1  3       0
+	-4 -2       0	
+

fabko/compiler/backend/sat/solver_context.cpp

@@ -53,19 +53,38 @@ bool has_conflict(const Solver_Context& ctx, const Clause& clause) { // @todo re
 }
 
 /**
- * @brief Increase the VSIDS activity of the variables in the clause
+ * @brief Increase the VSIDS activity of the variables in the provided learned clause, then decrease the VSIDS activity of all variables if configured to do so.
+ * @note this function is called after a conflict (and the learned clause from the conflict resolution is the parameter 'learned_clause')
  * @note if the VSIDS activity is too high, to avoid overflow, every variable activity is divided by 1e100
- * @param ctx
- * @param clause
+ * @param ctx solving context to update the VSIDS activity of the variables
+ * @param learned_clause clause learned from the conflict resolution, the literals in this clause are used to increase the VSIDS activity of the variables
  */
-void increase_vsids_activity(Solver_Context& ctx, const Clause& clause) {
-    const auto& all_lit = clause.get_literals();
-    std::for_each(all_lit.begin(), all_lit.end(), [&ctx](const auto& lit) {
-        const auto& [_, varid]                                = lit;
-        auto varstruct                                        = ctx.vars_soa_[varid];
-        auto& [literal, assignment, assignment_context, meta] = varstruct;
-        assignment_context.vsids_activity_ += ctx.config_.vsids_increment; //@todo handle numerical overflow
+void update_vsids_activity(Solver_Context& ctx, const Clause& learned_clause) {
+    const auto& all_lit = learned_clause.get_literals();
+
+    const bool need_normalization = std::ranges::any_of(all_lit, [&ctx](const auto& lit) { // check if any variable activity is too high
+        const auto vsids_activity = get<soa_assignment_ctx>(ctx.vars_soa_[lit.second]).vsids_activity_;
+        return vsids_activity >= (std::numeric_limits<decltype(vsids_activity)>::max() - ctx.config_.vsids_increment);
     });
+    if (need_normalization) {
+        static constexpr auto NORMALIZATION_FACTOR = 1e6;
+        std::ranges::for_each(ctx.vars_soa_, fil::soa_select<soa_assignment_ctx>([](auto& assignment_ctx) { //
+            assignment_ctx.vsids_activity_ /= NORMALIZATION_FACTOR;
+        }));
+    }
+
+    // increase the VSIDS activity of the variables in the learned clause
+    for (const auto& varid : all_lit | std::views::values) {
+        auto& assignment_context = get<soa_assignment_ctx>(ctx.vars_soa_[varid]);
+        assignment_context.vsids_activity_ += ctx.config_.vsids_increment;
+    }
+
+    // decrease the VSIDS for all variables if the counter of conflict exceeded the configured decay interval
+    if (ctx.statistics_.conflicts % ctx.config_.decay_interval == 0) {
+        std::ranges::for_each(ctx.vars_soa_, fil::soa_select<soa_assignment_ctx>([&ctx](auto& assignment_ctx) { //
+            assignment_ctx.vsids_activity_ /= ctx.config_.vsids_decay_ratio;
+        }));
+    }
 }
 
 /**
@@ -77,7 +96,6 @@ void increase_vsids_activity(Solver_Context& ctx, const Clause& clause) {
  * @return a resolution result that provides the learned clause as well as the backtracking level at which the solver must return to for continuation of the sat solve
  */
 conflict_resolution_result resolve_conflict(Solver_Context& ctx, Clauses_Soa::soa_struct conflict_soastruct_clause) {
-
     const auto& [conflict_clause, watcher, meta] = conflict_soastruct_clause;
     log_debug("analyzing conflicting clause: {}", to_string(conflict_clause));
 
@@ -324,9 +342,7 @@ std::expected<solver::result, sat_error> solve_sat(Solver_Context& ctx, const mo
             }
             learn_additional_clause(ctx, learned_clause);
             backtrack(ctx, backtrack_level);
-
-            // increase activity of learned clause
-            increase_vsids_activity(ctx, learned_clause);
+            update_vsids_activity(ctx, learned_clause);
 
         } else {
             if (make_decision(ctx))