Solving SAT by Algorithm Transform of Wu's Method

作     者：贺思敏 张钹 

作者机构：Department of Computer Science and Technology National Key Laboratory of Intelligent Technology and Systems Tsinghua University Beijing P.R. China 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：1999年第14卷第5期

页      面：468-480页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金 

主　　题：algorithm design satisfiability problem Wu's method automated reasoning 

摘      要：Recently algorithms for solving propositional satisfiability problem,or SAT, have aroused great illterest, and more attention has been paid to trans-formation problem solving. The commonly used transformation is representationtransform, but since its ifltermediate computing procedure is a black box from theviewpoint of the original problem, this aPproach has many limitations. In this paper, a new approach called algorithm transform is proposed and applied to solvingSAT by Wu s method, a general algorithm for solving polynomial equations. By es-tablishing the correspondellce between the primitive operation in Wu s method andclause resolution in SAT, it is shown that Wu s method, when used for solving SAT,is primarily a restricted clause resolution procedure. While Wu s method illtroduceselltirely new concepts, e.g. characteristic set of clauses, to resolution procedure, thecomplexity result of resolution procedure suggests an exponential lower bound toWu s method for solving general polynomial equations. Moreover, this algorithmtransform can help achieve a more efficiellt imp1ementation of Wu s method since itcan avoid the complex manipulation of polynomials and can make the best use ofdomain specific knowledge.