Research And Implementation Of Applying Linear Algebra To Solve Satisfiability Problem

Satisfiability(SAT) problems is not only the first NP problem which has beenproved, but also has been the core problem of research on computational theory.The quick solver to it is very important both in theory and in practice.Satisfiabilityproblem solving algorithm is widely used in various fields of production and life,such as the artificial intelligence design, computer-aided design,formal verifica-tion of circuit and so on. So, look for efficient algorithms to solve satisfiabilityproblem is significant.At present, Efficient algorithm to solve satisfiability prob-lem mainly there are two kinds of algorithms, including the complete algorithmand the incomplete algorithm. The former is mainly based on branch backtrack-ing strategy, its typical representative is Martin Davis, Hilary Putnam, GeorgeLogemann and Donald W. Loveland proposes(DPLL algorithm)in1962. Now themost popular complete algorithm present new rules to simple propositional for-mula, or chose branches further. But the time complexity of the algorithm is alsoin the level of exponent. The incomplete algorithm is primarily a local search al-gorithm based on stochastic search strategy. Although the two algorithms havemade great progress, but there is insufficient, the former efficiency is low, thelatter can not find the corresponding solution for satisfiability problem.A new idea is proposed in this paper for solving the SAT problem, solvingthe SAT problem can be converted to linear algebra, and then using the simplexmethod to solve the model of SAT problem. The main research works are de-scribed as follows:(i)Converting clauses of the satisfiability problem to matrix, based on thematrix transformation, found and proved the internal relations between the co-efficient matrix of clause set and the satisfiability problem. Through finding theright coefficient matrix, we can solve a clause set can find the assignment. (ii)After find a right matrix of the satisfiability problem, We design and im-plement a sat solver base on simplex method, and test performance use the exam-ples of SAT competition. At last,we analyzes the factors affecting the efficiency ofthe solver.In this paper, we designing and implementing the SAT solver based on linearalgebra, showed the ability of linear programming for solving the SAT problem,provides a new thought to study the satisfiability problem.