简单数理逻辑及其应用.pptx
简单数理逻辑及其应用清华大学 计算机科学与技术系李恺威概述数理逻辑命题联结词合式公式等值公式、定理范式SAT问题2-SATDPLL算法SMT问题分类应用命题命题变项简单命题和复合命题P:雪是白的且“1+1=2”可分割为R:雪是白的S:1+1=2命题联结词非与 合取或 析取 p p0110 p q pqpq0000010110011111推断推断因果关因果关系系等价等价 PQPQP QFFTTFTTFTFFFTTTT合式公式Well-formed formula命题变项和连接词的组合定义1.简单命题是合式公式2.如果A是合式公式，那么A也是合式公式3.如果A,B是合式公式，那么(A B),(A B),(A B)和(A B)是合式公式4.当且仅当经过有限次地使用1,2,3所组成的符号串才是合式公式合式公式合式公式简称公式例子p（pq）qIf 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的充分必要条件是AB是永真式不要将“=”视作连结词A=B表示公式A与B的一种关系1.自反性：A=A2.对称性：若A=B，则B=A3.传递性：若A=B，B=C，则A=C等值公式1.1.双重双重否定否定律律 P=P2.2.结合律结合律 (P Q)R=P (Q R)(P Q)R=P (Q R)(P Q)R=P (Q R)3.3.交换律交换律 P Q=Q P P Q=Q P P Q=Q P4.分配律分配律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=T6.吸收律吸收律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=(PQ)(PQ)(PQ)B=(PQ)(PQ)PQABFFTTFTTTTFFFTTTF从F列写A=(PQ)B=(PQ)(PQ)PQABFFTTFTTTTFFFTTTF范式列写方法多样，是否有标准形式？定义：文字：简单命题P及其否定式P合取式：一些文字的合取析取式：一些文字的析取析取范式：形如A1A2An(其中Ai为合取式)合取范式：形如A1A2An(其中Ai为析取式)范式范式定理：任意命题公式都存在有与其等值的合取范式和析取范式求范式AB=ABA B=(AB)(AB)=(AB)(AB)小结命题联结词合式公式等值公式、定理范式SAT问题Boolean satisfiability problem给出一个合式公式，判断其是否可满足将合式公式化成合取范式A1A2AnAi=(Pi1Pi2Pim)求解办法？2-SAT特殊情况合取式的每一项Ai最多只有2个变量析取(m=2)(X0X2)(X0X3)(X1X3)T T T T T T构图法N个变项，2N个节点（Ai与 Ai为对偶点）AB=A B对每一项(AB)从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问题)IntegersReal numbersArraysBit 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 位宽)y1:0+2z1:0+1=02y1:0+3z1:0 =0解线性比特向量算法(2 位宽)y1:0+2z1:0+1=02y1:0+3z1:0 =0求解y1:0(2 位宽)y1:0=2z+3带入y1:0(2 位宽)3z1:0+2=0解线性比特向量算法(2 位宽)3z1:0+2=0求解 z1:0(2 位宽)z1:0=2结果(3 位宽):z1:0=2y1:0=2z1:0+3=3y=y 2z=z 3x=4y+2z研究两大方向数学计算整数域、实数域线性、非线性计算机运算比特向量数组应用场景(1)方程求解应用场景(2)程序bug扫描int two-hop(int x)int a4=3,0,2,1;if(x 3)return-1;return aax-1;/out of range while x=1!Reference数理逻辑与集合论清华大学出版社 石纯一 20002-SAT解法浅析 赵爽http:/http:/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谢谢大家！
