The Research Of Algorithms For Minimum Satisfiability Problem Based On Local Search

The satisfiability problem is a non-deterministic polynomial complete problem that was proved first, namely, for a conjunction normal form, the problem is to find a candidate solution that makes the conjunction normal form true, or prove it to be false. The maximum satisfiability problem is a natural extension of the satisfiability problem, it is to find a candidate solution that makes the number of satisfied clauses maximum. In contrast to the maximum satisfiability problem, the minimum satisfiability problem is to find a candidate solution that makes the number of satisfied clauses minimum. Li Chumin professor comes from France Amiens University noted that converting combinatorial optimization problems to minimum satisfiability problems for solving is faster than converting them to maximum satisfiability problems. Moreover, the minimum satisfiability problem was be widely used in intelligent planning, scheduling, computer vision, hardware testing, bioinformatics and so on. So researching the minimum satisfiability problem problem is important in theoretical significance and practical applications.The algorithms for solving minimum satisfiability problems were divided into exact algorithms and heuristic algorithms. The exact algorithms can calculate the exact solutions and the heuristic algorithms may not be able to find the exact solutions, but it can find a better solution quickly. When the scale of a problem is big, the exact algorithms always cannot solve the problem in polynomial time, so there is a important application in solving the large-scale problems using heuristic algorithms. Currently, the main research of heuristic algorithms is the local search algorithm. The main work of this paper is to design some local search algorithms for solving minimum satisfiability problems.This paper presents four local search algorithms to solve the minimum satisfiability problems, they are basis local search algorithm, random walk local search algorithm, clause weighting local search algorithm and relaxed configure checking and clause weighting local search algorithm. The basis local search algorithm uses a greedy strategy, namely choosing the best variable to flip everytime. The random walk local search algorithm adopts the random walk strategy based on the greedy strategy, it reduced the cases that falling into local optima. The clause weighting local search algorithm uses the clause weighting strategy, it can find a better solution near the local optima though increasing the cost of the local optima. The relaxed configure checking and clause weighting local search algorithm adopts the relaxed configure checking strategy based on the clause weighting local search algorithm, the relaxed configure checking strategy can solve the circulation problems effectively in the process of searching.In this paper, there are three authoritative data sets in the experimental part, they are random data, RB model data and industrial data. We compared our algorithms with the solver of Min Satz which is a efficient solver currently based on the three data sets. The experimental results show that the relaxed configure checking and clause weighting local search algorithm is the most efficient algorithm for solving minimum satisfiability problems which are large-scale.