文章目录
前言布尔可满足性(Boolean satisfiability problem, SAT )SAT举例SAT基本求解算法：穷举基于赋值推导和冲突检测的SAT求解：DPLL(Davis-Putnam-Logemann-Loveland)冲突导向的子句学习：CDCL(Conflict-Driven Clause Learning)前言
视频：北大-软件分析-公开课
文档：课件
简单记录下。
布尔可满足性(Boolean satisfiability problem, SAT )
SAT问题是命题逻辑公式(propositional logical formula)的可满足性判定问题。基于命题逻辑，SAT问题可以进一步被描述为：给定一个命题逻辑公式f，公式f由子句集S组成，其中S由一组布尔变量V组成，判定是否存在一组对于f的赋值使得f中所有子句取值为真，如果存在，则称公式f可满足；否则，f不可满足。判定f是否可满足是SAT问题的核心。
任何命题逻辑公式可以表达为合取范式。即：SAT问题可以求解任何命题逻辑公式。
SAT举例
下面SAT问题是否可满足？—— 不满足。
# 数字表示字句的编号；符号表取非；{1, -4}∧{-2, 3}∧{2, 4}∧{-2, -3, 4}∧{-1, -4}
SAT基本求解算法：穷举
Sat(assign) {if (assign是完整的)if(每个子句中都有至少一个文字为真)return true;else return false;else选择一个未赋值的变量x；return sat(assign ∪ {x=0}) || sat(assign ∪ {x=1})}
基于赋值推导和冲突检测的SAT求解：DPLL(Davis-Putnam-Logemann-Loveland)
dpll(assign) {assign’=赋值推导(assign); // 赋值推导if (assign’有冲突) return false; // 冲突检测if (assign’是完整的) return true;选择一个未赋值的变量x；return dpll(assign’ ∪ {x=0}) || dpll(assign’ ∪ {x=1});}
算法解释如下：
冲突导向的子句学习：CDCL(Conflict-Driven Clause Learning)
cdcl() {assign=空赋值;while (true) {赋值推导(assign);if (推导结果有冲突) {if (assign为空) return false;添加新约束;撤销赋值;} else {if (推导结果是完整的) return true;选择一个未尝试的赋值x=1或者x=0;添加该赋值到assign;}}}
如果觉得《布尔可满足性》对你有帮助，请点赞、收藏，并留下你的观点哦！
