Research On Key Issues Of Boolean SAT Problem

The propositional satisfiability problem (SAT problem) is the first provedNon-Deterministic Polynomial (NP) problem. More important, SAT problem is also animportant issue in many areas of computer science, including the basic theory ofcomputer science, artificial intelligence, mathematical logic, etc. In2003and2007,Artificial Intelligence Conference proposed ten challenging issues of SAT problem, andin2001and2007, stated a complete summary of the SAT problem’s current situation.These challenging issues have played a strong role in promoting the theoretical studiesand improving of SAT problem. The current SAT problem is mainly used in electronicdesign automation; in the meantime, many real practical problems can be transformedinto SAT problems. Many researchers have also invested in SAT efficient algorithmresearches, mainly consisting of two parts: complete algorithms and incompletealgorithms. Complete SAT algorithms are mainly based onDavis–Putnam–Logemann–Loveland (DPLL), which can prove that propositionalformula is solvable, but the efficiency of algorithms is relatively low; and incompleteSAT algorithms mainly based on local search, which can quickly find solutions, butcannot prove that propositional formula is solvable. With the development of SATproblem, some branches problems have been proposed: Maximum Satisfiabilityproblem, Quantified Boolean Formula, and Satisfiability Module Theory.In the SAT problem, backbones are those variables with constant values in allsatisfiable assignments, which the scale of has a close relationship with the search sizeof SAT problem. This feature can be used to reduce the complexity of some problems,so backbones in some SAT questions can make some optimizations, such as faultdiagnosis, random3-SAT problem, and probabilistic message-passing algorithms.Because of these advantages, some algorithms of computing backbones areproposed, and mainly based on iterative-based, block-based, unsatisfiable core-based.And the combination of these ideas is used to form some hybrid algorithms to computebackbones.In this paper, some improved variable selection strategies are applied to theiterative-based backbone algorithms. Firstly, this paper uses the concept of level in theDPLL-based of SAT complete algorithm as variable selection strategy to compute backbones. The new algorithm uses the information of level to dynamically select thevariable to compute backbone and can improve the efficiency of computing backbones:decreasing the satisfying search-space by continuously removing non-backbones; andreducing the solving scale of computing backbone earlier by confirming backbones asearly as possible. This paper then reviews a neighbor strategy in the SAT incompletealgorithms. A new algorithm is based on the idea of this neighbor strategy to selectvariables for computing backbones, which can reduce the complexity of formula byearly finding backbones. Experimental results show that two new variable selectionstrategies can improve the performance of previous algorithm, and between twostrategies the new algorithm based on the neighbor strategy showed better performance.