形式化7：求解可满足性问题

性问题"/>

形式化7：求解可满足性问题

求解可满足性问题

解析

1. 在命题中找到一对相反的命题,例如 C = Q ( p ) ∧ R ( ¬ p ) C=Q(p)\land R(\neg p) C=Q(p)∧R(¬p)中的 p p p和 ¬ p \neg p ¬p就是一对相反的命题
2. 由于 p p p和 ¬ p \neg p ¬p一定有一个为假,因此可以推出 Q ( ⊥ ) Q(\bot) Q(⊥)或 R ( ⊥ ) R(\bot) R(⊥)
   Q ( p ) R ( ¬ p ) Q ( ⊥ ) ∨ R ( ⊥ ) \cfrac{Q(p)\quad R(\neg p)}{Q(\bot)\lor R(\bot)} Q(⊥)∨R(⊥)Q(p)R(¬p)​
3. 将推出的命题合取到原命题,由于本身就是根据原命题推出的,因此不会改变命题的可满足性
   C = Q ( p ) ∧ R ( ¬ p ) ∧ ( Q ( ⊥ ) ∨ R ( ⊥ ) ) C=Q(p)\land R(\neg p)\land (Q(\bot)\lor R(\bot)) C=Q(p)∧R(¬p)∧(Q(⊥)∨R(⊥))

例如,求 ( ¬ p ∨ q ) ∧ p ∧ ( ¬ q ) (\neg p\lor q)\land p\land (\neg q) (¬p∨q)∧p∧(¬q)的可满足性

1. 首先 ¬ p ∨ q \neg p\lor q ¬p∨q和 p p p存在一个互反的原子命题,对其解析可得:
   ¬ p ∨ q p q \cfrac{\neg p\lor q \quad p}{q} q¬p∨qp​
   (p为真,~p必为假,那么要使命题成立q必须为真)
2. 合取到原命题
   ( ¬ p ∨ q ) ∧ p ∧ ( ¬ q ) ∧ q (\neg p\lor q)\land p\land (\neg q) \land q (¬p∨q)∧p∧(¬q)∧q
3. 又发现了一对互反的原子命题 ¬ q \neg q ¬q和 q q q
   ¬ q q ⊥ \cfrac{\neg q \quad q}{\bot} ⊥¬qq​
4. 因此原命题UNSAT

传播

DPLL说明

DPLL是用来求解可满足性问题（SAT）的一种方法，在基于真值表上取得了以下关键性进展：

1. 分裂规则：对命题进行假设并分裂
2. 单元传播规则：根据假设简化命题

举例

例如求解(~p1\/~p2) /\ (p2\/p4)的可满足性：
首先假定p1为TF的两个分支，将之代入并简化

为了使合取为真，则p2只能为F

代入简化，只剩下一个p4

为了得到解，则p4只能为T。
由此仅通过1次尝试（而非指数次）就得到了一个可满足的模型：【p1=T p2=F p4=T】

代码逻辑

dpll(P){if(P==T)return sat; if(P==F) return unsat;unitProp(P);            // unit prop and simplify P x = select_atomic(P);   // choose an atomic prop if(dpll(P[x|->T]))      // splitting return sat;return dpll(P[x|->F]);
}

SAT问题的应用