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