Parameterized Algorithm For Satisfiability Problem

Satisfiability Problem (short as SAT) is a fundamental problem and a hardness standard of so many NP-Complete problems, which can finally transformed into the settlement of SAT problem. Parameterized SAT problem has formed an important kind of NP hard problem, and there has been a remarkable line of research in the study of parameterized SAT problem. Recently, a fixed parameterized tractable (short as FPT) algorithm for parameterized Almost 2-SAT problem (short as 2-ASAT) has been proposed which has been open for several years.In this paper, a survey of algorithms for SAT problem and its constrained sub-problems is firstly presented to establish a comprehensive understanding of techniques used in relevant algorithms and the research situation. Techniques used in the FPT algorithm for parameterized 2-ASAT problem are iterative compression and branch. In this paper, we analyze the combination branches of consecutive clauses in a walk for a given 2-CNF formula F in order to refine the branch process, and propose a determined parameterized algorithm of running time O~*(5~k) for 2-ASLASAT problem, which is useful for the solvement of parameterized 2-ASAT problem.Parameterized vertex cover in graphs with perfect matching (short as VC-PM) is FPT-equivalent to parameterized 2-ASAT problem. We analyze the relation between the perfect matching and the vertex cover in the graph, transform the problem into searching for a vertex cover containing at most k matched pairs of vertices, and propose a determined parameterized algorithm. Furthermore, a polynomial time algorithm is proposed when k =0.Finally, this paper sums up the whole study work on parameterized 2-ASAT problem and parameterized VC-PM problem and discuss the further work on the problems.