Struct Kernel 

pub struct Kernel {

    pub assignment: Vec<i8>,
    pub vars: Vec<Variable>,
    pub clauses: Vec<Clause>,
    pub watches: Vec<Vec<Watches>>,
    pub trail: Vec<Literal>,
    pub vsids: ActivityTable,
    pub phases: Phases,
    pub result: SATResult,
    pub level: usize,
    pub backtrack_level: usize,
    pub propagated: usize,
    pub assigned: usize,
    pub conflict: Option<(usize, Literal)>,
    pub lemma: Vec<Literal>,
    pub learnt: (Literal, Option<usize>),
    pub statistics: Statistics,
    mark_table: Vec<usize>,
    mark_epoch: usize,
    pending_clause: Vec<Literal>,
}

CDCL 求解核心内核状态。

Kernel 聚合了：

• CNF 子句库与 watcher 索引（2WL）；
• trail/决策层等搜索状态；
• VSIDS 与相位策略；
• 冲突分析与学习子句所需的临时缓存。

Fields

assignment: Vec<i8>

变量赋值表：-1=false，0=unassigned，1=true。

vars: Vec<Variable>

变量元信息表（层级、原因子句等）。

clauses: Vec<Clause>

子句数据库（原始子句 + 学习子句）。

watches: Vec<Vec<Watches>>

2WL watcher 桶。

trail: Vec<Literal>

trail（仅存当前被赋为真的文字）。

vsids: ActivityTable

VSIDS 活跃度表。

phases: Phases

相位策略状态表。

result: SATResult

当前求解结果。

level: usize

当前决策层。

backtrack_level: usize

冲突分析后要回跳到的层级。

propagated: usize

trail 中“已完成传播”的前缀长度。

assigned: usize

当前已赋值变量计数。

conflict: Option<(usize, Literal)>

当前冲突信息 (clause_id, conflict_lit)。

lemma: Vec<Literal>

冲突分析中的临时学习子句缓冲（lemma）。

learnt: (Literal, Option<usize>)

回跳后需要立即断言的 (literal, reason_clause)。

statistics: Statistics

统计信息。

mark_table: Vec<usize>

冲突分析与 LBD 计算用的时间戳标记表。

mark_epoch: usize

标记表当前 epoch。

pending_clause: Vec<Literal>

DIMACS 流式解析时暂存“尚未遇到 0 终止符”的子句。

Implementations

impl Kernel

pub fn new(max_vars: usize) -> Self

构建指定变量上限的求解内核。

pub fn add(&mut self, lit: Option<Literal>)

以流式方式添加子句文字。

• Some(lit)：把文字加入当前待完成子句；
• None：结束当前子句，落库并挂接 watcher。

pub fn value(&self, lit: Literal) -> i8

在当前赋值下评估文字取值。

返回值约定：

• 1：文字为真；
• -1：文字为假；
• 0：变量尚未赋值。

fn watcher_index(&self, lit: Literal) -> usize

把非零文字映射到 watcher 桶索引。

每个变量对应两个桶：

• 正文字 v -> 2*(v-1)
• 反文字 -v -> 2*(v-1)+1

例：v = 3 时，

• watch(3) 的索引是 4
• watch(-3) 的索引是 5

pub fn add_watch(&mut self, watched_lit: Literal, watch: Watches)

向 watched_lit 对应桶追加一个 watcher。

本实现遵循 2WL 常见约定：通常存入的是 -w（而非 w）， 即“让被监视文字 w 失效时会被触发”的桶，便于传播时 O(相关子句数) 访问。

fn attach_clause_watchers(&mut self, clause_id: usize)

为新子句初始化 watcher。

• 单子句 (l)：在 watch(-l) 挂一个 watcher；
• 非单子句 (l0 ∨ l1 ∨ ...)：
  • l0 的 watcher 放在 watch(-l0)，blocker=l1
  • l1 的 watcher 放在 watch(-l1)，blocker=l0

这样传播时只需读取被新真值文字触发的桶即可。

例：子句 (x1 ∨ -x4 ∨ x7) 初始挂接后：

• watch(-x1) 存一条 watcher，blocker = -x4
• watch(x4) 存一条 watcher，blocker = x1

pub fn watches(&mut self, lit: Literal) -> Vec<Watches>

取走并返回 lit 的整桶 watcher。

传播阶段采用 “take -> 处理 -> set” 方式，避免借用冲突并允许 watcher 迁移。

pub fn set_watches(&mut self, lit: Literal, ws: Vec<Watches>)

将传播后压实得到的 watcher 桶写回。

pub fn assign(&mut self, var_id: usize, lit: Literal, reason: Option<usize>)

写入一次变量赋值并记录到 trail。

• reason=None：决策赋值；
• reason=Some(clause_id)：传播蕴含赋值。

例：若在第 5 层写入 lit = -9 且 reason = Some(12)， 表示变量 x9 在第 5 层被子句 12 蕴含为假。

pub fn reset_value(&mut self, var_id: usize)

撤销变量赋值（用于回跳时弹栈）。

pub fn next_mark_epoch(&mut self) -> usize

申请一个新的标记 epoch。

若发生 usize 回绕，则清空标记表并从 1 重新开始。

pub fn mark_at(&self, idx: usize) -> usize

读取标记表在 idx 处的时间戳。

pub fn set_mark_at(&mut self, idx: usize, stamp: usize)

设置标记表 idx 的时间戳，不足则自动扩容。

pub fn add_learned_clause_with_lbd( &mut self, literals: Vec<Literal>, lbd: u32, ) -> usize

新增学习子句并初始化 watcher，返回子句编号。

pub fn satisfied(&self) -> bool

判断当前是否已给所有变量赋值。