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

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

基于学习子句删除策略的SAT求解器分支策略

对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突.但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响.针对此问题,提出了 一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度.基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD.以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较.实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了 15.5％.在2019年的例子测试中,Maple-DL_VDALCD 比 MapleLCMDistChronoBT-DL-v2.1 多求出 17个例子,增加了 7.6％.     

求解QBF 问题的启发式调查传播算法

提出了一种启发式调查传播算法,并基于该算法设计了一种QBF(quantified Boolean formulae)求解器——HSPQBF(heuristic survey propagation algorithm for solving QBF)系统.它将Survey Propagation信息传递方法应用到QBF求解问题中.利用Survey Propagation作为启发式引导DPLL(Davis,Putnam,Logemann and Loveland)算法,选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,HSPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而能够提高QBF问题的求解效率.实验结果表明,HSPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值.     

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

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

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

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

基于一种新型分支定价算法的电动车支线镇际快递配送路径规划研究

针对由电动汽车支持的支线镇际快递配送系统,提出一类新型的分支定价算法实现对车辆和货物的路径规划。研究利用时空网络将时间离散化构建模型,同时考虑了车辆资源、仓储资源和充电桩资源的管理问题。在分支定价算法中,分支策略和割平面策略的结合有效削弱了时间离散化所带来的对称性问题。强化策略则通过对生成路径变量进行有效筛选,并利用求解器帮助算法快速找到高质量可行解。实验将分支定价算法和商用求解器求解以及基于列生成的启发式算法进行对比,结果表明分支定价算法在精确求解小规模问题和启发求解中等规模问题时都具有明显优势,从而能有效地对该问题进行求解。     

基于问题结构的启发式策略在析取时态问题求解中的应用

智能规划和调度中的许多时态(或时序)问题可以表达为析取时态问题(DTP).目前,多数析取时态问题求解器将析取时态问题看作约束可满足问题(CSP)或可满足问题(SAT),并使用标准的CSP(或SAT)技术来求解DTP.虽然这些技术在求解DTP时已经可以达到较好的效率,然而,文献中极少研究者关注利用DTP本身特殊的结构中隐含的信息来帮助DTP求解.尝试从DTP的拓扑结构中提取出一种启发式策略.这种启发式策略试图从DTP的结构中提取出定性和定量的标准(TVS)来选择优先赋给当前变量的值,同时基于这种定量值选择标准设计了一个动态变量选择策略(TVO).这种技术基于定义的一种DTP的图模型--析取时态网络(DTN).实验结果显示TVS和TVO策略均可以有效减小搜索中节点访问次数;同时它与已有的RSV值选择策略效果相当,而TVO优于最少剩余值(MRV)方法(节省一个数量级以上的访问节点数);此外,配合其他CSP启发技术,可以得到一个高效的DTP求解算法DTN-DTP.     

一个基于最小冲突修补的动态约束满足求解算法

约束满足问题是人工智能中一个重要的研究方向,近年来,对动态变化的约束满足问题的研究逐渐成为该领域的热点.在目前该领域最流行的LC算法基础上,引入禁忌搜索策略,提出了一个基于最小冲突修补的算法Tabu_LC.算法在每次冲突调整时将所有冲突变量看成一个整体,并采用分支定界搜索策略求解冲突变量组成的子问题,极大地提高了求解效率.同时,在约束求解系统"明月1.0"架构下给出了算法的具体实现,并针对大量随机问题进行了对比实验.结果表明,Tabu_LC算法在求解效率和解的质量上都明显优于LC算法.     

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.     

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.     

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

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

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

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

Branch-and-Bound-Based Local Search Heuristics for Train Timetabling on Single-Track Railway Network

The modified formulation and two branch-and-bound-based local search heuristic algorithms for train timetabling in single-track railway network in the planning application are proposed. The original local search heuristic is modified such that when a neighbor of a currently tested resolved conflict for improvement is evaluated, the depth-first search branch-and-bound algorithm is employed with two branching rules: least-lower-bound and least-delay-time. The detailed implementation of the proposed heuristic algorithms are described, including the neighborhood definitions of overtaking and crossing conflicts, the procedure to detect overtaking and crossing conflicts, and a recursive procedure for the depth-first search branch-and-bound algorithm. The proposed heuristic algorithms, the original heuristic, the equivalent manual solution method and the exact solution method are compared using a toy problem and four problems (26-train, 50-train, 76-train and 108-train) in the Thailand Southern line railway network, which consisted of 266 single-track segments, 15 double-track segments, 282 stations/sidings, and total distance of 1577 km. The proposed heuristic algorithm with the least-lower-bound branching rule outperforms the other heuristics in terms of the solution quality with up to 2.827 % improvement over the equivalent manual solution method and less than 8 % optimality gap. The proposed heuristic algorithms require longer time to terminate than the original heuristic. The proposed heuristic algorithm with the least-lower-bound branching rule converges faster than that with the least-delay-time branching rule in all test problems. Based on the empirical results, the proposed heuristic algorithms are solvable in polynomial time. Furthermore, the proposed heuristic algorithm with the least-lower-bound branching rule is enhanced by embedding a uniform sampling strategy, and it is found that the total CPU time can be saved by about 50 % with marginally worse solution quality.     

改进的布尔冲突矩阵的高效属性约简算法

近年来,诸多学者喜欢用差别矩阵的方法来设计属性约简的算法,但由于计算差别矩阵不仅费时且还浪费空间,导致这些属性约简算法都不够理想。为了降低属性约简算法的复杂度,在布尔冲突矩阵的基础上,定义了一个启发函数,该函数能求出决策表中条件属性导致的冲突个数,同时给出了计算该启发函数的快速算法。然后用该启发函数设计了一个有效的基于改进的布尔冲突矩阵的不完备决策表的高效属性约简算法,该算法能够有效降低时间复杂度。最后实验结果说明了新算法的有效性。     

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures

Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g., model-checking, circuit testing, propositional planning) by encoding into SAT. However, a purely Boolean representation is not expressive enough for many other real-world applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in linear arithmetic logic (LAL), that is, the Boolean combination of propositional variables and linear constraints over numerical variables. In this paper we present MathSAT, a new, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art SAT solver with a dedicated mathematical solver for LAL. We improve MathSAT in two different directions. First, the top‐level line procedure is enhanced and now features a tighter integration between the Boolean search and the mathematical solver. In particular, we allow for theory-driven backjumping and learning, and theory-driven deduction; we use static learning in order to reduce the number of Boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stack-based interface that allows us to implement mathematical reasoning in an incremental and backtrackable way. Second, the mathematical solver is based on layering; that is, the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes call of the subsequent solvers superfluous. We provide a through experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several state-of-the-art decision procedures. We show that the behavior of MathSAT is often superior to its competitors, both on LAL and in the subclass of difference logic. This work has been partly supported by ISAAC, a European-sponsored project, contract no. AST3-CT-2003-501848; by ORCHID, a project sponsored by Provincia Autonoma di Trento; and by a grant from Intel Corporation. The work of T. Junttila has also been supported by the Academy of Finland, project 53695. S. Schulz has also been supported by a grant of the Italian Ministero dell'Istruzione, dell'Università e della Ricerca and the University of Verona.