earticle

영어

To NP-complete 3-SAT problem, this paper proposes a O(nm) polynomial time algorithm, where n is the number of literals and m is the total frequency of all literals in equation f. Conventionally well-known DPLLs should perform O(2 l) 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 l. 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 max l with the maximum frequency and sets max   = 1. It then deletes l∈c i clause in addition to l from l∈c i clause. Its test results on various k-SAT problems not only show that it performs less than existing DPLL algorithm, but prove its simplicity in satisfiability verification.

한국어

본 논문은 NP-완전으로 알려진 k-SAT 문제의 절의 수 m에 대해 O(km)의 다항시간 알고리즘을 제안하였다. 기존에 널리 알려진 DPLL은 문자 수 l에 대해 분기한정법의 전수탐색으로 해를 찾지 못하면 역추적을 수행하는 방식으로 최악의 경우 O(2 l)  을 수행해야 한다. DPLL은 최소 빈도수 문자가 포함된 절을 참(T)으로 하도록 문자에 참(T) 또는 거짓(F)을 대입하여 해당 문자가 포함된 절을 제거하는 방식으로 SAT Solver의 근간을 이루고 있다. 제안된 알고리즘은 DPLL과는 반대로 부울 수식 f에 존재하는 최대 빈도수 문자 max l을 선택하고, max   = 1로 설정하고, l∈c i 절은 삭제하며, l∈c i절에서 l 를 삭제하는 방법을 적용하였다. 제안된 알고리즘을 다양한 k-SAT 문제들에 적용한 결과 기존 의 DPLL 알고리즘보다 적은 횟수를 수행함을 알 수 있었다.