Disjoint Partial Enumeration without Blocking Clauses

기술 요약: 차단 절 없이 수행하는 불연속 부분 열거

문제 정의
All-Solution Satisfiability Problem(AllSAT) 은 명제 논리 공식에 대한 모든 만족 해를 찾는 것을 요구합니다. 지수적인 공간 복잡도로 인해 전체 할당의 명시적 열거는 종종 불가능하지만, 부분 모델 (implicants) 을 사용하면 해 집합을 간결하게 표현할 수 있습니다. 반복을 포함하는 열거와 불연속 열거 (disjoint AllSAT) 사이에는 중요한 차이가 존재하며, 여기서 각 전체 할당은 정확히 한 번만 커버되어야 합니다. 불연속 열거는 Weighted Model Integration 및 #SMT 와 같은 응용 분야에서 필수적입니다.

현재 불연속 AllSAT 에 대한 접근 방식은 일반적으로 두 가지 범주로 나뉩니다:

1. 차단 솔버 (Blocking Solvers): 이들은 비연속적 백트래킹 (NCB) 을 사용하는 충돌 기반 절 학습 (CDCL) 을 활용합니다. 모델을 찾은 후, 솔버가 동일한 할당을 다시 방문하지 못하도록 "차단 절 (blocking clauses)"을 추가합니다. 검색 공간을 가지치기하는 데 효과적이지만, 이 접근법은 모델 수가 증가함에 따라 차단 절의 수가 지수적으로 늘어나 단위 전파를 지연시키면서 메모리 소비와 성능 저하를 겪습니다.
2. 비차단 솔버 (Non-Blocking Solvers): 이들은 차단 절을 피하기 위해 연속적 백트래킹 (CB) 을 활용합니다. 그러나 전통적인 CB 기반 솔버는 종종 전체 할당만 생성하며, 학습된 충돌 절의 안내 없이 검색 공간의 비만족 영역에서 효율적으로 탈출하는 데 어려움을 겪습니다.

방법론
저자들은 차단 절 없이 불연속 부분 열거를 달성하기 위해 세 가지 핵심 기법을 통합한 TABULARALLSAT이라는 도구에 구현된 새로운 AllSAT 절차를 제안합니다:

1. 검색 가지치기를 위한 CDCL: 이 알고리즘은 표준 CDCL 을 사용하여 충돌 절을 학습하고, 만족하는 할당이 존재하지 않는 검색 분기를 탈출합니다. 이는 순수 CB 접근법의 일반적인 약점인 비만족 하위 트리에 솔버가 갇히는 것을 방지합니다.
2. 종료를 위한 연속적 백트래킹 (CB): NCB 를 사용하고 차단 절을 추가하는 대신, 솔버는 CB 를 사용합니다. 모델을 찾으면, 가장 최근에 할당된 결정 변수로 백트래킹하여 그 값을 반전시킵니다. 이 체계적인 탐색은 명시적인 차단 절 없이도 어떤 할당도 두 번 커버되지 않음을 보장합니다.
3. 연속적 함축자 축소 (Chronological Implicant Shrinking): 전체 모델뿐만 아니라 부분 모델을 생성하기 위해, 알고리즘은 사후에 전체 경로를 축소합니다.
   • 절의 만족에 대해 리터럴이 필요한지 효율적으로 확인하기 위해 2-Watched Literal Scheme을 활용합니다.
   • 축소 과정에서 watch 리스트 업데이트를 피하는 보수적이고 더 빠른 변형을 도입하여, 일부 최소화 깊이를 희생하더라도 상당한 속도 향상을 얻습니다.
   • **암시적 해 이유 (Implicit Solution Reasons)**를 사용합니다: 차단 절을 피하려는 목적을 무효화할 수 있는 메모리에 "백트래킹 이유 절"을 저장하는 대신, 솔버는 반전된 리터럴을 위한 특수 BACKTRUE 태그를 사용하여 충돌 분석 중에 이를 온더플라이 (on-the-fly) 로 재구성합니다.

주요 기여

• 새로운 알고리즘: 이 논문은 차단 절에 의존하지 않고 CDCL, 연속적 백트래킹, 그리고 함축자 축소를 결합한 최초의 실용적인 불연속 AllSAT 솔버 구현을 제시합니다.
• 이론적 기반: 이 작업은 Möhle 와 Biere(2019b) 가 제안한 형식적 계산을 기반으로 하여, 현대 SAT 솔버 데이터 구조에 맞게 적응시키고 (예: 전체 경로에서만 만족을 감지하는 솔버에서 부분 경로를 처리하는 문제 등) 실용적인 구현 격차를 해소합니다.
• 효율적인 데이터 구조: 암시적 백트래킹 이유와 보수적 리터럴 확인 변형의 도입으로 인해 솔버는 방대한 수의 모델을 열거할 때에도 높은 성능과 낮은 메모리 오버헤드를 유지할 수 있습니다.
• 결정 휴리스틱: 저자들은 부분 경로의 수를 최적화하기 위해 연속적 백트래킹에 맞춘 특정 변수 순서 휴리스틱 (VSADS, DLCS, VSIDS 기반) 을 제안합니다.

실험 결과
저자들은 TABULARALLSAT 을 차단 솔버 (BC, BC PARTIAL), 비차단 솔버 (NBC), BDD 기반 솔버 (BDD), 그리고 MathSAT5 를 포함한 최첨단 솔버들과 비교 평가했습니다. 벤치마크에는 제작된 이진 절 인스턴스, 무작위 3-SAT 인스턴스 (Rnd3sat), 그리고 SATLIB 벤치마크 (CBS, BMS) 가 포함되었습니다.

• 성능: TABULARALLSAT 은 1200 초 타임아웃 내에서 거의 모든 벤치마크에서 가장 많은 인스턴스를 해결했습니다. 전체 해결 인스턴스 수 측면에서 차단 솔버 (BC, MathSAT) 와 비차단 솔버 (NBC) 를 크게 능가했습니다.
• BDD 와의 비교: Rnd3sat 벤치마크 (낮은 절 대 변수 비율) 에서 BDD 기반 솔버가 TABULARALLSAT 보다 우수한 성능을 보였습니다. 저자들은 이러한 인스턴스의 구조적 단순성이 효율적인 BDD 컴파일을 가능하게 했기 때문이라고 설명합니다. 그러나 더 복잡한 벤치마크 (BMS, CBS) 에서는 TABULARALLSAT 이 우수한 성능을 입증했습니다.
• 축소 기법: 두 가지 함축자 축소 변형을 비교한 실험 결과, watch 리스트 기반 방법은 더 간결한 부분 할당을 생성하지만, "가벼운" 보수적 변형이 계산적으로 더 빠르며 특히 모델 수가 많을 때 전체 시간 효율성에 더 효과적이었습니다.

의의 및 주장
이 논문은 CDCL 과 연속적 백트래킹의 통합이 기존 불연속 AllSAT 접근법의 주요 단점을 효과적으로 완화한다고 주장합니다. 즉, 차단 절로 인한 메모리 및 전파 병목 현상을 피하면서도 동시에 비만족 검색 영역에 갇히는 비효율성을 동시에 방지합니다. 실험 결과는 이 하이브리드 접근 방식이, 특히 해가 많은 공식의 경우 불연속 부분 모델을 열거하기 위한 실현 가능하고 종종 더 우수한 대안임을 보여줍니다. 저자들은 겸손하게도 이 접근법이 매우 효과적이지만 모든 구조적 유형의 공식 (예: BDD 로 쉽게 컴파일되는 공식 등) 에 최적의 선택은 아닐 수 있으며, 향후 결정 휴리스틱 및 구성 요소 캐싱에 대한 연구가 필요하다고 언급합니다.