easy_sat_rs/
common.rs

1/// CNF 子句、2WL watcher、VSIDS 与相位策略等公共数据结构。
2use std::ops::{Index, IndexMut};
3
4use keyed_priority_queue::KeyedPriorityQueue;
5use ordered_float::OrderedFloat;
6
7use crate::constants::{
8    DEFAULT_VAR_DECAY, DEFAULT_VAR_DECAY_INC, DEFAULT_VAR_INC, INIT_PHASE, MAX_VAR_DECAY,
9};
10
11/// 求解器内部变量状态（不是 DIMACS 中变量定义本身）。
12///
13/// 该结构记录变量在搜索过程中的“赋值元信息”：
14/// - 在哪个决策层被赋值；
15/// - 在 `trail` 中的位置；
16/// - 若为传播赋值，其原因子句编号。
17#[derive(Debug, Clone, Copy, Default)]
18pub struct Variable {
19    /// 变量被赋值时所在的决策层。
20    pub level: usize,
21    /// 变量被压入 trail 时的位置（1-based 语义，由外部维护）。
22    pub trail_index: usize,
23    /// 赋值原因子句。
24    ///
25    /// - 决策赋值：`None`
26    /// - 蕴含赋值：`Some(clause_id)`
27    pub reason: Option<usize>,
28}
29
30/// 文字类型：正数表示正文字，负数表示反文字。
31pub type Literal = isize;
32
33#[derive(Debug, Clone, Default)]
34/// 子句（文字析取）结构。
35///
36/// - `literals`：子句中的文字序列；
37/// - `lbd`：学习子句质量指标（Literal Block Distance）；
38/// - `garbage`：删除标记（当前版本预留位）。
39pub struct Clause {
40    /// 学习子句的 LBD 指标。
41    lbd: u32,
42    /// 子句的文字列表。
43    literals: Vec<Literal>,
44    /// 垃圾回收标志位。
45    garbage: bool,
46}
47
48/// 双观察文字（2WL）中的 watcher 条目。
49///
50/// 其核心思想是：只跟踪每个子句中的少量关键文字，从而避免每次传播都整句扫描。
51/// - `clause_id` 指向被监视的子句；
52/// - `blocker` 通常存“另一个被监视文字”，若其已为真，则该子句已满足，可快速跳过。
53///
54/// ```mermaid
55/// flowchart LR
56///     C[子句 C 监视 l0 与 l1] --> W0[watch(-l0) 存 watcher]
57///     C --> W1[watch(-l1) 存 watcher]
58///     W0 --> P[当 l0 被赋假时触发检查]
59///     W1 --> Q[当 l1 被赋假时触发检查]
60/// ```
61///
62/// 例：若子句监视 `x3` 与 `-x8`，则 watcher 分别放在 `watch(-x3)` 与 `watch(x8)`。
63#[cfg_attr(doc, aquamarine::aquamarine)]
64#[derive(Debug, Clone, Default, Copy)]
65pub struct Watches {
66    pub clause_id: usize,
67    pub blocker: Literal,
68}
69
70/// VSIDS 的变量活跃度表。
71///
72/// 启发式目标：
73/// - 冲突相关变量会被 `bump`，分数上升；
74/// - `var_inc` 随冲突递增并经衰减控制，强调近期冲突；
75/// - 通过优先队列选取当前分数最高的未赋值变量。
76///
77/// 例：设初始 `var_inc = 1.0`、`var_decay = 0.8`。
78/// - 第 1 次冲突命中变量 `v`：`activity[v] += 1.0`
79/// - 调用 `decay_inc()` 后：`var_inc = 1.25`
80/// - 第 2 次冲突再次命中 `v`：`activity[v] += 1.25`
81///
82/// 因而近期冲突对分数贡献更大，变量选择会更偏向“最近导致冲突”的区域。
83pub struct ActivityTable {
84    pq: KeyedPriorityQueue<usize, OrderedFloat<f64>>,
85    activities: Vec<f64>,
86    var_inc: f64,
87    var_decay: f64,
88}
89
90/// 决策相位（phase）状态表。
91///
92/// 这是相位选择策略的简化实现：
93/// - `target_phase`：偏向稳定阶段的目标相位；
94/// - `saved_phases`：历史相位（phase saving），回溯后可复用。
95pub struct Phases {
96    /// 目标相位。
97    target_phase: Vec<bool>,
98    /// 保存相位（回溯后优先复用的历史相位）。
99    saved_phases: Vec<bool>,
100}
101
102impl Clause {
103    /// 创建空子句。
104    pub fn new() -> Self {
105        Self { lbd: 0, literals: Vec::new(), garbage: false }
106    }
107
108    /// 设置文字并按变量编号排序（便于规范化表示）。
109    pub fn with_literals(mut self, literals: Vec<Literal>) -> Self {
110        self.literals = literals;
111        self.literals.sort_by_key(|l1| l1.unsigned_abs());
112        self
113    }
114
115    /// 设置已按调用方规则排布的文字（不再重排）。
116    pub fn with_ordered_literals(mut self, literals: Vec<Literal>) -> Self {
117        self.literals = literals;
118        self
119    }
120
121    /// 设置子句的 LBD 值。
122    pub fn with_lbd(mut self, lbd: u32) -> Self {
123        self.lbd = lbd;
124        self
125    }
126
127    /// 返回子句 LBD。
128    pub fn lbd(&self) -> u32 {
129        self.lbd
130    }
131
132    /// 返回只读文字切片。
133    pub fn literals(&self) -> &[Literal] {
134        &self.literals
135    }
136
137    /// 返回该子句是否已标记为垃圾。
138    pub fn garbage(&self) -> bool {
139        self.garbage
140    }
141}
142
143impl IntoIterator for Clause {
144    type Item = Literal;
145    type IntoIter = std::vec::IntoIter<Literal>;
146
147    fn into_iter(self) -> Self::IntoIter {
148        self.literals.into_iter()
149    }
150}
151
152impl<'a> IntoIterator for &'a Clause {
153    type Item = &'a Literal;
154    type IntoIter = std::slice::Iter<'a, Literal>;
155
156    fn into_iter(self) -> Self::IntoIter {
157        self.literals.iter()
158    }
159}
160
161impl Index<usize> for Clause {
162    type Output = Literal;
163
164    fn index(&self, index: usize) -> &Self::Output {
165        &self.literals[index]
166    }
167}
168
169impl IndexMut<usize> for Clause {
170    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
171        &mut self.literals[index]
172    }
173}
174
175impl ActivityTable {
176    /// 初始化活跃度表并把所有变量放入优先队列。
177    pub fn new(max_vars: usize) -> Self {
178        let mut ret = Self {
179            pq: KeyedPriorityQueue::new(),
180            activities: vec![0.0; max_vars + 1],
181            var_inc: DEFAULT_VAR_INC,
182            var_decay: DEFAULT_VAR_DECAY,
183        };
184        for var in 1..=max_vars {
185            ret.pq.push(var, OrderedFloat(0.0));
186        }
187        ret
188    }
189
190    /// 提升变量活跃度（通常在冲突分析中调用）。
191    ///
192    /// 若变量已在堆中，更新其优先级；
193    /// 若暂不在堆中，按当前活跃度重新插入。
194    pub fn bump_var_score(&mut self, var_id: usize) {
195        match self.pq.entry(var_id) {
196            keyed_priority_queue::Entry::Occupied(e) => {
197                self.activities[var_id] += self.var_inc;
198                let p = OrderedFloat(self.activities[var_id]);
199                e.set_priority(p);
200            }
201            keyed_priority_queue::Entry::Vacant(e) => {
202                let p = OrderedFloat(self.activities[var_id]);
203                e.set_priority(p);
204            }
205        }
206    }
207
208    #[inline]
209    /// 增大“本轮 bump 的权重”，体现 EVSIDS 的近期偏好。
210    pub fn decay_inc(&mut self) {
211        self.var_inc /= self.var_decay
212    }
213
214    #[inline]
215    /// 调整衰减系数，逐步降低历史冲突的影响。
216    pub fn bump_decay_factor(&mut self) {
217        self.var_decay += DEFAULT_VAR_DECAY_INC;
218        if self.var_decay > MAX_VAR_DECAY {
219            self.var_decay = MAX_VAR_DECAY;
220        }
221    }
222
223    /// 选取下一个未赋值变量。
224    ///
225    /// `not_assigned` 由调用方提供，用于过滤当前已赋值变量。
226    pub fn next_variable<F>(&mut self, not_assigned: &F) -> Option<usize>
227    where
228        F: Fn(usize) -> bool,
229    {
230        while let Some((var_id, _)) = self.pq.pop() {
231            if not_assigned(var_id) {
232                return Some(var_id);
233            }
234        }
235        None
236    }
237}
238
239impl Phases {
240    /// 初始化相位表。
241    pub fn new(max_var: usize) -> Self {
242        Self {
243            target_phase: vec![INIT_PHASE; max_var + 1],
244            saved_phases: vec![INIT_PHASE; max_var + 1],
245        }
246    }
247
248    /// 按优先级选择变量相位并返回对应文字。
249    ///
250    /// 当前优先级：
251    /// 1. `target == true` 时使用 `target_phase`
252    /// 2. 其他情况使用 `saved_phases`
253    ///
254    /// ```mermaid
255    /// flowchart TD
256    ///     A[输入 var_id, target] --> B{target?}
257    ///     B -->|是| C[返回 target_phase[var_id]]
258    ///     B -->|否| D[返回 saved_phases[var_id]]
259    /// ```
260    ///
261    /// 例：若 `target=false` 且 `saved_phases[var_id]=true`，
262    /// 则本次决策文字为正文字 `+var_id`。
263    #[cfg_attr(doc, aquamarine::aquamarine)]
264    pub fn decide_phase(&self, var_id: usize, target: bool) -> Literal {
265        if target {
266            return var_id as isize * (if self.target_phase[var_id] { 1 } else { -1 });
267        }
268        var_id as isize * (if self.saved_phases[var_id] { 1 } else { -1 })
269    }
270
271    #[inline]
272    /// 保存变量最近一次赋值相位（phase saving）。
273    pub fn save_phase_for_variable(&mut self, var_id: usize, phase: bool) {
274        self.saved_phases[var_id] = phase;
275    }
276}
easy_sat_rs/common.rs

easy_sat_rs/
common.rs
