Algorithm ZJXQF for SAT Problem Author:JIANG Yong-jiang Input : A “0” and “1” table of clauses Q. Output: A Truth Value. Function ZJXQF(Q) (1). If a variable has 2 k -1 “0” and “1” in a k -block ( k =1,2,3,…, j, j is a constant number) Thenreturn “false”; (2). If a variable has unique solution in a clause block Then delete the variable and the relative clauses in Q,call (1); (3). If a variable has unique solution in a relative section Then delete the variable and relative clauses in Q,call (2); (4). Final, set 0 (or 1) to a selected variable in the possible solutions table and delete the line by relative clauses; (5). By relative value and extend the solution, can get the result. This polynomial algorithm is a completed for solve any SAT problem. I have the program for test. If you want get it, I will give you the program and the Eliminate-Clause method paper. MyEmail: accsysuibe@uibe.edu.cn 2017/5/16
标签: ZJXQF
