diff --git a/docs/cnf/4-queen-problem.cnf b/docs/cnf/4-queen-problem.cnf new file mode 100644 index 0000000..a99c3ef --- /dev/null +++ b/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 \ No newline at end of file diff --git a/docs/cnf/README.md b/docs/cnf/README.md new file mode 100644 index 0000000..631207c --- /dev/null +++ b/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) diff --git a/docs/cnf/propagation-chain.cnf b/docs/cnf/propagation-chain.cnf new file mode 100644 index 0000000..3be1075 --- /dev/null +++ b/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 diff --git a/docs/cnf/simple_conflict.cnf b/docs/cnf/simple_conflict.cnf new file mode 100644 index 0000000..223e9cd --- /dev/null +++ b/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 + diff --git a/docs/cnf/simple_straight.cnf b/docs/cnf/simple_straight.cnf new file mode 100644 index 0000000..345c4f1 --- /dev/null +++ b/docs/cnf/simple_straight.cnf @@ -0,0 +1,3 @@ +p cnf 3 2 +1 -3 0 +2 3 -1 0 \ No newline at end of file diff --git a/docs/cnf/test.cnf b/docs/cnf/test.cnf new file mode 100644 index 0000000..5cc7e13 --- /dev/null +++ b/docs/cnf/test.cnf @@ -0,0 +1,7 @@ +p cnf 4 4 + + -1 4 0 + -1 2 0 + -1 3 0 + -4 -2 0 + diff --git a/fabko/compiler/backend/sat/solver_context.cpp b/fabko/compiler/backend/sat/solver_context.cpp index 3554d90..bc0f9f9 100644 --- a/fabko/compiler/backend/sat/solver_context.cpp +++ b/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(ctx.vars_soa_[lit.second]).vsids_activity_; + return vsids_activity >= (std::numeric_limits::max() - ctx.config_.vsids_increment); }); + if (need_normalization) { + static constexpr auto NORMALIZATION_FACTOR = 1e6; + std::ranges::for_each(ctx.vars_soa_, fil::soa_select([](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(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([&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 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))