Algorithmic analysis on a class of Boolean equations

摘要

Efficient procedures for satisfiability verification are foundations of numerical simulation and algorithmic analysis of NP-complete problems. Previous researches in this direction include well-known Davis-Putnam-Logemann-Loveland (DPLL) and leaf removal procedures. In this paper, we propose a new procedure called Leaf-removal Gaussian Elimination procedure (LGC) to verify the satisfiability of a class of NP-complete problems. This novel procedure is much simpler and faster than the original DPLL procedure. We also provide estimation of the phase transition point based on this procedure. Numerical experiments are conducted for Boolean equations systems with different parameters and the results verify the validity and efficiency of our novel techniques.