基于动态奖惩的CDCL SAT求解器分支启发式算法

分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。     

一个求解SAT问题的新算法

基于对完备算法和非完备算法的研究,结合完备算法能够进行完备求解和不完备算法能够以较快速度进行求解的优点。提出一种新的求解SAT问题的算法——对子句分组、对分组求解的算法。该算法完备地对SAT子句分组,同时在分组求解时使用局部搜索方法以较快的速度求解。经过实验验证,结果表明该方法能明显提高求解效率。     

求解SAT问题的改进粒子群优化算法

利用限制哆公式的相关理论将可满足性问题（SAT）等价转换为定义在{0,1}^n上的多项式函数优化问题,并将二进制粒子群优化算法（BPSO）与局部爬山搜索策略相结合,给出了一种求解SAT问题的新算法：基于局部爬山搜索的改进二进制粒子群优化算法（简称IBPSO）．数值实验表明,对于随机产生的3-SAT问题测试实例,该算法的计算结果均优于著名的WalkSAT算法和SATI．3算法．     

利用近似解加速求解SAT问题的启发式完全算法

结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.     

带投资约束P-中位问题的混合蚁群算法

将投资限制引入经典约束p-中位问题,提出带投资的约束P-中位问题,该问题更适用于交通、物流等领域的设施选址。在深入分析带投资约束P-中位问题的数学模型的基础上,首先提出了适用于该问题求解的局部搜索策略;其次,将局部搜索策略与拉格朗日启发式算法和蚁群算法相结合,设计了求解该问题的拉格朗日混合蚁群算法。实验结果表明：带投资的约束P-中位问题能够根据投资金额规划不同的投资方案;且提出的混合蚁群算法较大程度上提高了蚁群算法和拉格朗日启发式算法的求解精度,具有较好的收敛性。     

求解虚拟企业资源结盟博弈的启发式群智能优化算法

通过对求解虚拟企业资源结盟博弈问题与求解经典SAT问题相似性的分析,提出了一种求解虚拟企业资源结盟博弈的启发式群智能优化算法.算法融合萤火虫优化算法与布谷鸟优化算法部分原理,并设计可行的交叉算子以及变异优化算子,能够修复不可行解并保持种群多样性.实验结果表明本文算法的迭代次数与搜索到的稳定联盟数成线性增长,较启发式遗传算法有着更好的爬山性能和搜索能力.     

使用输出分组和电路可满足性的等价性验证算法

介绍了一种使用电路可满足性解算器的组合电路等价性验证算法．对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题．同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间．实验结果表明,该算法是实用有效的．     

N皇后问题的启发式算法探讨

搜索策略的选择与设计是人工智能领域问题求解的核心问题之一,直接影响到问题求解过程中存储空间的占用和计算的复杂性,影响到问题求解的效率。在给出N皇后问题形式化描述和现有搜索算法的基础上,设计了3种解决N皇后问题的启发式算法,并将其与深度优先和宽度优先等搜索策略进行了分析和比较,得出了几点关于设计启发式算法的启示。     

两级定位-路径问题的变邻域人工蜂群算法

建立了两级定位-路径问题的数学模型,提出了一种求解该问题的人工蜂群算法。针对该算法容易出现早熟现象,将近年来国外出现的一种新颖的轨迹式启发式算法--变邻域搜索融入其中,由此提出三种变邻域搜索策略。基于不同变邻域搜索策略的人工蜂群算法和人工鱼群算法的求解效果进行对比仿真。实验结果表明,变邻域人工蜂群算法能有效求解两级定位-路径问题。     

正三角形容器内等圆Packing问题的启发式算法

等圆Packing问题研究如何将n个单位半径的圆形物体互不嵌入地置入一个边长尽量小的正三角形容器内,作为一类经典的NP难度问题,其有着重要的理论价值和广泛的应用背景.模拟退火算法是一种随机的全局寻优算法,通过将启发式格局更新策略与基于梯度法的局部搜索策略融入模拟退火算法,并与二分搜索相结合,提出一种求解正三角形容器内等圆Packing问题的启发式算法.该算法将启发式格局更新策略用来产生新格局和跳坑,用梯度法搜索新产生格局附近能量更低的格局,并用二分搜索得到正三角形容器的最小边长.对41个算例进行测试的实验结果表明,文中算法改进了其中38个实例的目前最优结果,是求解正三角形容器内等圆Packing问题的一种有效算法.     

一个适于形式验证的ATPG引擎

自动测试产生(ATPG)不仅应用于芯片测试向量生成，也是芯片设计验证的重要引擎之一．提出了一种组合电路测试产生的代数方法，既可作为组合验证的ATPG引擎，又可用于通常的测试产生．该算法充分发挥了二叉判决图(BDD)及布尔可满足性(SAT)的优势，通过启发式策略实现SAT算法与BDD算法的交替，防止因构造BDD可能导致的内存爆炸，而且使用增量的可满足性算法，进一步提高了算法的效率．实验结果表明了该算法的可行性和有效性．     

电路宽度制导的布尔推理

在基于逻辑电路的布尔推理过程中，经常用到二又判决图(BDD)与布尔可满足性(SAT)相结合的算法．由于电路宽度能很好地反映电路的复杂性，提出了一种基于电路宽度的启发式策略，根据电路宽度来实现SAT算法与BDD算法的交替．充分发挥两者的优势，不仅可以防止因构造BDD可能导致的内存爆炸，而且还能避免SAT算法可能遇到的超时现象．与以往同类策略相比，该启发式策略更节省计算资源，提高算法性能．针对组合电路的测试产生实验，证实了其在布尔推理中的效率．     

Efficient software product-line model checking using induction and a SAT solver

Software product line (SPL) engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT (Boolean satisfiability problem) solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram (BDD)-based techniques.     

基于多项式符号代数方法的高层次数据通路的等价验证

基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求.由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法.深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式.从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Gr(o)bner基计算的有效代数求解算法.针对不同基准数据通路的实验结果表明了该算法的有效性.     

Solving satisfiability in combinational circuits

As EDA evolves, researchers continue to find modeling tools to solve problems of test generation, design verification, logic, and physical synthesis, among others. One such modeling tool is Boolean satisfiability (SAT), which has very broad applicability in EDA. The authors review modern SAT algorithms, show how these algorithms can account for structural information in combinational circuits, and explain what recursive learning can add to SAT.     

Complete Boolean Satisfiability Solving Algorithms Based on Local Search

Boolean satisfiability (SAT) is a well-known problem in computer science, artificial intelligence, and operations research. This paper focuses on the satisfiability problem of Model RB structure that is similar to graph coloring problems and others. We propose a translation method and three effective complete SAT solving algorithms based on the characterization of Model RB structure. We translate clauses into a graph with exclusive sets and relative sets. In order to reduce search depth, we determine search order using vertex weights and clique in the graph. The results show that our algorithms are much more effective than the best SAT solvers in numerous Model RB benchmarks, especially in those large benchmark instances.     

UnitWalk: A new SAT solver that uses local search guided by unit clause elimination

In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([27,28] and [30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).     

UnitWalk: A new SAT solver that uses local search guided by unit clause elimination

In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds ([27,28] and [30,31]). We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT [34] and WalkSAT [33]) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete (PAC).     

On one class of decision diagrams

A class of decision diagrams for representation of the normal forms of Boolean functions was introduced. Consideration was given, in particular, to the disjunctive diagrams representing the disjunctive normal forms (DNF). In distinction to the binary decision diagrams (BDD) and reduced ordered binary decision diagram (ROBDD), the disjunctive diagram representing an arbitrary DNF is constructed in a time which is polynomial of the size of the DNF binary code. Corresponding algorithms were described, and the results were presented of the computer-aided experiments where the proposed diagrams were used to reduce the information content accumulated in the course of deciding hard variants of Boolean satisfiability problem (SAT).     

可满足性求解技术研究

求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点。最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望。