easy_sat_rs/
api.rs

1/// 此模块用于定义 pre/in-processing 技术，作为可插拔的组件
2use crate::{constants::SATResult, kernel::Kernel};
3
4/// 求解流程中的可插拔 Pass 接口。
5///
6/// Pass 可用于两类阶段：
7/// - 预处理（preprocess）：在正式搜索前简化公式或提前判定结果；
8/// - 搜索中处理（inprocess）：在 CDCL 循环中周期性介入，做轻量重启/清理/重排等。
9pub trait Pass {
10    /// Pass 的短名称，用于日志和排序配置。
11    fn name(&self) -> &'static str;
12    /// Pass 的功能描述。
13    fn description(&self) -> &'static str;
14    /// Pass 所属类别，例如 `preprocess` / `inprocess`。
15    fn category(&self) -> &'static str;
16    /// 当前内核状态下该 Pass 是否应执行。
17    fn applying(&self, kernel: &Kernel) -> bool;
18    /// 执行 Pass 并返回是否已能判定 SAT/UNSAT。
19    fn apply(&mut self, kernel: &mut Kernel) -> SATResult;
20}
21
22/// CDCL 搜索核心接口。
23///
24/// 典型循环为：
25/// `propagate -> (conflict ? analyze + backtrack : decide)`。
26///
27/// 直观伪代码：
28/// `while result == UNKNOWN {`
29/// `  if !propagate() { analyze(); backtrack(); }`
30/// `  else if all_assigned() { return SAT; }`
31/// `  else { decide(); }`
32/// `}`
33///
34/// ```mermaid
35/// flowchart TD
36///     Start([开始]) --> P[propagate: BCP]
37///     P -->|发现冲突| A[analyze: 冲突分析/学习]
38///     A --> B[backtrack: 非时序回跳]
39///     B --> P
40///     P -->|无冲突且全部已赋值| Sat([返回 SAT])
41///     P -->|无冲突但仍有未赋值变量| D[decide: 决策赋值]
42///     D --> P
43/// ```
44#[cfg_attr(doc, aquamarine::aquamarine)]
45pub trait Search {
46    /// 执行 BCP（通常基于双观察文字）。
47    ///
48    /// 返回 `false` 表示传播中遇到冲突。
49    fn propagate(&mut self, kernel: &mut Kernel) -> bool;
50    /// 在无冲突且仍有未赋值变量时执行一次决策赋值。
51    fn decide(&mut self, kernel: &mut Kernel);
52    /// 对当前冲突做分析，构造学习子句并计算回跳层级。
53    fn analyze(&mut self, kernel: &mut Kernel);
54    /// 按 `analyze` 结果回跳，并断言学习子句中的 UIP 文字。
55    fn backtrack(&mut self, kernel: &mut Kernel);
56    /// 驱动完整搜索流程，直至返回 `SAT`/`UNSAT`/`UNKNOWN`。
57    fn search(&mut self, kernel: &mut Kernel, in_processor: &mut Vec<Box<dyn Pass>>) -> SATResult;
58}
easy_sat_rs/api.rs

easy_sat_rs/
api.rs
