An Efficient Algorithm for Solving the 2-MAXSAT Problem

기술 요약: 2-MAXSAT 문제를 해결하기 위한 효율적인 알고리즘

문제 정의
본 논문은 MAXSAT(Maximum Satisfiability) 문제의 제한된 버전인 2-MAXSAT 문제를 다룬다. $m$개의 불리언 변수 $V$와 $n$개의 절(clause)로 구성된 CNF(Conjunctive Normal Form) 집합 $C$가 주어졌을 때, 각 절은 최대 두 개의 리터럴을 포함하며, 목적은 만족되는 절의 수를 최대화하는 진릿값 할당을 찾는 것이다. 이 문제는 이러한 제한 조건 하에서도 NP-완전(NP-complete)임이 확립되어 있다.

방법론
제안된 알고리즘은 전통적인 분기 한정법(branch-and-bound)이나 근사법에서 벗어나, 문제를 DNF(Disjunctive Normal Form) 최대화 작업으로 변환하고 특화된 그래프 기반 탐색 구조를 활용한다. 방법론은 세 가지 주요 단계로 진행된다:

1. DNF로의 변환:
   알고리즘은 원래의 CNF 식 $C$로부터 새로운 DNF 식 $D$를 구성한다. $C$의 모든 절 $C_i = l_{i1} \lor l_{i2}$에 대하여, 알고리즘은 새로운 보조 변수 $x_i$를 도입하고 두 개의 논리곱(conjunction) $D_{i1} = l_{i1} \land x_i$와 $D_{i2} = l_{i2} \land \neg x_i$를 생성한다. 결과물인 식 $D$는 $2n$개의 논리곱으로 구성된다. 논문의 명제 1은 $C$가 적어도 $n^*$개의 만족되는 절을 가질 필요충분조건이 $V \cup \{x_1, \dots, x_n\}$에 대한 진릿값 할당 하에서 $D$가 적어도 $n^*$개의 만족되는 논리곱을 갖는 것임을 입증한다.

2. 그래프 표현 (p-그래프 및 트라이(Trie)):*
   $D$의 논리곱들을 만족시키는 진릿값 할당을 효율적으로 표현하기 위해, 본 논문은 p-그래프*를 도입한다.

• 변수 시퀀스: 각 논리곱은 변수의 전역 출현 빈도에 따라 정렬된 변수 시퀀스로 변환된다. 부정 리터럴은 변수 $c$가 참 또는 거짓이 될 수 있거나(또는 건너뛸 수 있는) 상태를 나타내는 특수 표기법 $(c, *)$를 도입하여 처리된다.
• p-그래프: 시퀀스 내의 변수들에 대응하는 노드를 갖는 단일 논리곱을 나타내는 유향 그래프이다. "스팬(Spans)"(변수를 건너뛰는 엣지)은 $(c, *)$ 옵션을 나타낸다.
• p-그래프:* p-그래프를 개선한 것으로, "중첩된 스팬"(연속적인 선택적 변수)을 이행 폐쇄(transitive closure)를 통해 병합한다. 이는 그래프가 특정 논리곱에 대한 모든 유효한 진릿값 할당을 정확하게 표현하도록 보장한다.
• 트라이 형태의 구조 ($G$): 모든 p*-그래프는 하나의 트라이 형태 그래프 $G$로 통합된다. 이 구조는 중복 검사를 피하기 위해 공통된 변수 시퀀스를 클러스터링한다. 그래프에는 경로가 갈라지는 "분기 노드(branching nodes)"가 포함된다.

3. 재귀적 바텀업 탐색:
   핵填 알고리즘인 SEARCH(G)는 그래프 $G$를 바텀업(후위 순회) 방식으로 탐색하여 만족 가능한 논리곱의 최대 부분 집합을 찾는다.

• 도달 가능한 부분 집합 (Reachable Subsets, RS): 분기 노드 $v$에 대하여, 알고리즘은 조상으로부터의 스팬을 통해 도달 가능한 노드들의 "도달 가능한 부분 집합"을 계산한다. 이 부분 집합들은 특정 변수들을 건너뜀으로써 동시에 만족될 수 있는 논리곱들의 그룹을 나타낸다.
• 상한 경계 (Upper Boundaries, upBounds): RS를 바탕으로, 알고리즘은 서브그래프의 병합을 허용하는 노드들의 집합인 "상한 경계"를 식별한다.
• 재귀적 구성: 분기 노드와 마주치면, 알고리즘은 상한 경계에 위치한 노드들을 루트로 하는 새로운 더 작은 트라이 형태의 서브그래프를 구성한다. 연결성을 유지하기 위해 가상 루트(원래의 분기 노드)가 추가된다. 알고리즘은 이 서브그래프들에 대해 SEARCH를 재귀적으로 호출한다.
• 최적화: 중복 계산을 방지하기 위해 알고리즘은 두 가지 개선 사항을 적용한다: (1) RS 계산을 현재 분기 노드와 가장 낮은 조상 분기 노드 사이의 구간으로 제한하는 것, (2) 해시 배열을 사용하여 이전에 방문한 서브그래프의 결과를 캐싱함으로써 반복적인 재귀 호출을 억제하는 것이다.

주요 기여

• 변환 기법: 2-MAXSAT 문제를 DNF에서의 최대 만족 논리곱 문제로의 다항 시간 환원으로 변환하였다.
• p-그래프 구조:* 선택적 변수를 포함하는 논리곱의 진릿값 할당을 정확하고 압축적으로 표현하기 위한 p*-그래프 및 그 이행 폐쇄의 정의.
• 재귀적 트라이 탐색: "도달 가능한 부분 집합"과 "상한 경계"를 활용하여 솔루션 공간을 효율적으로 병합하며, 트라이 형태의 그래프 구조를 동적으로 구축하고 탐색하는 새로운 재귀 알고리즘.
• 복잡도 분석: 제안된 알고리즘이 다항 시간 범위 내에서 작동함을 주장하는 상세한 분석 제공.

결과 및 복잡도
본 논문은 제안된 알고리즘의 최악의 경우 시간 복잡도가 $O(n^2 m^4)$로 제한된다고 단언한다. 여기서 $n$은 절의 수, $m$은 변수의 수이다.

• 초기 트라이 및 p*-그래프 구성에는 $O(nm^2)$이 소요된다.
• 재귀적 탐색은 최대 $O(nm)$개의 분기 노드를 포함한다.
• 각 분기 노드는 그래프 높이의 감소로 인해 최대 $O(m)$번의 재귀 호출에 참여한다.
• 호출당 서브그래프를 구성하는 비용은 $O(nm^2)$이다.
• 이러한 요소들을 결합하면 $O(n^2 m^4)$의 상한이 도출된다.

의의 및 주장
논문은 2-MAXSAT 문제가 NP-완전임이 알려져 있으므로, 이를 해결하는 다항 시간 알고리즘의 존재는 P = NP의 증명에 해당한다고 결론짓는다. 저자들은 이 결과가 P = NP의 증명을 제공하며, 만족 가능성 문제에 대한 계산 복잡도의 이해를 근본적으로 변화시킨다고 기술한다. 본 연구는 NSERF(캐나다)의 지원을 받은 컨퍼로스 논문의 수정 및 확장판으로 제시되었다.