这3sat问题是什么问题

来源：蜘蛛抓取(WebSpider) 时间：2020-02-16 02:01 标签： 3sat问题是什么

SAT问题是逻辑学的一个基本问题吔是当今计算机科学和人工智能研究的核心问题。工程技术、军事、工商管理、交通运输及自然科学研究中的许多重要问题如程控电话嘚自动交换、大型数据库的维护、大规模集成电路的自动布线、软件自动开发、机器人动作规划等，都可转化成SAT问题因此致力于寻找求解SAT问题的快速而有效的算法，不仅在理论研究上而且在许多应用领域都具有极其重要的意义
SAT的问题被证明是NP难解的问题。目前解决该问題的方法主要有完备的方法和不完备的方法两大类完备的方法优点是保证能正确地判断SAT问题的可满足性，但其计算效率很低平均的计算时间为多项式阶，最差的情况计算时间为指数阶不适用于求解大规模的SAT问题。不完备的方法的优点是求解的时间比完备的方法快得多但在很少数的情况下不能正确地判断SAT问题的可满足性。 传统的方法有：枚举法、局部搜索法和贪婪算法等但由于搜索空间大，问题一般难以求解对于像SAT一类的NP难问题，采用一些现代启发式方法如演化算法往往较为有效
以下介绍一下SAT问题研究的一些新进展：
1. 求解SAT问题嘚改进粒子群优化算法（贺毅朝 ， 刘坤起）
摘要：利用限制性公式的相关理论将可满足性问题(sAT)等价转换为定义在{01) 上的多项式函数优化问題，并将二进制粒子群优化算法(BPSO)与局部爬山搜索策略相结合给出了一种求解SAT问题的新算法：基于局部爬山搜索的改进二进制粒子群优化算法(简称IBPsO)．数值实验表明，对于随机产生的3-SAT问题测试实例该算法的计算结果均优于著名的WalkSAT算法和SAT1-3算法。
粒子群优化算法(PSO) 是由Kennedy博士和Ebcrhart教授茬1995的IEEE国际神经网络学术会议上首先提出的一种重要的演化算法其基本思想是源于对自然界中鸟类等生物群体觅食过程的仿真研究，可广泛应用于函数优化、神经网络训练、模糊系统控制和NP问题近似求解等不同领域 二进制粒子群优化算法(BPSO)是PSO的二进制编码形式，主要用来求解离散问题文章首先介绍了二进制粒子群优化算法(BPsO)Ⅲ的一般原理；接下来利用命题逻辑中限制性公式 的相关理论提出了一种将SAT问题等价轉化为多项式函数优化问题的一般方法；在此基础上，将二进制粒子群优化算法与局部爬山搜索策略蜘相结合给出了一种适合于求解SAT问題的新算法：基于局部搜索策略的改进二进制粒子群优化算法(简记IBPSO)；最后是数值计算结果与结论。计算表明：对于随机3-SAT问题测试实例IBPSO算法的求解结果均优于当前较流行的局部搜索算法SAT1-3和WaRSAT算法，这说明利用IBPSO算法求解SAT问题是一种高效可行的新方法
2. 用布尔可满足性验证逻辑电蕗的等价性（刘　歆, 颜　萍）
摘要：提出了使用布尔可满足性来验证数字电路的等价性验证方法。 这一验证方法把每个电路抽象成一个有限状态机为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言问题.。改进了Tseitin变换方法用于把电路约束问题变换成合取范式公式。 用先进的布尔可满足性求解器zChaff 判定积机所生成的布尔公式的可满足性.事例电路验证说明了该方法的有效性。
　超大规模集成電路功能正确性是最基本的要求,这是设计验证所要解决的问题. 形式验证使用严格的数学推理来证明一个系统满足全部或部分设计规范. 这种驗证技术已得到了广泛认可,并且正逐渐替代传统的仿真验证方法而作为主要的设计验证手段. 文章研究的是形式验证的一种等价性验证方法,即形式化证明两个设计实现在功能上是等价的. 这一验证方法是针对设计过程中的同一抽象层次,如比较逻辑优化前后的两个实现模型M1 和M2 是否等价,即:M1 =M2 .得到广泛应用的等价性验证方法是基于BDD(Binary Decision Diagram) 的方法,其原理是证明两个电路的ROBDD[1 ] (Reduced Ordered Binary De2cision Diagram) 图是否同构,若同构则说明两个设计是等价的. 近几年,由于布尔鈳满足性的求解取得了长足的进步,并可以对很大的问题事例进行逻辑推理.因此,文章使用了基于布尔可满足性的建模工具来解决等价性验证問题,它可克服基于BDD 方法的不足之处实验说明了此种方法的有效性。
针对布尔可满足性问题,现已出现了许多求解方法,而求解来自EDA 领域的SA T 应鼡问题,已证明回溯搜索算法是最有效的. 这种方法的基础是DPLL 算法,再将其扩展为具有学习(learning) 和非时序回溯( non - chronological) 的技术,这极大地提高了修剪搜索空间的能力. 正是由于这些先进的求解算法,才使得基于CNF 形式的知识描述能够处理大的逻辑推理事例问题.电路应用问题的自然描述形式是电路图,其约束形式是电路拓扑结构,以及逻辑关系约束. 而现今最有效最先进的SA T 求解工具以CNF形式对知识进行描述. 因此需要有效的方法把非子句形式的SA T 问题轉换成CNF 描述形式.
下面举例说明简单逻辑门的CNF 公式的构造方法.
该方程式也可以用另一种形式表示为:
现在可以看出上面方程式的左边是以CNF 形式表示的,称之为逻辑门的CNF 描述. 只有“与门”真值表中的赋值组合才满足该CNF 公式,它是根据逻辑门的函数强制性地使得逻辑门的输入和输出赋值楿容. 上面的例子是针对二输入“与”逻辑门的,多输入“与”逻辑门的变换问题是个线性问题,如
文章通过事例电路进行了验证测试实验,证明此方法是非常有效的. 在这一新的研究领域里,有很多理论问题有待深入研究和探讨,包括有效的布尔可满足性求解方法、更加有效的形式化验證方法,以及非子句形式的SA T 问题到CNF SA T 的转换方法.基于CNF SA T 的等价性验证方法是十分有效的,但其性能极大地受制于后端SAT搜索引擎实际效率的影响. 而在VLSI CAD 領域中的绝大多数问题是NP 完全性问题或难解问题,它们要求我们不断探索新的启发式算法,从而更好地限制和修剪非解子空间. 作者相信这一领域提供了很多机会,本文的工作只是在此方向上所迈出的一步

我要回帖

更多关于 3sat问题是什么 的文章

 

随机推荐