Propositional Logic Satisfiability Problem: Complexity And Algorithms

The satisfiablity (SAT) problem plays an important role in artificialintelligence, machine learning, mathematical logic, VLSI design and detection and other areas. It lies at the very heart of a family of NP-Complete problems, and is important to both computer science and practical applications. Its importance and interesting character attracts us to do research on it.We procede from two aspects, one about the problem's intrinsic features and the other about efficient algorithms. It should be stressed that research on the two aspects are connected tightly, and shed light on each other. From the aspect of the intrinsic features, we studied the phase transition and the hardness of a problem, which helps to deeply understand the problem and to divide the problems into more precise categories. From the aspect of the efficient algorithms, we analyzed the faults and advantages of complete and incomplete algorithms, and proposed an idea that both categories should be combined to speed up the algorithms.Our works are listed below. We use the flag "P" to represent works on problem's feature, and "A" to represent works on algorithms.1.(P) A regression method is used to model the curve of the phase transition of random 3-SAT problem. This follows the result of the paper "An Empirical Study on the Location of 'Really' Hard 3-SAT Instances ", which was published in the AAAI-94 Workshop "Experimental Evaluation of Reasoning and Search Methods". Using the approach, we got two parameters Alpha and Beta. Alpha represents the probability that a randomly produced clause holds according to the truth assignment produced randomly, while Beta represents how many values a variable can be assigned on average. Under such a model, the phase transition point is not really in the point that the probability of the CNF(Conjunction Normal Formula) holds equals 0.5, but (1-1/e), about 0.63 instead.2.(A) A local search algorithm is utilized to obtain the global information of the CNF, which can guide how to select the branch variable. In more details, we...