Research On Boolean Satisfiability Algorithms

Boolean satisfiability(SAT) which is a famous category of NP-complete problem is a cross discipline problem. Due to the consistent improvement of the performance of SAT solving algorithms, they have been widely applied in solving practical problems such as combinational equivalence checking, Automatic Test Pattern Generation(ATPG), software model checking, Satisfiability Modulo Theories(SMT), computational biology and automatic planning. Many algorithms have been designed and optimized according to their own application with the hope to solving problems in a fast and robust manner. However, there are still some problems which solving algorithms are complicated. Both time complexity and space complexity of these algorithms are needed to be optimized. Thus a high efficient solving algorithm for a specific problem is one of the hot topics in computer science and AI areas.This dissertation proposes a few modeling methods and algorithms for specific problems based on SAT algorithms. It can be divided into four parts showing as follows.Aiming at characteristics of Model RB, the satisfiability problem of Model RB structure is modeled and described with set and graph structure. It is solved by algorithms incorporating advantages of both complete SAT algorithm and local search algorithm. By referring to searching procedure of complete SAT algorithm, a new searching and decision-making algorithm is proposed based on mutual exclusive set and relative set. During searching process, this algorithm can dynamically generate searching tree of sub clauses set, choose decision variable and determine backtrack mechanism. In order to achieve fast conflict backtracking, this algorithm exploits local search algorithm to get maximum clique whose nodes are used to construct initial searching tree. Experiment shows that this algorithm shows good performance in Model RB and graph coloring problems.With the more and more in-depth understanding of gene and improved technology in extract gene sequence, research on gene for computational biology has been converted from characteristic of single gene to dynamic characteristic of genetic regulatory networks. One of the most important topic in genetic regulatory networks is how to solve attractors. An attractor represents a stable status of a genetic regulatory network, one attractor also represents a cell type. Based on synchronous Boolean network modeling method, a new algorithm is proposed to transform the dynamic process of genetic regulatory network to a state transition graph of synchronous Boolean network, Boolean network is divided into blocks based on its strongly connected components, each block forms directional acyclic relationship. This algorithm calculates the global network attractor by calculating all local attractors and then do integration. While calculating attractors in a block, this algorithm converts this problem into SAT problem by expanding Boolean network transition function. Experiment shows that attractor finding algorithm based on SAT algorithm achieves remarkable advantage over complex genetic regulatory network problem.Parallel computing has become a naturally software design trend recently for full exploiting modern computers’ processing ability to achieve high efficient problem solving. Based on in-depth research on parallel SAT algorithm and benefit of partition algorithm, two parallel algorithms for solving attractors are proposed, one is based on partitioned block and the other is based on local attractors. The first algorithm is based on partitioned block to achieve SAT solving, the other algorithm solves the problem by message mechanism to achieve load balancing. Block based algorithm will equally distribute local attractors to all the CPU cores to continue calculation after calculating first block’s local attractor while the other one will find out idle CPU and notify them to continue calculation after the first calculation process. Experimental result shows that parallel algorithm shows better performance than single thread algorithm and local attractor based algorithm performs better than block based algorithm.Calculating Boolean network stable status is a NP-complete problem, a lot of real problem cannot obtain all the stable status in tolerable time limit. To make initial analysis of this kind of problem, a new calculation algorithm is proposed for calculating the stable status in which the length of cycle is less than or equal to the specific length. This algorithm modeled the problem based on bounded model checking and optimized ALL-solution SAT algorithm based on variable categorization and block clause generation based on implication graph. Experiment shows that this algorithm shows lower complexity on the instances in which distribution of length of cycles is uniform. This algorithm shows some values on complex network in which all cycles cannot be solved in limited time.