Expansive Map-based Stochastic Algorithm For Solving Sat Problems

An expander graph is a sparse yet highly connected graph, in which every set of vertices has a relatively very large boundary. So to disconnect a large part of the graph, one has to sever many edges. For this very special property, expander graphs have been very useful in diverse areas, including maths, communication engineering, and computer science. In application computer science, they play important role in algorithm design, cryptography, error correcting codes, pseudo randomness, sorting networks, robust computer networks etc. In theoretical computer science, they are also used to prove many conclusions on computer complexity theory for they behave like random graphs in certain respects, particularly with regard to their role in reducing the dependence of probabilistic algorithms on uniformly random bits, which attracts more and more scientists.As we know that the satisfiable problem of propositional formulae is a famous problem in theoretical computer science and AI. A direct method for this problem is Exhaustive Attack method, which is feasible in theory but not practical for the runtime will soon become very large. Other algorithms such as DPLL algorithm and Local Search algorithm have their own advantages and defections. So to design high performance and practical SAT algorithms have been focus in computer science.In this paper, the theory of expander graphs is analyzed thoroughly. And a new SAT algorithm based on the expander graphs is proposed. Firstly, the basic conceptions and properties are introduced from the combinatorial viewpoint. Secondly, we investigate the construction of expander graphs from the algebraic viewpoint. Here we present matrix product, Kronecker product, and replacement product and construct expander graphs based on these three kinds of product. Thirdly, we study expander graphs' random walk from the probabilistic viewpoint. Here we introduce expander mixing lemma and probabilistic estimate of random walk. Furthermore, we make use of expander graphs to design random algorithms. Finally, we introduce the SAT problem and the kinds of randomized algorithms and SAT algorithms, and propose new randomized SAT algorithms whose random walk is induced by expander graphs.