Research And Analysis Of Satisfiability Problem's Preprocessing Strategy

Satisfiability problem is the first proven classic NP problem. People have been working on how to solve the SAT problem in a limited time. Along with the size of SAT problem in real world grows, preprocessing technologies have get more and more attention. Because of its good effect of simplification, variable elimination algorithm has been applied to a variety of the preprocessor. As a lightweight preprocessing technology, its simplification effect is associated with the process of its elimination constraints directly.In order to improve the performance of variable elimination algorithm, this paper compares and studies variable elimination algorithm' performance of simplification and the influence of solution under different constraint conditions, and designs a variable elimination algorithm based on dynamic constraint of clause's literal length. It only allows performing variable elimination' operation when the length of clauses' literal after resolved is less than original one's. In order to reduce variable elimination algorithm' worthless computing, it introduces dynamic constraint mechanism, this mechanism greatly reduces the preprocessing time and improves further performance' simplification. Depend on this, this paper achieves a preprocessor based on MiniSat' open source for SAT problems- Mini Sat BFS. In addition to compare the performance of conventional analysis by two different constraints variable elimination preprocessing algorithm performance. Using statistical analysis method of complex networks, we will transform CNF into complex network. From both global and local dimensions of complex networks, we analyze the CNF instance simplified before and after pretreatment, and assess the performance of preprocessing algorithms.The final experimental results show that, compared with the existing algorithms based on constraint of clause number, the new algorithm not only reduces the size of the CNF instance, but also shortens the time of the pretreatment process and the solution process. More importantly, the improved algorithm can within a limited time solve more problems and has a significant performance advantage.