简单数理逻辑及其应用.ppt

简单数理逻辑及其应用清华大学 计算机科学与技术系李恺威概述•数理逻辑–命题–联结词–合式公式–等值公式、定理–范式•SAT问题–2-SAT–DPLL算法•SMT问题–分类–应用命题• 命题变项• 简单命题和复合命题•P:雪是白的且“1+1=2”•可分割为–R:雪是白的–S:1+1=2命题联结词•非¬•与∧   合取•或∨   析取 p  p0110 p q p∧∧qp∨q0000010110011111•推断推断–因果关系因果关系•等价等价 PQPQP QFFTTFTTFTFFFTTTT合式公式Well-formed formula•命题变项和连接词的组合•定义1.简单命题是合式公式2.如果A是合式公式，那么¬A也是合式公式3.如果A, B是合式公式，那么(A ∧ B), (A ∨ B), (A  B)和(A  B)是合式公式4.当且仅当经过有限次地使用1,2,3所组成的符号串才是合式公式合式公式•合式公式简称公式•例子p∧（pq）q•If A then B else C 能用合式公式表示吗？合式公式分类•永真式：在任何解释I下都为真(T)•可满足式：在某个解释I0下为真(T)•矛盾式：在任何解释I下都为假(F)•例1.P ∨ ¬P     I0=(T) I1=(F)2.P ∧ ¬QI0=(T, F)3.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=B表示公式A与B的一种关系1.自反性：A=A2.对称性：若A=B，则B=A3.传递性：若A=B，B=C，则A=C等值公式1.双重双重否定否定律律 ¬¬ P = P2.结合律合律 (P ∨∨ Q) ∨∨ R = P ∨∨ (Q ∨∨ R) (P ∧∧ Q) ∧∧ R = P ∧∧ (Q ∧∧ R) (P  Q)  R = P  (Q  R)3.交交换律律 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 = PP → P = T P  P = T6.吸收律吸收律P ∨∨ (P ∧∧ Q) = P P ∧∧ (P ∨∨ Q) = P7.摩根摩根（（De Morgan）律：）律： ¬ (P ∨∨ Q) = ¬P ∧∧ ¬Q ¬ (P ∧∧ Q) = ¬P ∨∨ ¬Q 命题公式与真值表•给出公式，列写真值表很容易•反过来呢？•尝试写出A，B由P，Q表达的公式PQABFFTTFTTTTFFFTTTF从T列写•A=(¬P∧¬Q)∨(¬P∧Q)∨(P∧Q)•B=(¬P∧¬Q)∨(¬P∧Q)PQABFFTTFTTTTFFFTTTF从F列写•A=(¬P∨Q)•B=(¬P∨Q)∧(¬P∨¬Q)PQABFFTTFTTTTFFFTTTF范式•列写方法多样，是否有标准形式？•定义：–文字：简单命题P及其否定式¬P–合取式：一些文字的合取–析取式：一些文字的析取–析取范式：形如A1∨A2∨……∨An(其中Ai为合取式)–合取范式：形如A1∧A2∧……∧An(其中Ai为析取式)范式•范式定理：任意命题公式都存在有与其等值的合取范式和析取范式•求范式•AB = ¬A∨B•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连一条边•从¬B向A连一条边•如果取了¬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 Φ 为空集 thenreturn trueif Φ 只含一个析取式 thenreturn truefor Φ 中的每个析取式l do如果析取式l只含有一个变量，直接确定其值使析取结果为Truefor Φ 中每个未定变量x do 如果x出现的形式相同，确定其值使结果为True选择Φ中一个未定变量yreturn DPLL(Φ∧y) or DPLL(Φ∧not y) //搜索SAT问题扩展？•一系列约束条件取并•判断是否可满足•SAT：约束条件为布尔变量的析取•布尔整数、实数？•析取数学运算？SMT•可满足模块理论•Satisfiability Modulo Theories•在不同论域上的约束判定问题•论域举例–Boolean (SAT问题)–Integers–Real numbers–Arrays–Bit vectors解线性比特向量算法(3 位宽)3x + 4y + 2z = 02x + 2y + 2 = 04y + 2x + 2z = 0X在第一个方程中的解3-1 mod 8 = 3,x = 4y + 2z(3 位宽)2y + 4z + 2 = 04y + 6z = 0带入x解线性比特向量算法(3 位宽)2y + 4z + 2 = 04y + 6z = 0所有系数为偶数除以2忽略最高位高位比特(2 位宽)y[1:0] + 2z[1:0] + 1 = 02y[1:0] + 3z[1:0] = 0解线性比特向量算法(2 位宽)y[1:0] + 2z[1:0] + 1 = 02y[1:0] + 3z[1:0] = 0求解y[1:0](2 位宽)y[1:0]=2z + 3带入y[1:0](2 位宽)3z[1:0] + 2 = 0解线性比特向量算法(2 位宽)3z[1:0] + 2 = 0求解 z[1:0](2 位宽)z[1:0]=2结果(3 位宽):z[1:0] = 2y[1:0] = 2z[1:0] + 3 = 3y = y’ @ 2z = z’ @ 3x = 4y + 2z研究两大方向•数学计算–整数域、实数域–线性、非线性•计算机运算–比特向量–数组应用场景(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://•http://•Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, and Dawson : 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谢谢大家！。