SAT问题中局部搜索法的改进

局部搜索方法在求解SAT问题的高效率使其成为一研究热点．提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束．使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度．用该方法对目前的一些重要的SAT问题的局部搜索算法(如WSAT,TSAT,NSAT,SDF等)进行改进,通过对不同规模的随机3-SAT问题的实例和一些不同规模的结构性SAT问题的实例,以及利用相变现象构造的难解SAT实例测试表明,改进后的这些局部搜索算法的求解效率有了很大的提高．该方法对其他局部搜索法的改进具有参考价值。     

基于分组的启发式SAT新算法——DC&DS算法

目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题,转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性。     

MAX-SAT问题的一种改进的禁忌搜索算法

求解SAT问题的经典禁忌搜索算法TSSAT初始解是随机产生的,本文在传统的禁忌搜索算法的基础上提出了一种改进初始解的方法.通过对不同规模的随机SAT问题实例的测试表明,这种改进可以有效地提高禁忌搜索过程中求解SAT问题的效率.     

MAX-SAT问题一种改进的局部搜索算法

局部搜索算法是求解大规模SAT问题的高效算法。经典的局部搜索算法有GSAT、WSAT、TSAT、NSAT等,但这些算法的初始解都是随机产生的。本文提出了用单纯形法产生“初始概率”（每个变量取1的概率）,用“初始概率”对局部搜索算法中变量的初始随机指派进行适当的约束,使在局部搜索的开始阶段,满足的子句数大大增加,加快了收敛的速度。通过对不同规模的随机STA问题实例的实验表明,这些改进有效地提高了局部搜索算法求解SAT问题的效率。     

一个求解结构SAT问题的高效局部搜索算法

逻辑表达式可满足性(SAT)问题是第一个被证明的NP完全问题.它也是解决人工智能和计算理论中许多实际问题的基础.人们发现,对于某些类型的SAT问题,局部搜索算法要比一些传统的算法(例如Davis-Putnam过程)更为有效.在本文中,我们主要讨论如何用局部搜索算法求解结构SAT问题.我们对一个典型的局部搜索算法GSAT+walk做了改进与扩展.首先,我们除去了GSAT+walk中GSAT部分的"平移";其次,我们给每一个子句赋权,并在GSAT+walk的搜索过程中动态地调整子句的权.文中给出的实验结果表明改进后的新算法对于求解结构SAT问题非常有效.     

求解柔性作业车间调度问题的新型改进Jaya算法

为有效解决复杂的柔性作业车间调度问题,以最小化最大完成时间为目标,提出了一种结合了变邻域搜索算法的新型改进Jaya算法来求解。为不断挖掘和优化探索最优解,提高算法求解的结果质量,通过Jaya算法的原理重新提出一种解的更新机制,此外在Jaya算法原理的基础上嵌入一种变邻域搜索策略,并在传统邻域结构的基础上重新设计了两种新型邻域结构,扩大了邻域搜索范围,增强了Jaya算法的局部搜索能力,避免算法因失去解的多样性从而陷入局部最优。运用基准算例对该算法的求解性能进行了验证,并与其他算法的仿真结果进行对比,结果表明该改进算法的求解效率更高。     

模糊Job Shop调度中的混合搜索策略的研究

采用并行遗传算法作为全局搜索算法，提出一种混合搜索策略，用于求解模糊Job Shop调度问题．根据模糊Job Shop调度问题解的特征，提出基于关键工序的邻域选择方法，并将基于这种邻域选择方法的禁忌搜索算法作为局部搜索算法，加强了遗传算法局部搜索能力．针对13个困难benchmark问题的实验结果表明，在较短的时间内，混合搜索策略的算法得到的平均满意度比并行遗传算法提高4.67%，比TSAB算法提高5.76%．采用的禁忌搜索算法改善了遗传算法的局部搜索能力，说明提出的混合搜索策略是有效的．     

面向柔性作业车间调度问题的改进变邻域搜索算法

针对柔性作业车间调度问题的特点,提出一种求解该问题的改进变邻域搜索算法。结合问题特点设计合理的编码方式,采用遗传算法进行最优解搜索,将搜索的结果作为变邻域搜索算法的初始解,以提高初始解的质量。为提高局部搜索能力,设计3种不同的邻域结构,构建邻域结构集以产生邻域解,保证邻域解的搜索过程中解的可行性以提高求解效率。针对一系列典型的柔性作业车间调度问题的实例,运用所设计的改进变邻域搜索算法进行测试求解,并将计算结果与文献中其他算法的测试结果进行比较,验证了所提出方法求解柔性作业车间调度问题的可行性和有效性。     

求解模糊Job Shop调度的遗传算法与蚁群算法融合研究

提出一种算法融合策略,解决单一算法求解模糊Job Shop调度问题存在的不足,提高这类问题的求解质量.算法融合策略中,采用遗传算法和蚁群算法进行并行搜索;根据模糊Job Shop调度问题解的特征,提出基于关键工序的邻域选择方法,并将基于这种邻域选择方法的禁忌搜索算法作为局部搜索算法,加强了遗传算法和蚁群算法的局部搜索能力.采用算法融合策略的混合优化算法对以13个难的benchmarks问题经模糊化得到实例进行求解,在较短的时间内,得到的平均满意度较并行遗传算法(PGA)提高5.24%、较TSAB算法提高8.40% .采用算法融合策略构造的混合算法具有较强的搜索能力,说明提出的混合搜索策略是有效的.     

基于动态行为选择的和声搜索算法

和声搜索算法是一种模拟音乐即兴创作过程的元启发式搜索,已成功应用于解决许多实际问题.针对高维函数优化问题,提出一种基于动态行为选择的和声搜索算法.在算法中新和声的即兴创作有3种策略,迭代过程中通过计算每个策略的即时价值和综合价值选择和声的即兴创作策略,并通过个体即兴创作策略选择方法提升寻优速度或避免陷入局部最优解.将所提出算法与9个改进和声搜索算法在22个基准函数上进行对比.实验结果表明,所提出算法具有较好的求解精度、稳定性和收敛速度,擅长于解决复杂的高维问题.     

求解SAT问题的拟人退火算法

该文利用一个简单的变换，将可满足性（SAT）问题转换为一个求相应目标函数最小值的优化问题，提出了一种用于跳出局部陷阱的拟人策略，基于模拟退火算法和拟人策略，为SAT问题的高效近注解得出了拟人退火算法（PA），该方法不仅具有模拟退火算法的全局收敛性质，而且具有一定的并行性，继承性。数值实验表明，对于本文随机产生的测试问题例，采用拟人策略的模拟退火算法的结果优于局部搜索算法，模拟退火算法以及近来国际上流行的WALKSAT算法，因此拟人退火算法是可行的和有效的。     

基于任务分配与调度的GSAT算法求解3-SAT问题

基于不同分配策略的云计算任务调度以及任务分配与调度的主要目的,提出了一种新的算法—求解3-SAT问题的基于任务分配与调度的GSAT算法。该算法将3-SAT问题中的每一个变量形成一个任务,在GSAT算法的基础上,引入任务分配与调度指导贪心搜索;同时,在保留原有贪心搜索的前提下,根据任务分配与调度的思想和3-SAT问题的特点,设计了两种新的策略—分配策略和调度策略共同完成整个贪心搜索过程。以标准的SATLAB库中变量个数从 20～250的3 700个不同规模的标准Uniform Random 3-SAT 问题对新的算法的性能进行了合理的测试,并与高效和普通性能改进的GSAT算法的结果作了比较,结果表明,该算法具有更高的成功率和更少的翻转次数。     

An Overview of Backtrack Search Satisfiability Algorithms

Propositional Satisfiability (SAT) is often used as the underlying model for a significant number of applications in Artificial Intelligence as well as in other fields of Computer Science and Engineering. Algorithmic solutions for SAT include, among others, local search, backtrack search and algebraic manipulation. In recent years, several different organizations of local search and backtrack search algorithms for SAT have been proposed, in many cases allowing larger problem instances to be solved in different application domains. While local search algorithms have been shown to be particularly useful for random instances of SAT, recent backtrack search algorithms have been used for solving large instances of SAT from real-world applications. In this paper we provide an overview of backtrack search SAT algorithms. We describe and illustrate a number of techniques that have been empirically shown to be highly effective in pruning the amount of search on significant and representative classes of problem instances. In particular, we review strategies for non-chronological backtracking, procedures for clause recording and for the identification of necessary variable assignments, and mechanisms for the structural simplification of instances of SAT.     

Adaptive memory-based local search for MAX-SAT

Many real world problems, such as circuit designing and planning, can be encoded into the maximum satisfiability problem (MAX-SAT). To solve MAX-SAT, many effective local search heuristic algorithms have been reported in the literature. This paper aims to study how useful information could be gathered during the search history and used to enhance local search heuristic algorithms. For this purpose, we present an adaptive memory-based local search heuristic (denoted by AMLS) for solving MAX-SAT. The AMLS algorithm uses several memory structures to define new rules for selecting the next variable to flip at each step and additional adaptive mechanisms and diversification strategies. The effectiveness and efficiency of our AMLS algorithm is evaluated on a large range of random and structured MAX-SAT and SAT instances, many of which are derived from real world applications. The computational results show that AMLS competes favorably, in terms of several criteria, with four state-of-the-art SAT and MAX-SAT solvers AdaptNovelty+, AdaptG2WSAT_p, IRoTS and RoTS.     

DSM中一种新型Cache一致性管理算法

存储器一致性管理是分布式共享存储器ＤＳＭ（ｄｉｓｔｒｉｂｕｔｅｄｓｈａｒｅｄｍｅｍｏｒｙ）系统的一个重要问题．在基于目录和所有者管理一致性的ＤＳＭ系统中,如何适时地更新所有者链表以及目录中关于所有者的信息是缩短查表时间的关键．本文介绍一种新型的链表更新算法的设计及其性能分析．分析表明,这种方案对维护存储器一致性来说,具有较灵活的适应性并有助于缩短查表时间,提高系统性能．该算法也可适用于树形层次结构的一致性管理方案．     

求解SAT问题的分级重排搜索算法

局部搜索法在ＳＡＴ问题上的成功运用已引起越来越广泛的重视,然而,它在面对不可满足问题例时的局限性不能不被考虑．分级重排搜索算法ＭＳＲＡ（ｍｕｌｔｉ－ｓｔａｇｅｓｅａｒｃｈｒｅａｒｒａｎｇｅ－ｍｅｎｔａｌｇｏｒｉｔｈｍ）正是为克服局部搜索法的不完备性而提出的,准确地讲,它是几种算法在思想上的集成,但为明确起见,把其最典型的分级重排过程作为名称．分级重排搜索算法在求解ＳＡＴ问题时,能表现出优于单一求解策略（如局部搜索法或回溯算法）的明显特性．由于可根据约束条件的强弱来估计ＳＡＴ问题例的可满足性,因此能够以此来确定更有效的求解策略．     

Improving configuration checking for satisfiable random <Emphasis Type="Italic">k</Emphasis>-SAT instances

Local search algorithms based on the Configuration Checking (CC) strategy have been shown to be efficient in solving satisfiable random k-SAT instances. The purpose of the CC strategy is to avoid the cycling problem, which corresponds to revisiting already flipped variables too soon. It is done by considering the neighborhood of the formula variables. In this paper, we propose to improve the CC strategy on the basis of an empirical study of a powerful algorithm using this strategy. The first improvement introduces a new and simple criterion, which refines the selection of the variables to flip for the 3-SAT instances. The second improvement is achieved by using the powerful local search algorithm Novelty with the adaptive noise setting. This algorithm enhances the efficiency of the intensification and diversification phases when solving k-SAT instances with k ≥ 4. We name the resulting local search algorithm Ncca+ and show its effectiveness when treating satisfiable random k-SAT instances issued from the SAT Challenge 2012. Ncca+ won the bronze medal of the random SAT track of the SAT Competition 2013.     

Heuristic-Based Backtracking Relaxation for Propositional Satisfiability

In recent years backtrack search algorithms for propositional satisfiability (SAT) have been the subject of dramatic improvements. These improvements allowed SAT solvers to successfully solve instances with thousands or tens of thousands of variables. However, many new challenging problem instances are still too hard for current SAT solvers. As a result, further improvements to SAT technology are expected to have key consequences in solving hard real-world instances. This paper introduces a new idea: choosing the backtrack variable using a heuristic approach with the goal of diversifying the regions of the space that are explored during the search. The proposed heuristics are inspired by the heuristics proposed in recent years for the decision branching step of SAT solvers, namely, VSIDS and its improvements. Completeness conditions are established, which guarantee completeness for the new algorithm, as well as for any other incomplete backtracking algorithm. Experimental results on hundreds of instances derived from real-world problems show that the new technique is able to speed SAT solvers, while aborting fewer instances. These results clearly motivate the integration of heuristic backtracking in SAT solvers.