清华大学 计算机科学与技术系 李恺威 chnlkw@gmail.com 简单数理逻辑及其应用 清华大学 计算机科学与技术系 李恺威 chnlkw@gmail.com

概述 数理逻辑 命题 联结词 合式公式 等值公式、定理 范式 SAT问题 2-SAT DPLL算法 SMT问题 分类 应用

命题 定义 一个非真即假的陈述句 例子 李恺威是学霸 郭家宝太牛啦！ 我在说的是假话

命题变项 命题符号化 P表示“李恺威是学霸” 命题变项P ：表示任意命题

简单命题和复合命题 P:雪是白的且“1+1=2” 可分割为 R:雪是白的 S:1+1=2

命题联结词 p  p 1 非¬ 与∧ 合取 或∨ 析取 p q p∧q p∨q 1

推断 因果关系 等价 P Q PQ P Q F T

合式公式 Well-formed formula 命题变项和连接词的组合 定义 简单命题是合式公式 如果A是合式公式，那么¬A也是合式公式 如果A, B是合式公式，那么(A ∧ B), (A ∨ B), (A  B)和(A  B)是合式公式 当且仅当经过有限次地使用1,2,3所组成的符号串才是合式公式

合式公式 合式公式简称公式 例子 p∧（pq）q If A then B else C 能用合式公式表示吗？

合式公式分类 永真式：在任何解释I下都为真(T) 可满足式：在某个解释I0下为真(T) 矛盾式：在任何解释I下都为假(F) 例 P ∨ ¬P I0=(T) I1=(F) P ∧ ¬Q I0=(T, F) P ∨ ¬P 矛盾

三种公式关系 A永真，当且仅当¬A永假 A可满足，当且仅当¬A非永真 A不可满足，当且仅当A永假

等值公式 两个公式A和B， P1,…,Pn是所有A和B中的命题变项 A和B有2n个不同的解释 在任何解释下，A和B的真值都相等

等值定理 对公式A和B，A=B的充分必要条件是AB是永真式 不要将“=”视作连结词 A=B表示公式A与B的一种关系 自反性：A=A 对称性：若A=B，则B=A 传递性：若A=B，B=C，则A=C

等值公式 双重否定律 ¬¬ P = P 结合律 (P ∨ Q) ∨ R = P ∨ (Q ∨ R) (P ∧ Q) ∧ R = P ∧ (Q ∧ R) (P  Q)  R = P  (Q  R) 交换律 P ∨ Q = Q ∨ P P ∧ Q = Q ∧ P P  Q = Q  P

4.分配律 P ∨ (Q ∧ R) = (P ∨ Q) ∧ (P ∨ R) P ∧ (Q ∨ R) = (P ∧ Q) ∨ (P ∧ R) P → (Q → R) = (P → Q) → (P → R) 5. 等幂律 P ∨ P = P P ∧ P = P P → P = T P  P = T

6. 吸收律 P ∨ (P ∧ Q) = P P ∧ (P ∨ Q) = P 7 6.吸收律 P ∨ (P ∧ Q) = P P ∧ (P ∨ Q) = P 7.摩根（De Morgan）律： ¬ (P ∨ Q) = ¬P ∧ ¬Q ¬ (P ∧ Q) = ¬P ∨ ¬Q

命题公式与真值表 给出公式，列写真值表很容易 反过来呢？ 尝试写出A，B由P，Q表达的公式 P Q A B F T

从T列写 A=(¬P∧¬Q)∨(¬P∧Q)∨(P∧Q) B=(¬P∧¬Q)∨(¬P∧Q) P Q A B F T

从F列写 A=(¬P∨Q) B=(¬P∨Q)∧(¬P∨¬Q) P Q A B F T

范式 列写方法多样，是否有标准形式？ 定义： 文字：简单命题P及其否定式¬P 合取式：一些文字的合取 析取式：一些文字的析取 析取范式：形如A1∨A2∨……∨An(其中Ai为合取式) 合取范式：形如A1∧A2∧……∧An(其中Ai为析取式)

范式 范式定理：任意命题公式都存在有与其等值的合取范式和析取范式 求范式 AB = ¬A∨B A  B = (¬A∨B)∧(A∨¬B)

小结 命题 联结词 合式公式 等值公式、定理 范式

SAT问题 Boolean satisfiability problem 给出一个合式公式，判断其是否可满足 将合式公式化成合取范式 A1∧A2∧……∧An Ai=(Pi1∨Pi2∨…Pim) 求解办法？

2-SAT 特殊情况 合取式的每一项Ai最多只有2个变量析取(m<=2) (X0∨X2)∧(¬ X0∨X3) ∧(X1∨¬X3) T T T T T T

构图法 N个变项，2N个节点 （Ai与¬ Ai为对偶点） A∨B = ¬A  B 对每一项(A∨B) 从¬A向B连一条边 若存在A到¬A存在路径，则无解

寻找可行解 有向图 强连通分量缩环 给个对偶分支取一条

3-SAT 析取式中某些项包含的变量为3个 上述算法不成立 第一个所知的NP完全问题 1971年由史提芬·A·古克(Stephen A. Cook)提出的古克定理证明 一般SAT问题，搜索！

DPLL算法 Davis-Putnam-Logemann-Loveland 它在1962年由Martin Davis, Hilary Putnam, George Logemann 和 Donald W. Loveland 提出,作为早期Davis-Putnam 算法的一种改进。Davis-Putnam 算法是Davis 与 Putnam在1960年发展的一种算法 50年来最有效的算法

Φ：一系列析取式的集合（表示它们合取） Function DPLL(Φ) if Φ 为空集 then return true if Φ 只含一个析取式 then for Φ 中的每个析取式l do 如果析取式l只含有一个变量，直接确定其值使析取结果为True for Φ 中每个未定变量x do 如果x出现的形式相同，确定其值使结果为True 选择Φ中一个未定变量y return DPLL(Φ∧y) or DPLL(Φ∧not y) //搜索

SAT问题扩展？ 一系列约束条件取并 判断是否可满足 SAT：约束条件为布尔变量的析取 布尔整数、实数？ 析取数学运算？

SMT 可满足模块理论 Satisfiability Modulo Theories 在不同论域上的约束判定问题 论域举例 Boolean (SAT问题) Integers Real numbers Arrays Bit vectors

解线性比特向量算法 (3 位宽) 3x + 4y + 2z = 0 X在第一个方程中的解 2x + 2y + 2 = 0 4y + 2x + 2z = 0 X在第一个方程中的解 3-1 mod 8 = 3, (3 位宽) 2y + 4z + 2 = 0 4y + 6z = 0 带入x x = 4y + 2z

解线性比特向量算法 (3 位宽) 所有系数为偶数 2y + 4z + 2 = 0 4y + 6z = 0 (2 位宽) 除以2 忽略最高位高位比特

解线性比特向量算法 带入y[1:0] (2 位宽) y[1:0] + 2z[1:0] + 1 = 0

解线性比特向量算法 (2 位宽) 3z[1:0] + 2 = 0 求解 z[1:0] 结果(3 位宽): z[1:0] = 2 y[1:0] = 2z[1:0] + 3 = 3 y = y’ @ 2 z = z’ @ 3 x = 4y + 2z (2 位宽) z[1:0]=2

研究两大方向 数学计算 整数域、实数域 线性、非线性 计算机运算 比特向量 数组

应用场景(1) 方程求解

应用场景(2) 程序bug扫描 int two-hop(int x) { int a[4] = {3, 0, 2, 1}; if(x < 0 or x > 3) return -1; return a[a[x]-1]; //out of range while x = 1 ! }

Reference 《数理逻辑与集合论》清华大学出版社 石纯一 2000 《2-SAT解法浅析》 赵爽 http://en.wikipedia.org/wiki/Boolean_satisfiability_problem http://en.wikipedia.org/wiki/DPLL_algorithm http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, and Dawson Engler.EXE: Automatically generating inputs of death. In Proceedings of the 13th ACM Conference on Computer and Communications Security, October-November 2006. DECISION PROCEDURES FOR BIT-VECTORS, ARRAYS AND INTEGERS. Vijay Ganesh.September 2007

谢谢大家！