زمان اجرا تجزیه و تحلیل مقایسه ای از الگوریتم های هیوریستیک برای مشکلات ارضا

The satisfiability problem is a basic core NP-complete problem. In recent years, a lot of heuristic algorithms have been developed to solve this problem, and many experiments have evaluated and compared the performance of different heuristic algorithms. However, rigorous theoretical analysis and comparison are rare. This paper analyzes and compares the expected runtime of three basic heuristic algorithms: RandomWalk, (1+11+1) EA, and hybrid algorithm. The runtime analysis of these heuristic algorithms on two 2-SAT instances shows that the expected runtime of these heuristic algorithms can be exponential time or polynomial time. Furthermore, these heuristic algorithms have their own advantages and disadvantages in solving different SAT instances. It also demonstrates that the expected runtime upper bound of RandomWalk on arbitrary k-SAT (k⩾3)(k⩾3) is O(n(k−1))O((k−1)n), and presents a k-SAT instance that has Θ(n(k−1))Θ((k−1)n) expected runtime bound.

The satisfiability problem (SAT) of a propositional formula plays a central role in computer science and artificial intelligence. It is the first proposed NP-complete problem [5,21] and one of the basic core NP-complete problems [10]. In addition to its theoretical importance, the SAT problem is also directly applied in VLSI formal verification, software automation, and so on. Researchers have been trying to look for an effective algorithm for the SAT problem. Since the SAT problem is an NPcomplete problem in nature, a polynomial algorithm is not currently available to solve it, although we cannot prove that such an algorithm does not exist. In fact, a basic conjecture of modern computer science and mathematics is that no polynomial algorithm exists for NP-complete problems. At present, the main methods for solving the SAT problems are complete algorithms [3,6,34] and incomplete algorithms [7,12,13,15,20,25,27,29,31,32]. There are several very successful complete algorithms (e.g., SATO [34]). A complete algorithm often explores the whole search space and can always determine whether a given propositional formula is satisfiable or not; however, its time complexity is usually exponential. An incomplete algorithm does not carry out a complete search on the search space; instead, it often explores some part of the search space using heuristic information within a limited time; however it does not give the correct answer with certainty. Since the 1990s, the use of incomplete algorithm for solving the SAT problem has grown quickly. The basic incomplete heuristic methods are RandomWalk algorithm [25], GSAT algorithm [13,31], WalkSat algorithm [32], UnitWalk [15],population-search-based evolutionary algorithms [7,12,20] and so on. In recent years, some powerful concepts and techniques of statistical physics have been applied to the SAT problem. One of these incomplete algorithms, known as “survey propagation” [4,22], which is based on statistical physics methods, shows good performance on some difficult randomly generated SAT instances. It is well known that one of the earliest applications of statistical physics in the optimization problem is the simulated annealing algorithm [19]. WalkSat [32] used a probability selection mechanism similar to that of the simulated annealing algorithm. For some heuristic algorithms for the SAT problem, theoretical results about computational complexities have been obtained to some extent. Papadimitiou [25] was the first to prove that the average time upper bound of RandomWalk for 2-SAT is O(n2). Schöning [29] presented a restarting local-search algorithm to show that, for any satisfiable k-CNF formula with n variables, the algorithm has to repeat O((2(1 − 1k))n) times, on average, to find a satisfying assignment. Specially if k = 3, the average time is O(1.334n) (the upper bound of an exhaustive search is O(2n)). There have been several improvements on the upper bound by hybrid algorithms based on randomized algorithms by Paturi et al. [27] and Schöning [29], e.g. O(1.324n) [18] and O(1.322n) [28]. Alekhnovich et al. [2] proved that, when the clause density is less than 1.63, the average time complexity of RandomWalk for 3-SAT is linear. Since there are many incomplete heuristic algorithms for SAT problems, comparing and understanding the working principals of these heuristic algorithms is useful. The first thing we have to accept is that no one algorithm beats all other algorithms on all problems. There have been many numerical experiments that compared various heuristic algorithms on SAT problems, but theoretical study has been rare. This paper analyzes and compares the expected running time of three basic heuristic algorithms: RandomWalk, (1+1) EA, and hybrid algorithm. We use absorbing Markov chains to model search processes of these heuristic algorithms, and use explicit expressions of the first hitting time of a Markov chain to analyze and estimate their expected runtime. Through runtime analysis of three SAT instances, we show that the expected runtime of these heuristic algorithms can be exponential or polynomial. We also find that these heuristic algorithms have their own comparative advantage under different circumstances. The rest of this paper is organized as follows. Section 2 introduces the concepts of the SAT problem, some heuristic algorithms for the SAT problem, and the first hitting time of an absorbing Markov chain. Section 3 discusses the worstcase bound and the worst-case example on RandomWalk. Section 4 analyzes and compares the expected runtime bounds of three heuristic algorithms on two 2-SAT instances. Section 5 presents our conclusions and suggestions for further research.

Incomplete heuristic algorithms are now among the most prominent and frequently applied techniques for SAT problems. Many experimental comparisons with different heuristic algorithms have been reported, although theoretic comparisons are rare. This paper contributes to the theory of heuristic algorithms for SAT problems. We derive the expected runtime bounds of RandomWalk on k-SAT problem. We construct two 2-SAT instances and provide analytic comparisons among RandomWalk, (1 + 1) EA, and hybrid algorithm on these instances. It is shown that these heuristic algorithms have their own advantages and disadvantages in solving two SAT instances and their expected runtime ranges from a polynomial time to an exponential time. Our analysis provides an insight into the runtime behavior among these heuristic algorithms. Admittedly, two SAT instances ψ1(x) and ψ2(x) considered in this paper are relatively simple. Future investigation should be extended to a broader class of SAT problems and more heuristic algorithms, such as UnitWalk [15] and PPSZ [27]. Theoretic runtime analysis and comparison for heuristic algorithms on the SAT problem lag far behind experimental comparisons. Effort should be made to fill in the gap between theoretical studies on SAT and the design and application of practical algorithms, even though such an investigation will be challenging.