已知的NP-complete问题多达几百个，但作为这些问题的“祖先”，历史上第一个被证明的NP-complete问题是来自于布尔逻辑的可满足性问题（SATISFIABLITY problem），简称为SAT。我们知道，布尔表达式是由布尔变量和运算符（NOT , AND , OR）所构成的表达式。如果对于变量的某个true,false赋值，使得一个布尔表达式的值为true，则该布尔表达式是可满足的。例如布尔公式 A = ((NOT x) AND y) OR ( x AND (NOT z))，当 x = false ,y = true z = false时，该布尔表达式值为true，则表达式A就是可满足的。可满足性问题就是判定一个给定的合取范式的布尔公式是否是可满足的
SAT问题是逻辑学的一个基本问题，也是当今计算机科学和人工智能研究的核心问题。工程技术、军事、工商管理、交通运输及自然科学研究中的许多重要问题，如程控电话的自动交换、大型数据库的维护、大规模集成电路的自动布线、软件自动开发、机器人动作规划等，都可转化成SAT问题。因此致力于寻找求解SAT问题的快速而有效的算法，不仅在理论研究上而且在许多应用领域都具有极其重要的意义。
SAT的问题被证明是NP难解的问题。目前解决该问题的方法主要有完备的方法和不完备的方法两大类。完备的方法优点是保证能正确地判断SAT问题的可满足性，但其计算效率很低，平均的计算时间为多项式阶，最差的情况计算时间为指数阶，不适用于求解大规模的SAT问题。不完备的方法的优点是求解的时间比完备的方法快得多，但在很少数的情况下不能正确地判断SAT问题的可满足性。 传统的方法有：枚举法、局部搜索法和贪婪算法等，但由于搜索空间大，问题一般难以求解。对于像SAT一类的NP难问题，采用一些现代启发式方法如演化算法往往较为有效。
以下介绍一下SAT问题研究的一些新进展：
1.
求解SAT问题的改进粒子群优化算法（贺毅朝 ， 刘坤起）
摘要：利用限制性公式的相关理论将可满足性问题(sAT)等价转换为定义在{0，1) 上的多项式函数优化问题，并将二进制粒子群优化算法(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 公式的构造方法.
例:设有一个二输入的AND 逻辑门,它的输入为a 和b ,输出为c ,那么该逻辑门的逻辑行为可以
用方程式描述为
c = a •b.
该方程式也可以用另一种形式表示为:
ab © c = 0.
或者… ac + … bc + ab€c = 0 ,
或者
( a ∨ c) ( b ∨ c) ( a ∨ b ∨ c) = 1.
现在可以看出上面方程式的左边是以CNF 形式表示的,称之为逻辑门的CNF 描述. 只有“与门”真值表中的赋值组合才满足该CNF 公式,它是根据逻辑门的函数强制性地使得逻辑门的输入和输出赋值相容. 上面的例子是针对二输入“与”逻辑门的,多输入“与”逻辑门的变换问题是个线性问题,如
y = AND( x1 , x2 , ⋯, xn ) ,
其变换后得到CNF 公式。
文章通过事例电路进行了验证测试实验,证明此方法是非常有效的. 在这一新的研究领域里,有很多理论问题有待深入研究和探讨,包括有效的布尔可满足性求解方法、更加有效的形式化验证方法,以及非子句形式的SA T 问题到CNF SA T 的转换方法.基于CNF SA T 的等价性验证方法是十分有效的,但其性能极大地受制于后端SAT搜索引擎实际效率的影响. 而在VLSI CAD 领域中的绝大多数问题是NP 完全性问题或难解问题,它们要求我们不断探索新的启发式算法,从而更好地限制和修剪非解子空间. 作者相信这一领域提供了很多机会,本文的工作只是在此方向上所迈出的一步
3. 利用近似解加速求解SAT问题的启发式完全算法（荆明娥、周 电、唐璞山、周晓方)
摘要：结合DPLL 完全算法能够证明可满足性(SAT) 问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT 问题的启发式完全算法。 首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策。该算法引导完全算法优先搜索近似解所在的子空间,加速解器找到可满足解的过程,为SAT 问题的求解提供了一种新的有效途径。实验结果表明,该算法有效地提高了决策的精度和SAT 解决器的效率,对很多实例非常有效。
SAT(satisfiability) 问题是目前形式验证的核心引擎，尤其是在集成电路EDA 验证中,SAT 问题已被广泛应用于模型检验、等价性检验、设计错误诊断 、ATPG检验等,并且已经取得了很大进展。而在SAT 问题求解中,基于深度优先搜索的完全算法DPLL 受到更为广泛的关注,成为目前SAT 解决器的主流算法文章结合DPLL 算法和局部搜索算法的优点,提出了利用近似解加速求解SAT 问题的启发式完全算法。该决策策略与布尔约束推理(Boolean constraintpropagation , BCP) 过程相结合,确保在整个搜索过程中尽可能地使大多数子句满足,即子句的布尔值为真,加速解决器找到解的速度。具体来说DPLL 算法尽管可以给出无解的证明,但对于较大规模的实例却很耗时;而局部搜索算法可以快速给出最优解或者近似解,但不能证明无解。 结合二者的优点,文章中给出的算法利用局部搜索算法在很短时间内得到一个近似解,并将其作为DPLL 算法的初始输入引导DPLL算法优先搜索近似解所在的子空间,效率有很大的提高。将局部搜索算法和完全算法有效地结合在一起,并得到的较好的结果,为SAT 问题的解决提供了一个新的有效途径。
4.SAT问题中局部搜索法的改进（杨晋吉 苏开乐）
摘要：局部搜索方法在求解SAT问题的高效率使其成为一研究热点．提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束．使在局部搜索的开始阶段，可满足的子句数大大增加，减少了翻转的次数，加快了求解的速度．用该方法对目前的一些重要的sAT 问题的局部搜索算法(如WSAT，TSAT，NSAT，SDF等)进行改进。通过对不同规模的随机3一SAT问题的实例和一些不同规模的结构性sAT问题的实例，以及利用相变现象构造的难解sAT实例测试表明，改进后的这些局部搜索算法的求解效率有了很大的提高．该方法对其他局部搜索法的改进具有参考价值．
5. 一种新的SAT问题预处理算法（熊 伟．唐璞山）
摘 要： 提出了一项新的正向推理技术：对称扩展的一元子句推导(Symmetric Extended Unit Propagation) 与传统的一元子句推导技术相比．文中的方法通过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句。基于这项新技术实现了一个可满足性问题(SAT)预处理器Snowball。实验结果验证了该项技术的有效性，表明该预处理器Snowball能够有效地化简SAT问题的规模并减少解决SAT问题的时间.。
6. Finding Bugs Efficiently with a SAT Solver(Julian Dolby、Mandana Vaziri、Frank Tip)
ABSTRACT：We present an approach for checking code against rich specifications, based on existing work that consists of encoding the program in a relational logic and using a constraint solver to find specification violations. We improve the efficiency of this approach with a new encoding of the program that effectively slices it at the logical level with respect to the specification. We also present new encodings for integer values and arrays, enabling the verification of realistic fragments of code that manipulate both. Our technique can handle integers of much larger ranges than previously possible, and permits large sparse arrays to be handled efficiently.We present a soundness proof for our slicing algorithm and a general condition under which relational formulae may be sliced. We implemented our technique and evaluated it by checking data structure invariants of several classes taken from the Java Collections Framework. We also checked for violations of Java's equality contract in a variety of opensource programs, and found several bugs.
7.New Inference Rules for Max-SAT（ chuMin Li ）
Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving
加载中…