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).     

A parsimony tree for the SAT2002 competition

Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem – they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.     

A parsimony tree for the SAT2002 competition

Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem — they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.     

Configuration landscape analysis and backbone guided local search.: Part I: Satisfiability and maximum satisfiability

Boolean satisfiability (SAT) and maximum satisfiability (Max-SAT) are difficult combinatorial problems that have many important real-world applications. In this paper, we first investigate the configuration landscapes of local minima reached by the WalkSAT local search algorithm, one of the most effective algorithms for SAT. A configuration landscape of a set of local minima is their distribution in terms of quality and structural differences relative to an optimal or a reference solution. Our experimental results show that local minima from WalkSAT form large clusters, and their configuration landscapes constitute big valleys, in that high quality local minima typically share large partial structures with optimal solutions. Inspired by this insight into WalkSAT and the previous research on phase transitions and backbones of combinatorial problems, we propose and develop a novel method that exploits the configuration landscapes of such local minima. The new method, termed as backbone-guided search, can be embedded in a local search algorithm, such as WalkSAT, to improve its performance. Our experimental results show that backbone-guided local search is effective on overconstrained random Max-SAT instances. Moreover, on large problem instances from a SAT library (SATLIB), the backbone guided WalkSAT algorithm finds satisfiable solutions more often than WalkSAT on SAT problem instances, and obtains better solutions than WalkSAT on Max-SAT problem instances, improving solution quality by 20% on average.     

H-GRASP：一种基于GRASP改进的混合SAT解法器*

为了改善GRASP的局限性,提出了一种能解决含有伪布尔（PB）和合取范式（CNF）混合约束问题的新的混合算法（H-GRASP）。该新算法采用了切削平面技术来提取PB约束条件之间的推论,并把它结合到普通的蕴涵图中,分析引起冲突的学习。与解决混合约束问题的其他两种方法——整数线性规划和纯基于SAT方法进行了彻底的比较。实验结果证明,H-GRASP方法从整体上大大减少了运行时间,加快了速度,同时还保证了加入这种方法的低耗费。     

Empirical investigation of stochastic local search for maximum satisfiability

The maximum satisfiability (MAX-SAT) problem is an important NP-hard problem in theory, and has a broad range of applications in practice. Stochastic local search (SLS) is becoming an increasingly popular method for solving MAX-SAT. Recently, a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances. However, the performance of CCLS on solving industrial MAX-SAT instances lags far behind. In this paper, we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAXSAT instances. First, we conduct experiments to analyze why CCLS performs poor on industrial instances. Then we propose a new strategy called additive BMS (Best from Multiple Selections) to ease the serious issue. By integrating CCLS and additive BMS, we develop a new SLS algorithm for MAXSAT called CCABMS, and related experiments indicate the efficiency of CCABMS. Also, we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT, and combine an effective initialization method with CCABMS, resulting in an enhanced algorithm. Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.     

求解可满足问题的调查传播算法以及步长的影响规律

该文研究了求解可满足问题的调查传播算法．该算法利用合取范式因子图进行调查消息的迭代,并根据每一次迭代的收敛情况对部分布尔变量赋值以对问题进行简化,最后把简化的问题利用局部搜索算法来求解．文中所谓步长是指在每一次迭代收敛之后根据赋值倾向进行赋值的变量个数．该文根据模拟实验观察到步长对调查传播算法的影响规律,即随着步长的递增,算法的时间耗费以及算法的有效性都有近似单调递减的趋势．     

The complexity of Boolean constraint satisfaction local search problems

The class of generalized satisfiability problems, first introduced by Schaefer in 1978, presents a uniform way of studying the complexity of Boolean constraint satisfaction problems with respect to the nature of constraints allowed in the input. We investigate the complexity of local search for this class of problems. We prove a dichotomy result: any generalized satisfiability local search problem is either in P or PLS-complete. In the meantime our study contributes to a better understanding of the complexity class PLS through the identification of an appropriate tool that captures reducibility among Boolean constraint satisfaction local search problems: sensitive implementation.     

The complexity of Boolean constraint satisfaction local search problems

The class of generalized satisfiability problems, first introduced by Schaefer in 1978, presents a uniform way of studying the complexity of Boolean constraint satisfaction problems with respect to the nature of constraints allowed in the input. We investigate the complexity of local search for this class of problems. We prove a dichotomy result: any generalized satisfiability local search problem is either in P or PLS-complete. In the meantime our study contributes to a better understanding of the complexity class PLS through the identification of an appropriate tool that captures reducibility among Boolean constraint satisfaction local search problems: sensitive implementation.     

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

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

Superior solution guided particle swarm optimization combined with local search techniques

Particle swarm optimization (PSO) is an evolutionary algorithm known for its simplicity and effectiveness in solving various optimization problems. PSO should have strong yet balanced exploration and exploitation capabilities to enhance its performance. A superior solution guided PSO (SSG-PSO) framework integrated with an individual level based mutation operator and different local search techniques is proposed in this study. In SSG-PSO, a collection of superior solutions is maintained and updated with the evolutionary process, such that each particle can comprehensively learn from the recorded superior solutions. In addition, to maintain the diversity of the particle swarm, SSG-PSO is combined with an individual level based mutation operator, which will be invoked when a particle is trapped in a local optimum (determined by the fitness and position states of the particle), thereby improving the adaptation and flexibility of each individual particle. Moreover, two gradient-based local search techniques, namely, the Broyden–Fletcher–Goldfarb–Shanno (BFGS) and Davidon–Fletcher–Powell (DFP) Quasi–Newton methods, and two derivative-free local search techniques, namely, pattern search and Nelder–Mead simplex search, are incorporated into SSG-PSO. The performances of SSG-PSO and that of its local search enhanced variants are extensively and comparatively studied on a suit of benchmark optimization functions.     

Nagging: A scalable fault-tolerant paradigm for distributed search

This paper describes nagging, a technique for parallelizing search in a heterogeneous distributed computing environment. Nagging exploits the speedup anomaly often observed when parallelizing problems by playing multiple reformulations of the problem or portions of the problem against each other. Nagging is both fault tolerant and robust to long message latencies. In this paper, we show how nagging can be used to parallelize several different algorithms drawn from the artificial intelligence literature, and describe how nagging can be combined with partitioning, the more traditional search parallelization strategy. We present a theoretical analysis of the advantage of nagging with respect to partitioning, and give empirical results obtained on a cluster of 64 processors that demonstrate nagging's effectiveness and scalability as applied to A^* search, β minimax game tree search, and the Davis–Putnam algorithm.     

Resolution versus Search: Two Strategies for SAT

The paper compares two popular strategies for solving propositional satisfiability, backtracking search and resolution, and analyzes the complexity of a directional resolution algorithm (DR) as a function of the width (w ^*) of the problem"s graph. Our empirical evaluation confirms theoretical prediction, showing that on low-w ^* problems DR is very efficient, greatly outperforming the backtracking-based Davis–Putnam–Logemann–Loveland procedure (DP). We also emphasize the knowledge-compilation properties of DR and extend it to a tree-clustering algorithm that facilitates query answering. Finally, we propose two hybrid algorithms that combine the advantages of both DR and DP. These algorithms use control parameters that bound the complexity of resolution and allow time/space trade-offs that can be adjusted to the problem structure and to the user"s computational resources. Empirical studies demonstrate the advantages of such hybrid schemes.     

Extractive single-document summarization based on genetic operators and guided local search

Due to the exponential growth of textual information available on the Web, end users need to be able to access information in summary form – and without losing the most important information in the document when generating the summaries. Automatic generation of extractive summaries from a single document has traditionally been given the task of extracting the most relevant sentences from the original document. The methods employed generally allocate a score to each sentence in the document, taking into account certain features. The most relevant sentences are then selected, according to the score obtained for each sentence. These features include the position of the sentence in the document, its similarity to the title, the sentence length, and the frequency of the terms in the sentence. However, it has still not been possible to achieve a quality of summary that matches that performed by humans and therefore methods continue to be brought forward that aim to improve on the results. This paper addresses the generation of extractive summaries from a single document as a binary optimization problem where the quality (fitness) of the solutions is based on the weighting of individual statistical features of each sentence – such as position, sentence length and the relationship of the summary to the title, combined with group features of similarity between candidate sentences in the summary and the original document, and among the candidate sentences of the summary. This paper proposes a method of extractive single-document summarization based on genetic operators and guided local search, called MA-SingleDocSum. A memetic algorithm is used to integrate the own-population-based search of evolutionary algorithms with a guided local search strategy. The proposed method was compared with the state of the art methods UnifiedRank, DE, FEOM, NetSum, CRF, QCS, SVM, and Manifold Ranking, using ROUGE measures on the datasets DUC2001 and DUC2002. The results showed that MA-SingleDocSum outperforms the state of the art methods.     

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.     

Solving the irregular strip packing problem via guided local search for overlap minimization

The irregular strip-packing problem (ISP) requires a given set of non-convex polygons to be placed without overlap within a rectangular container having a fixed width and a variable length, which is to be minimized. As a core sub-problem to solve ISP, we consider an overlap minimization problem (OMP) whose objective is to place all polygons into a container with given width and length so that the total amount of overlap between polygons is made as small as possible. We propose to use directional penetration depths to measure the amount of overlap between a pair of polygons, and present an efficient algorithm to find a position with the minimum overlap for each polygon when it is translated in a specified direction. Based on this, we develop a local search algorithm for OMP that translates a polygon in horizontal and vertical directions alternately. Then we incorporate it in our algorithm for OMP, which is a variant of the guided local search algorithm. Computational results show that our algorithm improves the best-known values of some well-known benchmark instances.     

LOCAL++: A C++ framework for local search algorithms

Local search is an emerging paradigm for combinatorial search which has recently been shown to be very effective for a large number of combinatorial problems. It is based on the idea of navigating the search space by iteratively stepping from one solution to one of its neighbors, which are obtained by applying a simple local change to it. In this paper we present LOCAL++, an object‐oriented framework to be used as a general tool for the development and implementation of local search algorithms in C++. The framework comprises a hierarchy of abstract template classes, one for each local search technique taken into account (i.e. hill‐climbing, simulated annealing and tabu search). Each class specifies and implements the invariant part of the algorithm built according to the technique, and is supposed to be specialized by a concrete class once a given search problem is considered, so as to implement the problem‐dependent part of the algorithm. LOCAL++ comprises also a set of abstract classes for creating new techniques by combining different search techniques and different neighborhood relations. The architecture of LOCAL++ provides a principled modularization for the solution of combinatorial search problems, and helps the designer deriving a neat conceptual scheme of the application, thus facilitating the development and debugging phases. LOCAL++ proved to be flexible enough for the implementation of the algorithms solving various scheduling problems. Copyright © 2000 John Wiley & Sons, Ltd.     

Extended guided tabu search and a new packing algorithm for the two-dimensional loading vehicle routing problem

In this paper, we develop an extended guided tabu search (EGTS) and a new heuristic packing algorithm for the two-dimensional loading vehicle routing problem (2L-CVRP). The 2L-CVRP is a combination of two well-known NP-hard problems, the capacitated vehicle routing problem, and the two-dimensional bin packing problem. It is very difficult to get a good performance solution in practice for these problems. We propose a meta-heuristic methodology EGTS which incorporates theories of tabu search and extended guided local search (EGLS). It has been proved that tabu search is a very good approach for the CVRP, and the guiding mechanism of the EGLS can help tabu search to escape effectively from local optimum. Furthermore, we have modified a collection of packing heuristics by adding a new packing heuristic to solve the loading constraints in 2L-CVRP, in order to improve the cost function significantly. The effectiveness of the proposed algorithm is tested, and proven by extensive computational experiments on benchmark instances.     

A multi-start evolutionary local search for the two-dimensional loading capacitated vehicle routing problem

This paper addresses an extension of the capacitated vehicle routing problem where customer demand is composed of two-dimensional weighted items (2L-CVRP). The objective consists in designing a set of trips minimizing the total transportation cost with a homogenous fleet of vehicles based on a depot node. Items in each vehicle trip must satisfy the two-dimensional orthogonal packing constraints. A GRASP×ELS algorithm is proposed to compute solutions of a simpler problem in which the loading constraints are transformed into resource constrained project scheduling problem (RCPSP) constraints. We denote this relaxed problem RCPSP-CVRP. The optimization framework deals with RCPSP-CVRP and lastly RCPSP-CVRP solutions are transformed into 2L-CVRP solutions by solving a dedicated packing problem. The effectiveness of our approach is demonstrated through computational experiments including both classical CVRP and 2L-CVRP instances. Numerical experiments show that the GRASP×ELS approach outperforms all previously published methods.     

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

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