DPLL 求解 SAT 的回溯搜索

把 DPLL 想成走迷宫：能推理就推理（单元传播），推不动就猜一步（决策）， 撞墙（冲突）就退回岔口换条路（回溯）。 这次的迷宫：让 F = (¬p₁∨p₂) ∧ (¬p₂∨p₃) ∧ (p₁∨p₃) ∧ (¬p₃∨p₂) 为真。

搜索树 · 迷宫地图

Decide unit unit 翻转 p₂ 回溯 backtrack unit ∅ p₂ = F • p₁ = F p₃ = F ✗ 冲突 C3 p₂ = T • p₃ = T ✓ SAT

子句状态 · 全绿才算走出迷宫

当前赋值 M · 已走的路

🏁 记住：DPLL 就是走迷宫 —— 能推就推（单元传播），推不动就猜（决策），撞墙（冲突）就退回岔口换条路（回溯）。
文字为真 文字为假 满足 单元 = 只剩一条活路 冲突 = 撞墙 • 决策 = 岔口