基于动态奖惩的分支策略的SAT完备算法

针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题,提出了基于动态奖惩的分支策略。首先,对每次单子句传播的变元进行惩罚,依据变元是否产生冲突和产生冲突的间隔,确立不同的惩罚函数;其次,在学习阶段,利用学习子句确定对构造冲突有益的变元,非线性增加它们的活跃度;最后,选择活跃度最大的变元作为新分支变元。在glucose3.0算法基础上,完成了改进的动态奖惩算法——AP7。实验结果表明,相比glucose3.0算法,AP7算法的剪枝率提高了14.2%~29.3%,少数算例剪枝率的提高可达51%,且改进后的AP7算法相比glucose3.0算法,运行时间缩短了7%以上。所提分支策略可以有效降低搜索树规模,使搜索树更加平衡,减少计算时间。     

基于变量混合特征的分支启发式策略

先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略,它因其稳健性而被广泛使用,但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题,本文提出了一种基于变量混合特征的分支启发式算法,目的是充分地利用参与冲突分析的变量所携带的不同信息特征来区分变量,来进一步指导变量活性增长.并将所提出的分支策略算法嵌入到Glucose4.1中形成求解器Glucose4.1+MFBS,通过对比测试,实验结果表明改进的分支算法比原本的VSIDS策略,具有一定的优势,求解明显个数增加.     

基于分支回溯的NAE-3SAT问题求解算法

NAESAT问题是可满足性问题的一个重要扩展,在集合分裂、最大割集等NP完全问题中有着重要的应用.针对NAESAT问题的泛化NAE-3SAT问题,提出了一个基于分支回溯的精确算法NAE.算法给出了多种化简规则,这些化简规则很好地提高了算法的时间效率.最后证明了算法在最坏情况下的时间复杂度上界为O(1.618n),其中n为公式中的变量数目.     

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

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

结合启发式算子的单变量边缘分布算法求解SAT问题

单变量边缘分布算法(UMDA)是一种新的进化算法,是求解复杂问题的一种有效算法.根据SAT问题的特点,本文提出了一种求解SAT问题的改进单变量边缘分布算法(HeUMDASAT),该算法结合SAT问题本身固有的结构信息与当前群体的优秀解所提供的全局信息,构造了一个新的启发算子,并将此算子结合到单变量边缘分布算法中.此算子不同于随机搜索算子,由其产生的个体可以使得算法跳出局部最优并探索新的潜在区域,并且加快算法的收敛速度.用SATLIB库中的标准SAT问题对HeUMDASAT算法进行测试,实验结果表明该算法在求解速度和成功率方面都有明显的改善.     

基于关键文字的求解SAT问题的启发式算法

逻辑公式的可满足问题的求解方法是近几年研究的重点,通过对逻辑公式的关键文字和骨干变元集的研究与分析,使用启发式算法寻找公式的关键文字,在公式化简中引入关键文字规则,给出了一种新的求解SAT问题的启发式算法。     

基于变量决策层的启发式变量选择策略

启发式分支策略是SAT求解器中不可或缺的一部分，直接影响求解器的效率。早期的启发式分支决策需要遍历整个子句数据库，效率比较低。随着独立变量状态衰减和（Variable State Independent Decaying Sum, VSIDS）分支策略的出现，SAT求解器的效率有所提高，但VSIDS策略以及它的延伸策略中变量的增量都只是与变量的冲突次数有关，没有考虑变量的决策层在分支策略中的影响。因此当发生冲突时，如果与冲突有关的变量的得分相同而决策层不同时，对于变量的选择就具有随机性。基于此，本文在阐述变量的决策层的重要性之后在VSIDS策略的基础上，提出一种基于变量决策层的启发式变量选择策略--HSVDL策略。然后通过实例显示HSVDL策略在变量决策阶段选择决策层低的变量的可能性比选择决策层高的变量的可能性要大，而且得分比较小，减少了内存的占用。最后通过实验表明HSVDL策略能够求解出更多的实例，求解器的效率也有所提高，说明该策略有一定的优势。     

基于加权平均值的一种分支启发式方法

在可满足性(Satisfiability,SAT)问题算法中提出有效的分支策略可以提高求解器的效率,文中主要从冲突分析的角度出发,依据变量是否发生冲突和冲突的次数,提出 一种基于加权平均值的分支启发式方法。该方法首先采用一组序列来记录变量是否参与冲突;其次赋予一个加权平均函数,依据变量的序列和决策层求出函数值;最后选择具有最大的函数值变量赋值,执行实例分析比较。由于该方法是对控制编码方法的改进,因此在进行例子分析时,采用了比较法和分析法,同时分析比较了所提方法、 SUM(Sum in experiment)策略和 ACIDS(Average Conflict-index Decision Score)策略。对SATLIB(SAT Little Information Bank)中的实例进行分析,结果表明所提方法能够实现更多子句被满足或最新冲突子句优先满足。     

基于演化算法的SAT问题求解

SAT问题即布尔可满足性问题是逻辑学的一个基本问题,也是计算机科学和人工智能研究的核心问题。寻找求解SAT问题的快速算法不仅在理论研究上而且在许多应用领域都具有极其重要的意义。本文讨论了基于演化算法的SAT问题求解方法。     

Solving SAT problem by heuristic polarity decision-making algorithm

This paper presents a heuristic polarity decision-making algorithm for solving Boolean satisfiability (SAT). The algorithm inherits many features of the current state-of-the-art SAT solvers, such as fast BCP, clause recording, restarts, etc. In addition, a preconditioning step that calculates the polarities of variables according to the cover distribution of Karnaugh map is introduced into DPLL procedure, which greatly reduces the number of conflicts in the search process. The proposed approach is implemented as a SAT solver named DiffSat. Experiments show that DiffSat can solve many "real-life" instances in a reasonable time while the best existing SAT solvers, such as Zchaff and MiniSat, cannot. In particular, DiffSat can solve every instance of Bart benchmark suite in less than 0.03 s while Zchaff and MiniSat fail under a 900 s time limit. Furthermore, DiffSat even outperforms the outstanding incomplete algorithm DLM in some instances.     

A branching heuristic for SAT solvers based on complete implication graphs

Science China Information Sciences - Given a set of radio broadcast programs, the radio broadcast scheduling problem is to allocate a set of devices to transmit the programs to achieve the optimal...     

多星联合动态调度问题的启发式算法研究

对地观测多星联合动态调度问题是一类复杂的调度问题。在对多星联合动态调度问题的动态来源进行深入分析的基础上,对该问题进行了统一描述。针对问题的特点,提出了一种基于规则的启发式求解算法,设计了最大竞争度的退出启发式规则和最小冲突度的插入启发式规则。最后给出了一个应用实例,对算法进行了验证。     

基于加强概率控制策略的SAT局部搜索算法

局部搜索算法是目前求解SAT问题比较有效的方法,而Sattime算法是在SAT国际大赛中获得大奖的一种典型局部搜索算法。在Sattime算法的求解过程中,记录变元翻转事件流数据库,通过数据分析与模式挖掘,发现Sattime算法的局部搜索行为中会出现相邻搜索步选择同一个变元的现象,即所谓的回环现象,从而降低了求解效率。为解决此问题,提出两种概率控制策略：加强子句选择策略和加强变元选择策略,并将这两种策略应用到Sattime算法中,形成新的局部搜索算法Sattime-P。实验结果表明,与Sattime算法相比,改进后的Sattime-P算法求解效率有显著的提升。该方法也对其他局部搜索算法的改进具有参考价值。     

基于频次的SAT问题学习子句混合评估算法

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器（GLUCOSE 4.1并行版本）为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。     

基于变元加权的一种求解SAT问题的新方法

研究合取范式可满足性的SAT问题作为一个NP完全问题,在计算机科学及组合优化问题领域中有着中心课题的重要地位。由于其NP问题的性质决定了它尚无通用快速的完全算法,因此基于“实验算法学”的思想,按照平均性态而不是最坏情况性态的原则,对具有启发式策略的不完全算法的研究成为近年来大家关注与努力的焦点。该文正是立足于此,提出了“加权消元”这一种全新而且高效的算法。     

矩形件优化排样的混合启发式方法

提出一种启发式递归与遗传算法相结合的混合启发式算法求解矩形件优化排样问题。首先给出一种启发式递归算法,利用该算法逐个从待排矩形件中生成局部利用率高的条料,直到所有待排矩形件均生成条料;利用遗传算法全局搜索能力强的特点,对这些条料序进行搜索重组,使其所用的板材数最少;最后再次利用遗传算法,对条料生成之前的矩形件种类序进行全局最优搜索,使总的板材利用率达到了最大。对两个典型实际算例进行计算,并与相关文献比较,结果表明了该算法的有效性。     

Fleet-sizing for multi-depot and periodic vehicle routing problems using a modular heuristic algorithm

In this paper, we address the problem of determining the optimal fleet size for three vehicle routing problems, i.e., multi-depot VRP, periodic VRP and multi-depot periodic VRP. In each of these problems, we consider three kinds of constraints that are often found in reality, i.e., vehicle capacity, route duration and budget constraints. To tackle the problems, we propose a new Modular Heuristic Algorithm (MHA) whose exploration and exploitation strategies enable the algorithm to produce promising results. Extensive computational experiments show that MHA performs impressively well, in terms of solution quality and computational time, for the three problem classes.