pub trait Search {
// Required methods
fn propagate(&mut self, kernel: &mut Kernel) -> bool;
fn decide(&mut self, kernel: &mut Kernel);
fn analyze(&mut self, kernel: &mut Kernel);
fn backtrack(&mut self, kernel: &mut Kernel);
fn search(
&mut self,
kernel: &mut Kernel,
in_processor: &mut Vec<Box<dyn Pass>>,
) -> SATResult;
}Expand description
CDCL 搜索核心接口。
典型循环为：
propagate -> (conflict ? analyze + backtrack : decide)。
直观伪代码：
while result == UNKNOWN {
if !propagate() { analyze(); backtrack(); }
else if all_assigned() { return SAT; }
else { decide(); }
}
flowchart TD
Start([开始]) --> P[propagate: BCP]
P -->|发现冲突| A[analyze: 冲突分析/学习]
A --> B[backtrack: 非时序回跳]
B --> P
P -->|无冲突且全部已赋值| Sat([返回 SAT])
P -->|无冲突但仍有未赋值变量| D[decide: 决策赋值]
D --> P