최대-최대 빈도수 k-SAT 알고리즘 (k-SAT Problem Algorithm Based on Maximum-Maximum Frequency)

서지정보

· 발행기관 : 한국인터넷방송통신학회
· 수록지 정보 : 한국인터넷방송통신학회 논문지 / 23권 / 6호 / 125 ~ 132페이지
· 저자명 : 이상운

초록

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

영어초록

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.

참고자료

· 없음