SOLVING SATISFIABILITY PROBLEM BY WU'S METHOD (I)ALGORITHM TRANSFORM
He Si · Chinese Journal of Computers · 1998
in this paper, a new approach called algorithm transform is proposed and applied tosolving SAT by Wu's method, a general algorithm for solving polynomial equations. By establishingthe correspondence between the primitive operation in Wu's method and clause resolution in SAT, itis shown that Wu's method, when used for solving SAT, is primarily a restricted clause resolutionprocedure. While Wu's method introduces entirely new concepts, e. g. characteristic set of clauses,to resolution procedure, the complexity result of resolution procedure suggests an exponential lowerbound to Wu's method when solving general polynomial equations. Moreover, this algorithmtransform can help achieve a more efficient implementation of Wu's method since it can avoid the complexmanipulation of polynomials and can make the best use of domain specific experience.