The Continue Solution Of SAT With Algebraic Geometry

Boolean satisfiability problem, known as SAT, is one of the basic theoretical problems of computer science, which has been studied in long time and widely applied in the verification and testing of discrete event systems, software validation,debugging, and many other regions. We study the algebraic geometry method to solve a SAT problem, e.g., expressing a concrete SAT problem by the functions of continuous mathematics, say polynomial equations, and then try to decide its solution, then the solution of a SAT problem is concluded as a well-studied ZERO existence problem. We proposed two ways of continuous model of SAT, e.g.,physical and geometry model. In terms of these two models, we adopt two way to compute ZEROs, e.g., Gr(?)bner Base and Triangle Set. Then we proposed a complete and realized framework for solving SAT problem continuously. We also show a case-study to illustrate our solution.In addition to solve some practical problems, due to the limited of CNF formula expression in SAT Problem, we often need to express them with first-order logic formulas which expressed stronger. In this paper we have studied Satisfiability Modelo Theories of polynomials in real fields with algebraic geometry, the main idea is that it is equivalent to the polynomial equations contained quantifier of polynomial theoretical model in real fields transformed into a polynomial formula without quantifier by quantifier elimination, so the original model is became a formula which refuses quantifiers. Since each clause be a polynomial equation, finding out the assignment model is equivalent to solve the solution of the equations generated from Clauses, finally the decision problem is transformed into computation problem, and then the solvable equations reflect the satisfied original one; otherwise, the original model is unsatisfied.In this paper, we studied the way of modeling and solving of a satisfiability problem with algebraic geometry, and we studied Satisfiability Modelo Theories of polynomials in real fields, both of which are brand new ideas and methods for satisfiability problem, we demonstrate the feasibility and accuracy of these methods through some examples also.