Trait Pass 

pub trait Pass {
    // Required methods
    fn name(&self) -> &'static str;
    fn description(&self) -> &'static str;
    fn category(&self) -> &'static str;
    fn applying(&self, kernel: &Kernel) -> bool;
    fn apply(&mut self, kernel: &mut Kernel) -> SATResult;
}

求解流程中的可插拔 Pass 接口。

Pass 可用于两类阶段：

• 预处理（preprocess）：在正式搜索前简化公式或提前判定结果；
• 搜索中处理（inprocess）：在 CDCL 循环中周期性介入，做轻量重启/清理/重排等。

Required Methods

fn name(&self) -> &'static str

Pass 的短名称，用于日志和排序配置。

fn description(&self) -> &'static str

Pass 的功能描述。

fn category(&self) -> &'static str

Pass 所属类别，例如 preprocess / inprocess。

fn applying(&self, kernel: &Kernel) -> bool

当前内核状态下该 Pass 是否应执行。

fn apply(&mut self, kernel: &mut Kernel) -> SATResult

执行 Pass 并返回是否已能判定 SAT/UNSAT。

Implementors