기술 요약: 차단 절을 사용하지 않는 SAT 및 SMT 를 위한 불연속 투영 열거

문제 정의

본 논문은 모든 해 만족성 (AllSAT) 및 그 확장인 이론 하의 모든 해 만족성 (AllSMT) 에 내재된 계산적 과제를 다룹니다. 목표는 공식의 모든 만족하는 할당을 열거하는 것입니다. 전통적인 SAT 해결사는 단일 해를 찾으면 종료되지만, 열거는 전체 탐색 공간을 탐색해야 합니다.

주요 어려움 두 가지가 식별되었습니다:

1. 지수적 탐색 공간: $n$개의 변수를 가진 공식의 경우, 가능한 전체 할당은 $2^n$개입니다. $n$이 크면 명시적 열거는 불가능합니다. 본 논문은 전체 할당 집합을 나타내기 위해 부분 할당 (implicants) 을 사용하여 해 공간을 압축할 것을 주장합니다.
2. 차단 절과 메모리: 충돌 기반 절 학습 (CDCL) 및 비연속적 백트래킹 (NCB) 기반의 전통적인 AllSAT 해결사들은 동일한 모델을 재발견하지 않도록 차단 절을 추가하는 데 의존합니다. 모델의 수가 증가함에 따라 차단 절의 수도 지수적으로 증가할 수 있어 메모리 폭주와 단위 전파 성능 저하를 초래합니다.
3. 투영: 많은 응용 분야 (예: Tseitin 변환을 통한 비-CNF 공식 변환) 에서는 "중요한" 변수 집합 ($V_r$) 에 대한 해만 열거하고 보조 "무관한" 변수 ($V_i$) 는 무시해야 합니다.

본 논문은 불연속 열거에 초점을 맞추는데, 이는 확률적 추론 및 가중치 모델 통합 (WMI) 과 같은 응용 분야에서 필수적인 요구 사항인 반복 할당을 엄격히 금지하는 것입니다.

방법론

저자들은 TabularAllSAT(명제 논리용) 와 TabularAllSMT(SMT 용) 라는 두 가지 새로운 해결사를 제안합니다. 두 해결사 모두 차단 절의 필요성을 제거하면서도 불연속성을 유지하기 위해 CDCL과 연속적 백트래킹 (CB) 을 통합합니다.

1. 핵심 탐색 알고리즘 (CDCL + CB)

탐색 루프는 충돌 분석을 통해 비만족 영역을 탈출하는 CDCL 의 강점과 중복 차단 절 없이 체계적인 탐색을 가능하게 하는 CB 의 강점을 결합합니다.

• 충돌 처리: 충돌이 감지되면 해결사는 충돌 절을 유도하기 위해 표준 충돌 분석을 수행합니다. 그러나 표준 CDCL 과 같이 충돌 절의 수준으로 비연속적으로 점프하는 대신, 해결사는 연속적으로 백트래킹하여 가장 최근에 할당된 결정 리터럴로 이동하고 그 값을 반전시킵니다.
• 암시적 차단: 명시적 차단 절을 저장하지 않고 불연속성을 보장하기 위해, 해결사는 가상 백트래킹 이유 절을 활용합니다. 모델이 발견되고 결정 리터럴이 반전될 때, 그 반전의 이유가 Backtrue로 기록됩니다. 이는 그 시점까지의 모든 결정 리터럴의 부정을 포함하는 차단 절을 암시적으로 정의합니다.
• 종료: 해결사가 결정 수준 0 으로 백트래킹할 때 탐색이 종료되며, 이는 전체 공간이 반복 없이 체계적으로 스캔되었음을 보장합니다.

2. 연속적 함의 축소

핵심 구성 요소는 전체 할당을 컴팩트한 부분 할당 (함의) 으로 축소하는 것입니다. 본 논문은 두 가지 알고리즘을 소개합니다:

• 보수적 축소 (기준): 2-감시 리터럴에 기반한 이 알고리즘은 현재 부분 할당이 공식을 만족시키기 위해 리터럴이 필요한지 확인합니다. 불연속성을 보장하기 위해 결정 순서와 Backtrue 플래그를 존중합니다.
• 공격적 축소 (신규): 이 알고리즘은 최적의 결정 순서를 시뮬레이션합니다. 특정 절을 만족하는 데 필요한 "필수" 리터럴과 "불필요" 리터럴을 식별합니다. 충돌 분석에 관여하거나 Backtrue 로 표시되지 않는 한, 불필요한 리터럴의 결정 수준과 관계없이 이를 제거할 수 있습니다. 이는 다음을 통해 달성됩니다:
  1. 각 절에서 현재 트레일 (trail) 에 포함된 리터럴의 수를 세는 것.
  2. 어떤 절의 유일한 만족자가 아닌 리터럴을 반복적으로 제거하는 것.
  3. 필수 리터럴만으로 트레일을 재구성하여 불필요한 변수의 할당을 탐색 루프의 끝으로 미루는 것.

3. 투영 및 SMT 로의 확장

• 투영 열거: 알고리즘은 관련 변수의 부분 집합 ($V_r$) 을 처리하도록 적응됩니다. 결정 휴리스틱은 무관한 변수 ($V_i$) 보다 $V_r$을 우선시합니다. 함의 축소 과정에서 $V_i$에 해당하는 리터럴은 자동으로 폐기되어, 출력에 $V_r$에 대한 할당만 포함되도록 보장합니다.
• AllSMT 통합: 프레임워크는 이론 해결사 (MathSAT5) 를 통합합니다. 단위 전파 후 T-일관성 검사가 탐색 루프에 포함됩니다. 이론 충돌이 발생하면 Boolean 충돌과 유사하게 분석되며, 해결사는 연속적으로 백트래킹합니다. 해결 과정에서 생성된 이론 원자 (atoms) 는 투영 목적으로 무관한 변수로 간주됩니다.

주요 기여

본 논문은 다섯 가지 주요 기여를 제시합니다:

1. 불연속 부분 열거: 차단 절을 도입하지 않고 불연속 부분 모델을 열거하기 위해 CDCL 과 연속적 백트래킹을 결합한 절차.
2. 함의 축소 알고리즘: 기본 계산의 불연속성 제약을 엄격히 준수하면서 부분 할당을 최소화하도록 설계된 두 가지 알고리즘 (보수적 및 공격적).
3. 투영 열거 확장: CNF 변환 중 생성된 보조 변수를 처리하여 중요한 변수의 부분 집합만 열거하도록 해결사를 적응시킨 것.
4. SMT 확장: 이론 추론을 열거 프레임워크에 통합하여 불연속 부분 열거를 통한 AllSMT 해결 가능.
5. 실험적 평가: 최신 해결사들에 대한 포괄적인 벤치마킹.

실험 결과

저자들은 MathSAT5, Dualiza, BDD 기반 해결사, D4+ModelGraph 등 다양한 해결사와 비교하여 TabularAllSAT 및 TabularAllSMT 를 다양한 벤치마크 (랜덤 3-SAT, SATLIB, 합성 SMT, 비-CNF 공식) 에서 평가했습니다.

• 함의 축소: 새로운 공격적 축소 알고리즘은 보수적 기준선에 비해 생성된 부분 할당의 수를 크게 줄였으며, 특히 총 해가 많은 인스턴스에서 두드러졌습니다. 매우 작은 인스턴스에서는 약간의 오버헤드가 발생했지만, 더 큰 문제에서는 전체 실행 시간을 단축시켰습니다.
• AllSAT 성능: TabularAllSAT 는 대부분의 해결사 (BC, NBC, MathSAT5) 와 경쟁하거나 더 나은 성능을 보였습니다. 컴파일 오버헤드가 낮은 절이 적은 특정 벤치마크에서는 지식 컴파일 도구 (BDD, D4+ModelGraph) 에 비해 성능이 떨어지기도 했습니다. 그러나 TabularAllSAT 는 더 낮은 메모리 점유율을 보였으며 메모리 고갈로 인한 시간 초과를 경험하지 않았습니다.
• 투영 AllSAT: 투영이 필요한 비-CNF 벤치마크에서 TabularAllSAT 는 속도와 해결된 인스턴스 수 측면에서 MathSAT5 와 Dualiza 를 크게 능가했습니다. 또한 더 어려운 합성 벤치마크에서는 D4+ModelGraph 를 능가했습니다.
• AllSMT 성능: TabularAllSMT 는 총 열거 및 부분 열거 작업에서 MathSAT5(공식적으로 이용 가능한 유일한 투영 AllSMT 해결사) 를 능가했습니다. TabularAllSMT 에 차단 절이 없기 때문에 문제 복잡도가 증가함에 따라 MathSAT5 에서 관찰되었던 성능 저하가 발생하지 않았습니다.

중요성 및 주장

본 논문은 제안된 접근 방식이 전통적인 차단 절 기반 열거에 대한 우월한 대안을 제공한다고 주장하며, 특히 투영과 SMT 추론이 필요한 시나리오에서 그렇습니다.

• 효율성: 차단 절의 지수적 증가를 피함으로써 해결사는 안정적인 단위 전파 성능을 유지하고 메모리 폭주를 방지합니다.
• 컴팩트성: 공격적 함의 축소 알고리즘은 더 컴팩트한 부분 할당을 생성하여 출력 크기와 후속 열거 단계의 탐색 공간을 줄입니다.
• 일반성: 프레임워크는 명제 논리와 이론 기반 열거 모두에 대해 CDCL 과 연속적 백트래킹을 성공적으로 통합하여, 불연속 열거의 적용 범위를 1 차 이론에 대한 확률적 추론 및 모델 카운팅과 같은 복잡한 영역으로 확장합니다.

저자들은 자신의 작업을 [17] 에서 제시된 형식적 계산의 실용적 구현으로 위치시키며, 차단 절의 오버헤드 없이 투영과 SMT 를 효과적으로 처리하는 첫 번째 구현을 제공한다고 주장합니다.