From 5aa06b6333f9da2fdb82118dec55510f3bb72649 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:28:48 -0700 Subject: [PATCH] refactor phase update --- src/sat/sat_solver.cpp | 72 +++++++++++++++--------------------------- src/sat/sat_solver.h | 1 + 2 files changed, 26 insertions(+), 47 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index cd4793416..a90840d3b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -657,11 +657,16 @@ namespace sat { if (l.var() >= num_vars()) return; bool value = !l.sign(); - if (m_phase[l.var()] != value) - m_phase_birthdate[l.var()] = m_stats.m_conflicts; + set_phase(l.var(), value); if (m_best_phase[l.var()] != value) m_best_phase_birthdate[l.var()] = m_stats.m_conflicts; - m_best_phase[l.var()] = m_phase[l.var()] = value; + m_best_phase[l.var()] = value; + } + + void solver::set_phase(bool_var v, bool value) { + if (m_phase[v] != value) + m_phase_birthdate[v] = m_stats.m_conflicts; + m_phase[v] = value; } struct solver::cmp_activity { @@ -915,9 +920,7 @@ namespace sat { m_assignment[(~l).index()] = l_false; bool_var v = l.var(); m_justification[v] = j; - if (m_phase[v] != !l.sign()) - m_phase_birthdate[v] = m_stats.m_conflicts; - m_phase[v] = !l.sign(); + set_phase(v, !l.sign()); m_assigned_since_gc[v] = true; m_trail.push_back(l); @@ -2197,11 +2200,9 @@ namespace sat { if (!was_eliminated(v)) { m_model[v] = value(v); bool is_true = value(v) == l_true; - if (m_phase[v] != is_true) - m_phase_birthdate[v] = m_stats.m_conflicts; + set_phase(v, is_true); if (m_best_phase[v] != is_true) m_best_phase_birthdate[v] = m_stats.m_conflicts; - m_phase[v] = is_true; m_best_phase[v] = is_true; } } @@ -2972,9 +2973,7 @@ namespace sat { bool_var v = m_trail[i].var(); TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";); bool value = m_rand() % 2 == 0; - if (m_phase[v] != value) - m_phase_birthdate[v] = m_stats.m_conflicts; - m_phase[v] = value; + set_phase(v, value); } if (is_sat_phase() && head >= m_best_phase_size) { m_best_phase_size = head; @@ -3032,18 +3031,12 @@ namespace sat { void solver::do_rephase() { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (!m_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = true; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, true); break; case PS_ALWAYS_FALSE: - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = false; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, false); break; case PS_FROZEN: break; @@ -3052,23 +3045,16 @@ namespace sat { case 0: for (unsigned i = 0; i < m_phase.size(); ++i) { bool value = (m_rand() % 2) == 0; - if (m_phase[i] != value) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = value; + set_phase(i, value); } break; case 1: - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = false; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, false); break; case 2: - for (unsigned i = 0; i < m_phase.size(); ++i) { - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = !m_phase[i]; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, !m_phase[i]); break; default: break; @@ -3076,29 +3062,21 @@ namespace sat { break; case PS_SAT_CACHING: if (m_search_state == s_sat) - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i] != m_best_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = m_best_phase[i]; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, m_best_phase[i]); break; case PS_RANDOM: for (unsigned i = 0; i < m_phase.size(); ++i) { bool value = (m_rand() % 2) == 0; - if (m_phase[i] != value) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = value; + set_phase(i, value); } break; case PS_LOCAL_SEARCH: if (m_search_state == s_sat) { if (m_rand() % 2 == 0) bounded_local_search(); - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i] != m_best_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = m_best_phase[i]; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, m_best_phase[i]); } break; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index d50ee9461..5581668ef 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -376,6 +376,7 @@ namespace sat { void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } void set_phase(literal l) override; + void set_phase(bool_var v, bool value); bool get_phase(bool_var b) { return m_phase.get(b, false); } bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); } uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }