Random backtracking in backtrack search algorithms for satisfiability

This paper proposes the utilization of randomized backtracking within complete backtrack search algorithms for propositional satisfiability (SAT). In recent years, randomization has become pervasive in SAT algorithms. Incomplete algorithms for SAT, for example the ones based on local search, often resort to randomization. Complete algorithms also resort to randomization. These include state-of-the-art backtrack search SAT algorithms that often randomize variable selection heuristics. Moreover, it is plain that the introduction of randomization in other components of backtrack search SAT algorithms can potentially yield new competitive search strategies. As a result, we propose a stochastic backtrack search algorithm for SAT, that randomizes both the variable selection and the backtrack steps of the algorithm. In addition, we relate randomized backtracking with a more general form of backtracking, referred to as unrestricted backtracking. Finally, experimental results for different organizations of randomized backtracking are described and compared, providing empirical evidence that the new search algorithm for SAT is a very competitive approach for solving hard real-world instances.     

Combining the Scalability of Local Search with the Pruning Techniques of Systematic Search

Systematic backtracking is used in many constraint solvers and combinatorial optimisation algorithms. It is complete and can be combined with powerful search pruning techniques such as branch-and-bound, constraint propagation and dynamic variable ordering. However, it often scales poorly to large problems. Local search is incomplete, and has the additional drawback that it cannot exploit pruning techniques, making it uncompetitive on some problems. Nevertheless its scalability makes it superior for many large applications. This paper describes a hybrid approach called Incomplete Dynamic Backtracking, a very flexible form of backtracking that sacrifices completeness to achieve the scalability of local search. It is combined with forward checking and dynamic variable ordering, and evaluated on three combinatorial problems: on the n-queens problem it out-performs the best local search algorithms; it finds large optimal Golomb rulers much more quickly than a constraint-based backtracker, and better rulers than a genetic algorithm; and on benchmark graphs it finds larger cliques than almost all other tested algorithms. We argue that this form of backtracking is actually local search in a space of consistent partial assignments, offering a generic way of combining standard pruning techniques with local search.     

Upper bounds for objective functions of discrete competitive facility location problems

Under study is the problem of locating facilities when two competing companies successively open their facilities. Each client chooses an open facility according to his own preferences and return interests to the leader firm or to the follower firm. The problem is to locate the leader firm so as to realize the maximum profit (gain) subject to the responses of the follower company and the available preferences of clients. We give some formulations of the problems under consideration in the form of two-level integer linear programming problems and, equivalently, as pseudo-Boolean two-level programming problems. We suggest a method of constructing some upper bounds for the objective functions of the competitive facility location problems. Our algorithm consists in constructing an auxiliary pseudo-Boolean function, which we call an estimation function, and finding the minimum value of this function. For the special case of the competitive facility location problems on paths, we give polynomial-time algorithms for finding optimal solutions. Some results of computational experiments allow us to estimate the accuracy of calculating the upper bounds for the competitive location problems on paths.     

Local search with a generalized neighborhood in the optimization problem for pseudo-Boolean functions

In the optimization problem for pseudo-Boolean functions we consider a local search algorithm with a generalized neighborhood. This neighborhood is constructed for a locally optimal solution and includes nearby locally optimal solutions. We present some results of simulations for pseudo-Boolean functions whose optimization is equivalent to the problems of facility location, set covering, and competitive facility location. The goal of these experiments is to obtain a comparative estimate for the locally optimal solutions found by the standard local search algorithm and the local search algorithm using a generalized neighborhood.     

Analysis and Solving SAT and MAX-SAT Problems Using an L-partition Approach

In this paper, we study SAT and MAX-SAT using the integer linear programming models and L-partition approach. This approach can be applied to analyze and solve many discrete optimization problems including location, covering, scheduling problems. We describe examples of SAT and MAX-SAT families for which the cardinality of L-covering of the relaxation polytope grows exponentially with the number of variables. These properties are useful in analysis and development of algorithms based on the linear relaxation of the problems. Besides we present the L-class enumeration algorithm for SAT using the L-partition approach. In addition we consider an application of this algorithm to construct exact algorithm and local search algorithms for the MAX-SAT problem.     

Runtime Analysis of Ant Colony Optimization with Best-So-Far Reinforcement

The paper provides some theoretical results on the analysis of the expected time needed by a class of Ant Colony Optimization algorithms to solve combinatorial optimization problems. A part of the study refers to some general results on the expected runtime of the considered class of algorithms. These results are then specialized to the case of pseudo-Boolean functions. In particular, three well known functions and a combination of two of them are considered: the OneMax, the Needle-in-a-Haystack, the LeadingOnes, and the OneMax-Needle-in-a-Haystack. The results obtained for these functions are also compared to those from the well-investigated (1+1)-Evolutionary Algorithm. The results shed light on a suitable parameter choice for the considered class of algorithms. Furthermore, it turns out that for two of the four studied problems, the expected runtime for the considered class, expressed in terms of the problem size, is of the same order as that for (1+1)-Evolutionary Algorithm. For the other two problems, the results are significantly in favour of the considered class of Ant Colony Optimization algorithms.      

Analyzing the Complexity of Finding Good Neighborhood Functions for Local Search Algorithms

A drawback to using local search algorithms to address NP-hard discrete optimization problems is that many neighborhood functions have an exponential number of local optima that are not global optima (termed L-locals). A neighborhood function η is said to be stable if the number of L-locals is polynomial. A stable neighborhood function ensures that the number of L-locals does not grow too large as the instance size increases and results in improved performance for many local search algorithms. This paper studies the complexity of stable neighborhood functions for NP-hard discrete optimization problems by introducing neighborhood transformations. Neighborhood transformations between discrete optimization problems consist of a transformation of problem instances and a corresponding transformation of solutions that preserves the ordering imposed by the objective function values. In this paper, MAX Weighted Boolean SAT (MWBS), MAX Clause Weighted SAT (MCWS), and Zero-One Integer Programming (ZOIP) are shown to be NPO-complete with respect to neighborhood transformations. Therefore, if MWBS, MCWS, or ZOIP has a stable neighborhood function, then every problem in NPO has a stable neighborhood function. These results demonstrate the difficulty of finding effective neighborhood functions for NP-hard discrete optimization problems.This research is supported in part by the Air Force Office of Scientific Research (F49620-01-1-0007, FA9550-04-1-0110).     

Solving the weighted MAX-SAT problem using the dynamic convexized method

Satisfiability (SAT) and maximum satisfiability (MAX-SAT) are difficult combinatorial problems that have many important real-world applications. In this paper we investigate the performance of the dynamic convexized method based heuristics on the weighted MAX-SAT problem. We first present an auxiliary function which is constructed based on a penalty function, and minimize the function by a local search method which can escape successfully from previously converged local minimizers by increasing the value of a parameter. Two algorithms of the approach are implemented and compared with the Greedy Randomized Adaptive Search Procedure (GRASP) and the GRASP with Path Relinking (GRASP + PR). Experimental results illustrate efficient and faster convergence of our two algorithms.     

Using automatic programming to generate state-of-the-art algorithms for random 3-SAT

The paper focuses on automatic programming and how to synthesize stochastic local search algorithms using automatic design of algorithms through evolution (ADATE). The main goal is to provide support for the hypothesis that automatic programming can generate competitive heuristic algorithms. A well studied and highly optimized SAT solver, G2WSAT, is used as a case study. The results indicate that automatic programming is an effective design tool for heuristics and that there may be many well studied optimization problems that could benefit from the ADATE system and the specification methodology that we describe.     

On the final steps of Newton and higher order methods

The Newton method is one of the most used methods for solving nonlinear system of equations when the Jacobian matrix is nonsingular. The method converges to a solution with Q-order two for initial points sufficiently close to the solution. The method of Halley and the method of Chebyshev are among methods that have local and cubic rate of convergence. Combining these methods with a backtracking and curvilinear strategy for unconstrained optimization problems these methods have been shown to be globally convergent. The backtracking forces a strict decrease of the function of the unconstrained optimization problem. It is shown that no damping of the step in the backtracking routine is needed close to a strict local minimizer and the global method behaves as a local method. The local behavior for the unconstrained optimization problem is investigated by considering problems with two unknowns and it is shown that there are no significant differences in the region where the global method turn into a local method for second and third order methods. Further, the final steps to reach a predefined tolerance are investigated. It is shown that the region where the higher order methods terminate in one or two iteration is significantly larger than the corresponding region for Newton’s method.     

Running time experiments on some algorithms for solving propositional satisfiability problems

Satisfiability problems are of importance for many practical problems. They are NP-complete problems. However, some instances of the SAT problem can be solved efficiently. This paper reports on a study concerning the behaviour of a variety of algorithmic approaches to this problem tested on a set of problems collected at FAW. The results obtained give a lot of insight into the algorithms and problems, yet also show some general technical and methodological problems associated with such comparisons.     

Recognition problems for special classes of polynomials in 0–1 variables

This paper investigates the complexity of various recognition problems for pseudo-Boolean functions (i.e., real-valued functions defined on the unit hypercubeB ⁿ = {0, 1} ⁿ ), when such functions are represented as multilinear polynomials in their variables. Determining whether a pseudo-Boolean function (a) is monotonic, or (b) is supermodular, or (c) is threshold, or (d) has a unique local maximum in each face ofB ⁿ , or (e) has a unique local maximum inB ⁿ , is shown to be NP-hard. A polynomial-time recognition algorithm is presented for unimodular functions, previously introduced by Hansen and Simeone as a class of functions whose maximization overB ⁿ is reducible to a network minimum cut problem.     

Simulated annealing for the unconstrained quadratic pseudo-Boolean function

In this paper, we develop a simulated annealing (SA) based heuristic for the unconstrained quadratic pseudo-Boolean function. An algorithm that solves the problem in O(n²) at each temperature of the cooling schedule is given. The performance of SA based heuristic is compared with existing bounding algorithms for this problem. Computational results and comparisons on several hundred test problems demonstrate the efficiency of our heuristic in terms of solution quality and computational time. A new set of hard test problems with their best solution is provided to facilitate future comparison.     

AN ADAPTIVE NONMONOTONIC TRUST REGION METHOD WITH CURVILINEAR SEARCHES

In this paper,an algorithm for unconstrained optimization that employs both trustregion techniques and curvilinear searches is proposed.At every iteration,we solve thetrust region subproblem whose radius is generated adaptively only once.Nonmonotonicbacktracking curvilinear searches are performed when the solution of the subproblem isunacceptable.The global convergence and fast local convergence rate of the proposedalgorithms are established under some reasonable conditions.The results of numericalexperiments are reported to show the effectiveness of the proposed algorithms.     

A competitive and cooperative approach to propositional satisfiability

Propositional satisfiability (SAT) has attracted considerable attention recently in both Computer Science and Artificial Intelligence, and a lot of algorithms have been developed for solving SAT. Each SAT solver has strength and weakness, and it is difficult to develop a universal SAT solver which can efficiently solve a wide range of SAT instances. We thus propose parallel execution of SAT solvers each of which individually solves the same SAT instance simultaneously. With this competitive approach, a variety of SAT instances can be solved efficiently in average. We then consider a cooperative method for solving SAT by exchanging lemmas derived by conflict analysis among different SAT solvers. To show the usefulness of our approach, we solve SATLIB benchmark problems, planning benchmark problems as well as the job-shop scheduling problem with good performance. The system has been implemented in Java with both systematic and stochastic solvers.     

Randomized Algorithms with Splitting: Why the Classic Randomized Algorithms Do Not Work and How to Make them Work

We show that the original classic randomized algorithms for approximate counting in NP-hard problems, like for counting the number of satisfiability assignments in a SAT problem, counting the number of feasible colorings in a graph and calculating the permanent, typically fail. They either do not converge at all or are heavily biased (converge to a local extremum). Exceptions are convex counting problems, like estimating the volume of a convex polytope. We also show how their performance could be dramatically improved by combining them with the classic splitting method, which is based on simulating simultaneously multiple Markov chains. We present several algorithms of the combined version, which we simple call the splitting algorithms. We show that the most advance splitting version coincides with the cloning algorithm suggested earlier by the author. As compared to the randomized algorithms, the proposed splitting algorithms require very little warm-up time while running the MCMC from iteration to iteration, since the underlying Markov chains are already in steady-state from the beginning. What required is only fine tuning, i.e. keeping the Markov chains in steady-state while moving from iteration to iteration. We present extensive simulation studies with both the splitting and randomized algorithms for different NP-hard counting problems.     

An improved SAT formulation for the social golfer problem

The Social Golfer Problem (SGP) is a sports scheduling problem that exhibits a lot of symmetry and has recently attracted significant attention. In this paper, we first revisit an existing SAT encoding for the SGP and correct some of its clauses. We then propose a change in the encoding that significantly reduces the number of variables for all instances. We achieve considerable performance improvements when solving many SGP instances with common SAT solvers using local search and complete backtracking. This makes SAT formulations a more promising approach for solving the SGP than previously.     

一簇非线性等式约束优化问题的过滤线搜索修正正割方法

本文提供了一簇新的过滤线搜索修正正割方法求解非线性等式约束优化问题.新算法簇的特点是:用修正正割算法簇中的一个算法获得搜索方向,回代线搜索技术得到步长,过滤准则用来决定是否接受步长,引入二阶校正技术减少不可行性并克服Maratos效应.在合理的假设条件下,分析了算法的总体收敛性.并证明了,通过附加二阶校正步,算法簇克服了Maratos效应,并二步Q-超线性收敛到满足二阶充分最优条件的局部解.数值结果表明了所提供的算法具有有效性.     

非线性等式约束优化问题的仿射信赖域方法

提出非线性等式和有界约束优化问题的结合非单调技术的仿射信赖域方法. 结合信赖域方法和内点回代线搜索技术, 每一步迭代转到由一般信赖域子问题产生的回代步中且满足严格内点可行条件. 在合理的假设条件下, 证明了算法的整体收敛性和局部超线性收敛速率. 最后, 数值结果表明了所提供的算法具有有效性.     

The Million-Variable “March” for Stochastic Combinatorial Optimization

Combinatorial optimization problems have applications in a variety of sciences and engineering. In the presence of data uncertainty, these problems lead to stochastic combinatorial optimization problems which result in very large scale combinatorial optimization problems. In this paper, we report on the solution of some of the largest stochastic combinatorial optimization problems consisting of over a million binary variables. While the methodology is quite general, the specific application with which we conduct our experiments arises in stochastic server location problems. The main observation is that stochastic combinatorial optimization problems are comprised of loosely coupled subsystems. By taking advantage of the loosely coupled structure, we show that decomposition-coordination methods provide highly effective algorithms, and surpass the scalability of even the most efficiently implemented backtracking search algorithms.