The Research About New Decision Method For Boolean Satisfiability

Boolean satisfiability(SAT)problem is whether there exists a set of assignments to the boolean variables X,such that the CNF formula constructed by X is true.SAT problem is the first proven NP-complete problem,and plays an important role in compu-tational theory.If a complete and polynomial algorithm can be found for SAT problem,then P=NP;otherwise,if it can be confirmed that the lower bound of the worst-case time complexity of all the SAT algorithms is exponential,then P?NP.In addi-tion,SAT problem has great practical significance in circuit verification,combinatorial optimization,automated reasoning,etc.The algorithms for SAT can be divided into two classes:complete and incomplete algorithms.Complete algorithms can always find an satisfying assignment,or prove the unsatisfiability of the formula.Currently,the DPLL-based search algorithms are a mainstream type of complete algorithms.These algorithms systematically search the space of assignments with backtracking.Among various improvements for the DPLL algorithm,the CDCL algorithm greatly reduces the times of backtracking using clause learning and non-chronological backtracking.The worst-case time complexity of the known complete algorithms for SAT are exponential.And incomplete algorithms im-prove the efficiency for the SAT problems in practice.The local search algorithms widely use the probabilistic and greedy strategy and search the partial space of assign-ments to improve the search efficiency.The optimization-based methods transform SAT problem into optimization problems,then solve them by Lagrangian method,Newton method,etc.In addition,inspired by statistical physics,some researchers propose sur-vey propagation based on message passing.When incomplete algorithms can not find a satisfying assignment,whether the formula is satisfiable can not be decided.In order to further study SAT,some researchers turn their attention to some special SAT problems,such as 1-in-3-SAT.The 1-in-3-SAT is also NP-complete because 1-in-3-SAT and 3-SAT can be transformed into each other in polynomial time.Recently,a method named LAF can be used to prove the unsatisfiability of some 1-in-3 instances.However,the LAF algorithm is to be improved for the 1-in-3 satisfiable instances.Based on LAF,this paper proposes a pruning search method to search 1-in-3 satisfying assignment.The experiment shows that the search method can determine the 1-in-3 satisfiability for most of the instances within 160 variables.When the number of variables increases,the efficiency of pruning search declines.This is because the computational complexity of 1-in-3-SAT depends on the number of the variables and clauses in the formula.How to reduce the 1-in-3 formula to one with less variables or clauses is the key to improve the efficiency of solving 1-in-3-SAT.Based on a new type of normal form-XCNF,this paper proposes a new algebraic logic reduction method to reduce the number of 1-in-3 formula in polynomial time.After reduction,the reduced formula has the same 1-in-3 satisfiability with the original one.