sat问题发展情况.ppt

《sat问题发展情况.ppt》由会员分享，可在线阅读，更多相关《sat问题发展情况.ppt（20页珍藏版）》请在三一办公上搜索。

1、Sat,时间复杂度,时间复杂度并不是表示一个程序解决问题需要花多少时间，而是当问题规模扩大后，程序需要的时间长度增长得有多快。,时间复杂度,多项式级的复杂度。如 O(1),O(log(n),O(na)等 因为它的规模n出现在底数的位置！,非多项式级的复杂度 如：O(an)和O(n!)等！,P问题,如果一个问题可以找到一个能在多项式的时间里解决它的算法，那么这个问题就属于P问题。我们常见到的一些题目都是P问题。？,NP类问题,NP类问题：在多项式时间内可以验证一个算法问题的实例是否有解的算法问题的集合；它包含复杂性类P同时，它也包含NP完全问题，即在NP中“最难”的问题。,NP困难问题和NP完全

2、问题（npc）,要理解这几个概念，首先要明白几件事：1、对于NP问题是否存在确定的多项式时间的解，目前还不清楚（即有可能有一天可以证明NP问题=P问题，但目前还证明不出来、也不能证明NP问题P问题，目前的结论只是 NP问题集 P问题集2、对于两个问题X和Y，用T(X)和T(Y)表示它们的时间复杂度。如果T(Y)=f(T(X)，其中f是一个多项式函数，则写作Y=pX，即Y可以在多项式时间内归约到X。通俗地讲X至少和Y一样难。规约：如果能找到这样一个变化法则，对任意一个程序A的输入，都能按这个法则变换成程序B的输入，使两程序的输出相同，那么我们说，问题A可约化为问题B。,NP困难问题（NP-har

3、d problems）如果对于某个问题X，任意NP问题Y，都有Y=pX，则称X是NP难的问题NP完全问题（NP-complete problems）如果一个问题既是NP困难问题又是NP问题，我们称之为NP完全问题。,SAT问题及其研究进展,NPC问题多达几百个，但作为这些问题的“祖先”，于年证明了布尔逻辑的可满足性问题（SATISFIABLITY problem 简称为SAT）是世界上第一个完全（）问题，也就是说，任何非确定多项式问题（NP）都可在多项式时间内规约到进行求解，因此一个能高效地解决问题的算法一定能解决所有的问题。,布尔表达式是由布尔变量和运算符（NOT,AND,OR）所构成的表达

4、式。如果对于变量的某个true,false赋值，使得一个布尔表达式的值为true，则该布尔表达式是可满足的。例如布尔公式 A=(NOT x)AND y)OR(x AND(NOT z)，当 x=false,y=true z=false时，该布尔表达式值为true，则表达式A就是可满足的。问题描述：给定一个合取范式CNF，问是否存在变量的某种取值使得CNF的值为真。例如：（AB）（BD）（ACD）可满足性问题(SAT)就是判定一个给定的合取范式的布尔公式是否是可满足的。,问题应用和编码方面。加强实例和工业应用研究，将生产实际中更多难题转化为问题进行求解，研究问题规约和表示，并研究特定领域的问题求解

5、算法。为不同问题类型设计不同的算法是求解问题的有效途径。预处理方面。进一步研究应用预处理技术降低的问题规模和求解空间，并将有效的预处理技术融入其他求解算法。求解算法。当前难解问题方面。针对目前多数求解器无能为力的难满足实例、大规模问题实例等，加强问题内部逻辑结构的研究，将一些应用的特定知识作为启发式信息，提高解决实际问题的效率。求解器实现方面。研究求解算法的设计与实现，降低求解时间和空间代价。理论研究方面。研究各类典型求解算法的证明系统、证明复杂性及算法分析等。,研究方向,sat求解算法,SAT问题是逻辑学的一个基本问题，也是当今计算机科学和人工智能研究的核心问题。工程技术、军事、工商管理、交

6、通运输及自然科学研究中的许多重要问题，如程控电话的自动交换、大型数据库的维护、大规模集成电路的自动布线、软件自动开发、机器人动作规划等，都可转化成SAT问题。因此致力于寻找求解SAT问题的快速而有效的算法，不仅在理论研究上而且在许多应用领域都具有极其重要的意义。,SAT求解算法分类：完备算法不完备算法组合算法（混合不同求解策略或并行多个求解器）,问题按照可满足性可划分为：可满足的类不可满足的类按照问题产生的来源可划分为：应用类（application）随机生成类（random）难以满足的组合类（hard combination）,给定一个 问题公式（），在有限的时间内判定其是否可满足的算法称为

7、求解算法。,完备求解算法,完备算法比不完备算法的出现时间早。由于采取穷举和回溯的思想，完备算法从理论上能保证判定给定命题公式的的可满足性，在实例无解的情况下可以给出完备证明，因此也被称为系统搜索方法。该方法针对应用类实例很有效，优势明显。算法算法算法,DPLL算法,DPLL的重要思想在于穷举、分支回溯和布尔约束传播（），对所有变量进行深度搜索以形成一棵完全二叉树的遍历过程，如果问题是可满足的，则给出所有解；如果问题是不可满足的，则给出完备性证明。若公式中所有变量都被赋值，且没有发现一个冲突子句，那么该布尔公式是可满足的，否则是不可满足的。（）的变量集合，,基 于 的 求 解 器 主 要 发 展

8、 为 两 种 形 式，即 冲 突 驱 动 子 句 学 习（）和 前 向 搜 索（），前者较适合大规模验证问题，后者则更适合不可满足的难解随机问题实例。,Cdcl算法,算法是目前完备算法中最重要的一类，主要框架基于，但在预处理、分支策略、冲突分析、子句学习、非时序回溯、重启、数据结构等方面做了一系列改进。与的个重要区别：搜索过程不再递归，回溯使用一个显示的赋值栈称为trail在搜索过程中每次发现一个冲突子句时，都通过一个学习机制推导并增加新的子句，似乎增加的子句是多余的，但在剩余的整个搜索中它们能帮助确定文字取值。回溯不再限制返回之前的决策点，子句学习的结果是双重的，在生成一个学习子句的同时分析

9、哪些决策导致冲突，如果最近的个决策与冲突不相干，程序不仅会撤销最近的决策，也会撤销这 次决策以及相应的。当 前 求解器的代表作有、等,算法,算法和算法绝大多数时间都用来尝试各种可能的情况，可以看作蛮力求解算法。算法的框架基于，但侧重于通过大量的附加推理以及选择有效决策变量构建一个小巧平衡的搜索树来求解问题，在某些问题上优于前两种算法。算法简化公式的方式可以通过观察进而强制给变量指定值，也可以通过附加分解得到进一步的公式约束。算法整体是在前向搜索过程和搜索过程之间不断转换的，其在每一步会选择一个决策变量，并递归调用简化公式，正如其名字所示，当一个自由变量被设置确定布尔值时，它会执行一个决策启发式

10、前向计算可能的消减，从而测量该变量的重要性，然后使用导向启发式测量选择该变量的真值赋值。,不完备求解算法,除了极个别的不完备算法被用来尝试解决不可满足问题外，绝大多数不完备算法都不能判断问题的不可满足性。它尽管是不完备的，但在处理可满足的大规模随机生成问题时往往比完备算法快，因此受到广泛的应用和研究。不完备算法主要基于局部搜索的思想，将不满足的子句数量看成优化目标，在解空间随机搜索，但并非是单纯随机地搜索，而是在目标函数的引导下逐步逼近最终解。算法算法算法,算法,大多数不完备算法是基于的，其搜索过程为：给定一个命题公式，首先随机地生成一个真值赋值，如果该赋值使得公式可满足，则搜索结束；否则选择

11、其中一个变量翻转其真值，该过程一直重复，直到找到使得公式满足的真值赋值或迭代次数达到预定上限（公式的可满足性不能确定）尽管求解器会因附加不同的启发式而使复杂性提高，但整体来说，求解器都基于局部搜索非常简单的规则，同时支持运行过程中相当严谨的分析。代表算法有：GSAT、WalkSAT,算法,算法是相对较新的一种启发式算法。起源于无序系统的统计物理领域，通过计算全局信息来引导搜索过程，尽管消息传送方法并不适合每一类问题，但它发展出了一种计算所有解的统计特性的有效方法。此类最著名且最成功的求解器有可信传播（）、纵览传播（）、模 拟 退 火算法等。基于 的求解器能在可接受的时间内解决数以百万计变量的大

12、规模随机问题。,EA算法,算法是近年来发展起来的一种模仿自然界生物进化过程中“物竞天择，适者生存”原理的优化方法，研究人员在算法求解问题方面也做了许多成功尝试，开辟了解决问题的途径。其基本思想是将问题转化为一个求响应目标函数最小值（或最大值）的优化问题，采取一系列启发式初始化种群并不断寻优，直到达到终止条件或找到问题的解。如遗传算法、拟物拟人算法、量 子 免 疫 克 隆 算 法、粒 子 群 算 法、模拟 算法、量子算法、人工蜂群算法、组织进化算法等，,组合求解算法,混合求解：一个混合求解器包含两个或更多求解器，基本目标是创建能继承各个组件优点而回避缺点的一个求解器。一个理想的混合求解器能快速、

13、完备、低成本地求解各类问题。不完备算法擅长使用较少内存处理随机类问题，可以把全局信息传送给完备算法，从而指导完备算法决策变量的选择；而完备算法占用较多内存，擅长处理应用类和加工类问题，在随机类问题上表现平平，但它逻辑性较强，可以给不完备算法提供逻辑指导，二者有一定的互补性。,并行求解：单纯的序列（非并行）求解算法不可避免地受到 速度限制，并行求解算法日益受到广泛关注。最初的并行求解基于网络通信下的多核、共享存储空间等技术实现，目前并行求解主要采取两种方法，一种是采取分治思想将搜索空间划分为多个子空间进而分别调用序列算法求解；另一种更为突出的方法是并行组合方法，它利用不同序列算法的互补性使之在同一公式上相互竞争和合作，如Plingeling、动态子句共享策略、并行局部搜索、并行求解等。,几种典型求解算法比较,Thank You!,