To NP-complete 3-SAT problem, this paper proposes a polynomial time algorithm, where is the number of literals and is the total frequency of all literals in equation . Conventionally well-known DPLLs should perform in the worst case by performing back...
To NP-complete 3-SAT problem, this paper proposes a polynomial time algorithm, where is the number of literals and is the total frequency of all literals in equation . Conventionally well-known DPLLs should perform in the worst case by performing backtracking if they fail to find a solution in a brute-force search of a branch-and-bound for the number of literals . DPLL forms the core of the SAT Solver by substituting true(T) or false(F) for a literal so that a clause containing the least frequency literal is true(T) and removing a clause containing that literal. Contrary to DPLL, the proposed algorithm selects a literal with the maximum frequency and sets . It then deletes clause in addition to from clause. Its test results on various -SAT problems not only show that it performs less than existing DPLL algorithm, but prove its simplicity in satisfiability verification.