一种求解布尔不可满足子式的局部搜索算法

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少。因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式。通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法。     

Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques

Some search problems are most directly specified by conjunctions of (sets of) disjunctions of pseudo-Boolean (PB) constraints. We study a logic PL ^PB whose formulas are of such form, and design local-search methods to compute models of PL ^PB theories. In our approach we view a PL ^PB theory T as a data structure, a concise representation of a certain propositional conjunctive normal form (CNF) theory cl(T) logically equivalent to T. The key idea is an observation that parameters needed by local-search algorithms for CNF theories, such as walksat, can be estimated on the basis of T without the need to compute cl(T) explicitly. We compare our methods to a local-search algorithm wsat(oip). The experiments demonstrate that our approach performs better. In order for wsat(oip) to handle arbitrary PL ^PB theories, it is necessary to represent disjunctions of PB constraints by sets of PB constraints, which often increases the size of the theory dramatically. A better performance of our method underscores the importance of developing solvers that work directly on PL ^PB theories. This paper combines and extends results included in conference papers [14, 15].     

UC-based Approximate Incremental Reachability

In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in safety-critical areas. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This study analyzes and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, Unsatisfiable Core (UC)-based Approximate Incremental Reachability (UAIR), mainly utilizes the UC to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, this study uses the UC obtained by the satisfiability solver to construct the candidate safety invariant, and if the transition system itself is safe, the obtained initial invariant is only an approximation of the safety invariant. Then, while checking the safety, the study incrementally improves the candidate safety invariant until it finds a true invariant that proves the system is safe; if the system is unsafe, the method can finally find a counterexample to prove the system is unsafe. The brand new method exploits UCs for safety model checking and achieves good results. It is known that there is no absolute best method in the field of model checking. Although the proposed method cannot surpass the current mature methods such as IC3 and complement Approximate Reachability (CAR), in terms of the number of solvable benchmarks, the method in this paper can solve three cases that other mature methods are unable to solve. It is believed that the method can be a valuable addition to the model checking toolset.     

基于不可满足核的近似逼近可达性分析

近年来,形式化验证技术受到了越来越多的关注,它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支,具有十分广阔的发展前景.本文中我们研究并提出了一种新的模型检测技术,可以有效地对迁移系统进行模型检测,包括不安全性检测和证明安全性.与现有的模型检测算法不同,我们提出的这种方法——基于不可满足核（unsatisfiable core,UC）的近似逼近可达性分析（UC-based approximate incremental reachability,UAIR）,主要利用不可满足核来求解一系列的候选安全不变式直至生成最终的不变式,以此来实现安全性证明和不安全性检测（漏洞查找）.在基于SAT求解器的符号模型检测中,我们使用由可满足性求解器得到的UC构造候选安全不变式,如果迁移系统本身是安全的,我们得到的初始不变式只是安全不变式的一个近似.然后,我们在检查安全性的同时,逐步改进候选安全不变式,直到找到一个真正的不变式,证明系统是安全的;如果系统是不安全的,我们的方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法,我们利用不可满足核进行安全性模型检测,取得了相当好的效果.众所周知,模型检测领域没有绝对最好的方法,尽管我们的方法在基准的可解数量上无法超越当前的成熟方法例如IC3、CAR等,但是我们的方法却可以解出3个其他方法都无法解出的案例,相信本方法可以作为模型检测工具集很有价值的补充.     

一种SAT邻域的快速搜索算法

用局部搜索算法求解SAT问题．通常都需要在较大的邻域中。寻找合适的邻解。如果对邻域中的每个邻解。都通过重新判断每个子句是否为可满足来得到其可满足的子句个数．则时间耗费较多。已经有一些经典的处理方法．例如通过修改邻域结构．来减小搜索空间。从另外一个角度来考虑搜索过程．根据当前解和邻解的内在关系．介绍一种SAT邻域的快速搜索算法。该算法能在不影响解质量的前提下．快速寻找合适的邻解．从而进一步提高局部搜索算法的求解速度。另外．该算法还提供用于提高解质量的信息。有助于研究新的局部搜索算法。     

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

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

Survey Propagation：一种求解SAT的高效算法

Survey propagation是一种新生的SAT(CSP)算法。它基于统计物理的spin glass模型，针对具体问题进行纵览(survey)，从而极大地降低求解的复杂度。但sp算法在某些时候不收敛，或引导向错误的解。对此，G．Parisi提出一种复杂回溯(backtrack)算法，而作者在sp中加入简单回溯，也使一部分此类问题得到解决。     

SAT Local Search Algorithms: Worst-Case Study

Recent experiments demonstrated that local search algorithms (e.g. GSAT) are able to find satisfying assignments for many hard Boolean formulas. A wide experimental study of these algorithms demonstrated their good performance on some inportant classes of formulas as well as poor performance on some other ones. In contrast, theoretical knowledge of their worst-case behavior is very limited. However, many worst-case upper and lower bounds of the form 2 ⁿ (<1 is a constant) are known for other SAT algorithms, for example, resolution-like algorithms. In the present paper we prove both upper and lower bounds of this form for local search algorithms. The class of linear-size formulas we consider for the upper bound covers most of the DIMACS benchmarks; the satisfiability problem for this class of formulas is NP-complete.     

Guided Local Search for Solving SAT and Weighted MAX-SAT Problems

In this paper, we show how Guided Local Search (GLS) can be applied to the SAT problem and show how the resulting algorithm can be naturally extended to solve the weighted MAX-SAT problem. GLS is a general, penalty-based meta-heuristic, which sits on top of local search algorithms to help guide them out of local minima. GLS has been shown to be successful in solving a number of practical real-life problems, such as the traveling salesman problem, BT"s workforce scheduling problem, the radio link frequency assignment problem, and the vehicle routing problem. We present empirical results of applying GLS to instances of the SAT problem from the DIMACS archive and also a small set of weighted MAX-SAT problem instances and compare them with the results of other local search algorithms for the SAT problem.     

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

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

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

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

基于SAT方法进一步加速差分特征的搜索

回顾了孙等使用Matsui边界条件加速差分特征搜索的方法,为了进一步提高搜索效率,改进了Matsui边界条件以及利用Matsui边界条件加速差分特征自动化搜索的方法,并提出了一种改进的方法来搜索分组密码的最优差分特征。研究了线程数和询问条件的加速效果并提出了选择线程数以及询问条件的策略。使用STP和CryptoMiniSat分别搜索概率为2^-24、2^-25、2^-26的8轮SPECK96差分特征以及概率为2^-39的11轮HIGHT差分特征,并比较了在不同线程数和询问条件下求解SAT/SMT问题的耗时。研究发现线程数对搜索差分特征的耗时影响较大,而询问条件对搜索差分特征的耗时影响较小,从而提出了一种如何选择线程数和询问条件的策略。根据所提策略,使用改进的边界条件和方法搜索HIGHT的11轮最优差分特征,并首次获得了HIGHT的11轮最优差分特征的紧致概率,即2^-45。现有的11轮HIGHT最优差分特征概率的最紧致边界是P_Opt¹¹≥2     

Sequential search and its application to vehicle-routing problems

Local search is the most frequently used heuristic technique for solving combinatorial optimization problems. It is also the basis for modern metaheuristics, like, e.g., Tabu Search, and Variable Neighborhood Search. The paper introduces sequential search as a generic technique for the efficient exploration of local-search neighborhoods. One of its key concepts is the systematic decomposition of moves, which allows pruning within local search based on associated partial gains. The application of theoretical concepts to several well-known neighborhoods of the vehicle-routing problem (VRP) is demonstrated. Computational tests show substantial speedup factors, e.g., up to 10 000 for the 3-opt* neighborhood. This underlines the superiority of sequential search over straightforward techniques in the VRP context.     

基于Lucene的本地搜索引擎研究与实现

为了改善计算机传统搜索在效率和返回结果上的不足,基于Lucene全文检索高效、准确的特点,采用非结构化文档结构化的思想,提出了文档内容自然分片索引的方法,实现了一个针对本地资源的个性化搜索引擎。     

Local Search Algorithms for SAT: An Empirical Evaluation

Local search algorithms are among the standard methods for solving hard combinatorial problems from various areas of artificial intelligence and operations research. For SAT, some of the most successful and powerful algorithms are based on stochastic local search, and in the past 10 years a large number of such algorithms have been proposed and investigated. In this article, we focus on two particularly well-known families of local search algorithms for SAT, the GSAT and WalkSAT architectures. We present a detailed comparative analysis of these algorithms" performance using a benchmark set that contains instances from randomized distributions as well as SAT-encoded problems from various domains. We also investigate the robustness of the observed performance characteristics as algorithm-dependent and problem-dependent parameters are changed. Our empirical analysis gives a very detailed picture of the algorithms" performance for various domains of SAT problems; it also reveals a fundamental weakness in some of the best-performing algorithms and shows how this can be overcome.     

On the Quantum Query Complexity of Local Search in Two and Three Dimensions

The quantum query complexity of searching for local optima has been a subject of much interest in the recent literature. For the d-dimensional grid graphs, the complexity has been determined asymptotically for all fixed d≥5, but the lower dimensional cases present special difficulties, and considerable gaps exist in our knowledge. In the present paper we present near-optimal lower bounds, showing that the quantum query complexity for the 2-dimensional grid [n]² is Ω(n ^1/2?δ ), and that for the 3-dimensional grid [n]³ is Ω(n ^1?δ ), for any fixed δ>0.A general lower bound approach for this problem, initiated by Aaronson (based on Ambainis’ adversary method for quantum lower bounds), uses random walks with low collision probabilities. This approach encounters obstacles in deriving tight lower bounds in low dimensions due to the lack of degrees of freedom in such spaces. We solve this problem by the novel construction and analysis of random walks with non-uniform step lengths. The proof employs in a nontrivial way sophisticated results of Sárközy and Szemerédi, Bose and Chowla, and Halász from combinatorial number theory, as well as less familiar probability tools like Esseen’s Inequality.     

基于函数变换的求解SAT问题的新算法

提出了一种基于函数变换的求解SAT问题的新算法,这个新算法利用SAT问题自身的特点将判定问题转化为连续函数的求极值问题。随机选取一组初始值,利用最速下降法求解变换后的连续函数在每个初始值邻域内所能达到的局部极值,如果这个局部极值为0,则该SAT问题就是可满足的。实验结果表明：与现有的求解SAT问题的算法相比,基于函数变换的求解算法在求解速度、成功率和求解问题的规模等方面都有明显的提高。     

A tabu search approach to an urban transport problem in northern Spain

In this work we analyze an urban transport problem that the City Council of Burgos, a city in northern Spain, has posed to the authors. Given a fleet of buses and drivers, the problem consists in designing routes and assigning buses to the routes such that the service level is optimized. The optimality of the service level is measured in terms of the waiting time at the bus stops and the duration of the trip. Thus, the problem comprises two decision levels (route design and bus assignment) and differs from other urban transport models found in the literature. In order to solve the problem, we propose two algorithms: one with a local search strategy and another with a tabu search strategy. In both cases, the solutions of the two decision levels are modified in alternating steps. The proposed algorithms obtained significantly better results than the tools currently applied by the transport authorities. In addition, the solutions obtained are very robust with respect to variations on demand, as shown by the experiments.     

求解SAT问题的局部搜索算法及其平均时间复杂性分析

ＳＡＴ问题在人工智能、ＶＬＳＩ设计和计算机理论等领域有着广泛的应用背景，近年来，局部搜索算法在求解ＳＡＴ问题时得到了巨大的成功。本文除提出了多种改进策略之外，还对一般局部搜索算法进行了平均时间复杂性分析。     

可满足性问题全部解的求解算法

SAT问题在人工智能、计算机基础理论研究和人工智能等领域有着广泛的应用,近年来,证明该问题的可满足性取得了巨大的成功,但在求出SAT问题的所有解方面还有待进一步研究。利用一个简单的变换,将可满足性（SAT）问题转化为多项式形式,然后根据命题逻辑的性质以及多项式的性质,得到一个求解出SAT问题所有解的算法。实验结果显示该算法是有效和可行的。