Algorithms for the maximum satisfiability problem

Old and new algorithms for the Maximum Satisfiability problem are studied. We first summarize the different heuristics previously proposed, i.e., the approximation algorithms of Johnson and of Lieberherr for the general Maximum Satisfiability problem, and the heuristics of Lieberherr and Specker, Poljak and Turzik for the Maximum 2-Satisfiability problem. We then consider two recent local search algorithmic schemes, the Simulated Annealing method of Kirkpatrick, Gelatt and Vecchi and the Steepest Ascent Mildest Descent method, and adapt them to the Maximum Satisfiability problem. The resulting algorithms, which avoid being blocked as soon as a local optimum has been found, are shown empirically to be more efficient than the heuristics previously proposed in the literature.     

Onk-positive satisfiability problem

An algorithm for solving the satisfiability problem is presented. It is proved that this algorithm solves 2-SAT and Horn-SAT in linear time andk-positive SAT (in which every clause contains at mostk positive literals) in timeO(|F|·ξ _n ^k ), where |F| is the length of inputF, n is the number of atoms occurring inF, and ξ _k is the greatest real number satisfying the equation . Compared with previous results, this nontrivial upper bound on time complexity could only be obtained fork-SAT, which is a subproblem ofk-positive SAT. Research partially supported by NSFC grant 221-4-1439. HUANG Xiong received his B.S. and M.S. degrees in computer science from Peking University in 1992 and 1995 respectively. Now he is a Ph.D. candidate in Beijing University of Aeronautics and Astronautics. His major research interests are design and analysis of algorithms, computational complexity, and satisfiability problem. LI Wei received his B.S. degree in mathematics from Peking University in 1966 and his Ph.D. degree in computer science from The University of Edinburgh in 1983. Since 1986, he has been a Professor in computer science at Beijing University of Aeronautics and Astronautics. He has published over 100 papers in the areas of concurrent programming languages, operational semantics, type theory, and logical foundation of artificial intelligence.     

On-line algorithms for polynomially solvable satisfiability problems

Given a propositional Horn formula, we show how to maintain on-line information about its satisfiability during the insertion of new clauses. A data structure is presented which answers each satisfiability question in O(1) time and inserts a new clause of length q in O(q) amortized time. This significantly outperforms previously known solutions of the same problem. This result is extended also to a particular class of non-Horn formulae already considered in the literature, for which the space bound is improved. Other operations are considered, such as testing whether a given hypothesis is consistent with a satisfying interpretation of the given formula and determining a truth assignment which satisfies a given formula. The on-line time and space complexity of these operations is also analyzed.     

Evolutionary algorithms for the multi‐objective test data generation problem

Automatic test data generation is a very popular domain in the field of search‐based software engineering. Traditionally, the main goal has been to maximize coverage. However, other objectives can be defined, such as the oracle cost, which is the cost of executing the entire test suite and the cost of checking the system behavior. Indeed, in very large software systems, the cost spent to test the system can be an issue, and then it makes sense by considering two conflicting objectives: maximizing the coverage and minimizing the oracle cost. This is what we did in this paper. We mainly compared two approaches to deal with the multi‐objective test data generation problem: a direct multi‐objective approach and a combination of a mono‐objective algorithm together with multi‐objective test case selection optimization. Concretely, in this work, we used four state‐of‐the‐art multi‐objective algorithms and two mono‐objective evolutionary algorithms followed by a multi‐objective test case selection based on Pareto efficiency. The experimental analysis compares these techniques on two different benchmarks. The first one is composed of 800 Java programs created through a program generator. The second benchmark is composed of 13 real programs extracted from the literature. In the direct multi‐objective approach, the results indicate that the oracle cost can be properly optimized; however, the full branch coverage of the system poses a great challenge. Regarding the mono‐objective algorithms, although they need a second phase of test case selection for reducing the oracle cost, they are very effective in maximizing the branch coverage. Copyright © 2011 John Wiley & Sons, Ltd.     

The complexity of the satisfiability problem for Krom formulas

We study the computational complexity of the satisfiability problem for Krom (CNF-2) formulas. Upper and lower bounds are obtained for several decidable classes of formulas determined by quantifier prefix and degree of predicate letters. For example, we show that determining satisfiability of Krom formulas with quantifier prefix of the form ……… is complete for deterministic exponential time, but that if the number of universal quantifiers is bounded then polynomial time suffices.     

An effective heuristic algorithm for the maximum satisfiability problem

Stochastic local search algorithms (SLS) have been increasingly applied to approximate solutions of the weighted maximum satisfiability problem (MAXSAT), a model for solutions of major problems in AI and combinatorial optimization. While MAXSAT instances have generally a strong intrinsic dependency between their variables, most of SLS algorithms start the search process with a random initial solution where the value of each variable is generated independently with the same uniform distribution. In this paper, we propose a new SLS algorithm for MAXSAT based on an unconventional distribution known as the Bose-Einstein distribution in quantum physics. It provides a stochastic initialization scheme to an efficient and very simple heuristic inspired by the co-evolution process of natural species and called Extremal Optimization (EO). This heuristic was introduced for finding high quality solutions to hard optimization problems such as colouring and partitioning. We examine the effectiveness of the resulting algorithm by computational experiments on a large set of test instances and compare it with some of the most powerful existing algorithms. Our results are remarkable and show that this approach is appropriate for this class of problems.     

Verification of consensus algorithms using satisfiability solving

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes.     

Algorithms for four variants of the exact satisfiability problem

We present four polynomial space and exponential time algorithms for variants of the E S problem. First, an O(1.1120ⁿ) (where n is the number of variables) time algorithm for the NP-complete decision problem of E 3-S , and then an O(1.1907ⁿ) time algorithm for the general decision problem of E S . The best previous algorithms run in O(1.1193ⁿ) and O(1.2299ⁿ) time, respectively. For the #P-complete problem of counting the number of models for E 3-S we present an O(1.1487ⁿ) time algorithm. We also present an O(1.2190ⁿ) time algorithm for the general problem of counting the number of models for E S ; presenting a simple reduction, we show how this algorithm can be used for computing the permanent of a 0/1 matrix.     

Genetic-fuzzy approach to the Boolean satisfiability problem

This study is concerned with the Boolean satisfiability (SAT) problem and its solution in setting a hybrid computational intelligence environment of genetic and fuzzy computing. In this framework, fuzzy sets realize an embedding principle meaning that original two-valued (Boolean) functions under investigation are extended to their continuous counterparts resulting in the form of fuzzy (multivalued) functions. In the sequel, the SAT problem is reformulated for the fuzzy functions and solved using a genetic algorithm (GA). It is shown that a GA, especially its recursive version, is an efficient tool for handling multivariable SAT problems. Thorough experiments revealed that the recursive version of the GA can solve SAT problems with more than 1000 variables     

Bee colony optimization for the satisfiability problem in probabilistic logic

This paper presents the first heuristic method for solving the satisfiability problem in the logic with approximate conditional probabilities. This logic is very suitable for representing and reasoning with uncertain knowledge and for modeling default reasoning. The solution space consists of variables, which are arrays of 0 and 1 and the associated probabilities. These probabilities belong to a recursive non-Archimedean Hardy field which contains all rational functions of a fixed positive infinitesimal. Our method is based on the bee colony optimizationmeta-heuristic. The proposed procedure chooses variables from the solution space and determines their probabilities combining some other fast heuristics for solving the obtained linear system of inequalities. Experimental evaluation shows a high percentage of success in proving the satisfiability of randomly generated formulas. We have also showed great advantage in using a heuristic approach compared to standard linear solver.     

The satisfiability problem in regular CNF-formulas

 In this paper we deal with the propositional satisfiability (SAT) problem for a kind of multiple-valued clausal forms known as regular CNF-formulas and extend some known results from classical logic to this kind of formulas. We present a Davis–Putnam-style satisfiability checking procedure for regular CNF-formulas equipped with suitable data structures and prove its completeness. Then, we describe a series of experiments for regular random 3-SAT instances. We observe that, for the regular 3-SAT problem with this procedure, there exists a threshold of the ratio of clauses to variables such that (i) the most computationally difficult instances tend to be found near the threshold, (ii) there is a sharp transition from satisfiable to unsatisfiable instances at the threshold and (iii) the value of the threshold increases as the number of truth values considered increases. Instances in the hard part provide benchmarks for the evaluation of regular satisfiability solvers.     

A comparative runtime analysis of heuristic algorithms for satisfiability problems

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+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) is O(n(k−1)), and presents a k-SAT instance that has Θ(n(k−1)) expected runtime bound.     

Evolutionary algorithms for continuous-space optimisation

From a global viewpoint, evolutionary algorithms (EAs) working on continuous search-spaces can be regarded as homogeneous Markov chains (MCs) with discrete time and continuous state. We analyse from this viewpoint the (1?+?1)EA on the inclined plane fitness landscape, and derive a closed-form expression for the probability of occupancy of an arbitrary target zone, at an arbitrary iteration of the EA. For the hitting-time of an arbitrary target zone, we provide lower and upper bounds, as well as an asymptotic limit. Discretization leads to an MC with discrete time, whose simple structure is exploited to carry out efficient numerical investigations of the theoretical results obtained. The numerical results thoroughly confirm the theoretical ones, and also suggest various conjectures which go beyond the theory.     

Combining finite learning automata with GSAT for the satisfiability problem

A large number of problems that occur in knowledge-representation, learning, very large scale integration technology (VLSI-design), and other areas of artificial intelligence, are essentially satisfiability problems. The satisfiability problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. The growing need for more efficient and scalable algorithms has led to the development of a large number of SAT solvers. This paper reports the first approach that combines finite learning automata with the greedy satisfiability algorithm (GSAT). In brief, we introduce a new algorithm that integrates finite learning automata and traditional GSAT used with random walk. Furthermore, we present a detailed comparative analysis of the new algorithm's performance, using a benchmark set containing randomized and structured problems from various domains.     

Sorting,linear time and the satisfiability problem

Let DLIN denote the class of problems that are computable withinO(n/logn) uniform time on a RAM which can read its input (of lengthn) in blocks and which only uses integersO(n/logn). We prove that the sorting problem belongs to DLIN and formulate the Linear Time Thesis: Each problem computable by a linear time bounded algorithm (in an intuitive sense) belongs to DLIN. We also study the subclass DTIME_SORT(n) of problems computable within linear time on a Turing machine using in addition a fixed number of sortings, and we show how the reductions of this class, so-called sort-lin reductions, are useful to classify NP problems: e.g. there is a sort-lin reduction from SAT to 3-SAT (using no sorting) and a sort-lin reduction from the NP-complete graph problem KERNEL to SAT (but we do not know of any similar reduction in DTIME(n)). Similarly, problem 2-SAT is linearly equivalent to the problem of Horn renaming (via sort-lin reductions). Finally, SAT is compared with many other combinatorial problems. A problemA is SAT-easy (resp. SAT-hard) if there is a sort-lin reduction fromA to SAT (resp. SAT toA). A SAT-equivalent problem is a problem both SAT-easy and SAT-hard. It is shown that the class of SAT-easy (resp. SAT-equivalent) problems is very large and that its generalization to so-called special clauses or, more generally, regular clauses, does not enlarge it. Moreover, we justify our opinion that problem SAT is, in some sense, a minimal NP-complete problem.     

On optimizing the satisfiability (SAT) problem

1IntroductionThesatisfiability(SAT)problemistodeterminewhetherthereexistsanassignmentofvaluesin{0,1}toasetofBooleanvariables{x1,xm}thatmakesaconjunctivenormalform(CNF)formulatrue.ThesatisfiabilityproblemofaCNFformulawithatmostlliteralsineachclauseiscalledthel-SATproblem.Theoretically,for>3,theSATproblemisawell-knownNP-completeproblem.Andthus,thereexistsnopolynomialtimealgorithmfortheSATproblemontheassumptionthatPNP.Ontheotherhand,theSATproblemisfundamentalinsolvingmanypracticalprob…     

An Algorithm Based on Tabu Search for Satisfiability Problem

In this paper,a computationally effective algorithm based on tabu search for solving the satisfiability problem(TSSAT)is proposed.Some novel and efficient heuristic strategies for generating candidate neighborhood of the curred assignment and selecting varibables to be flipped are presented. Especially,the aspiration criterion and tabu list tructure of TSSAT are different from those of traditional tabu search.Computational experiments on a class of problem insteances show that,TSSAT,in a reasonable amount of computer time ,yields better results than Novelty which is currently among the fastest known.Therefore TSSAT is feasible and effective.     

求解多文字可满足SAT问题的置信传播算法

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真.多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真.显然,此问题仍然是一个NP难问题.为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法.最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法.     

约束可满足性中求解RB模型实例的算法综述

约束满足问题是人工智能领域中最基本的NP完全问题之一。多年来,随着约束满足问题的深入研究,国内外学者提出多种实例模型。其中,RB模型是一种能生成具有精确相变的增长域约束满足问题实例,其求解难度极具挑战性。为了寻找其求解的新型高效算法,促进约束可满足问题的RB模型求解算法领域的研究,首先从约束满足问题的模型发展、求解技术进行分析;其次,对各类求解RB模型实例算法进行梳理,将求解的算法文献划分为回溯启发式类、信息传播类和元启发式类相关改进算法,从算法原理、改进策略、收敛性和精确度等方面进行对比综述;最后给出求解RB模型实例算法的研究趋势和发展方向。