DPLL / 归结 求解器 · SAT 可视化

输入一个 CNF（合取范式），DPLL 算法逐步演示 单元传播 → 决策 → 冲突 → 回溯， 最终判定 可满足 (SAT) 并给出一个模型，或 不可满足 (UNSAT)。