기술 요약: 전처리 과정을 통한 d-DNNF 표현의 쿼리 효율성 향상

문제 정의

본 논문은 논리곱 표준형(CNF)으로 인코딩된 명제 공식(propositional formulas)을 쿼리할 때 발생하는 계산적 어려움을 다룹니다. 특히, 이 논문은 세 가지 근본적인 작업인 균등 샘플링(uniform sampling), 직접 모델 접근(direct model access) (사전식 순서에 따른 $k$-번째 모델 검색), 그리고 **모델 열거(model enumeration)**에 초점을 맞춥니다. 이러한 작업들은 종종 #P-완전( #P-complete) 문제를 포함하므로, 가공되지 않은 CNF 공식 상에서는 계산 비용이 매우 높습니다.

이를 완화하기 위해, 저자들은 CNF 공식을 d-DNNF(Deterministic Decomposable Negation Normal Form) 또는 decision-DNNF로 컴파일하기 전에 더 효율적인 표현으로 변환하는 **전처리 기법(preprocessing techniques)**의 사용을 조사합니다. 핵심 문제는 어떤 전처리 기법이 이러한 특정 쿼리들에 적합한지를 결정하는 것입니다. 저자들은 최신 전처리기들이 SAT 해결(SAT solving)이나 모델 카운팅에는 효과적일 수 있지만, 직접 접근이나 균등 샘플링과 같이 정확한 모델 수나 특정 모델 순서가 필요한 작업에는 부적합하도록 솔루션 공간(solution space)을 변경할 수 있다는 점에 주목합니다.

방법론

저자들은 CNF 공식이 먼저 전처리된 후, d4 컴파일러를 통해 decision-DNNF 표현으로 컴파일되고, 최종적으로 decdnnf_rs 도구를 사용하여 쿼리되는 파이프라인을 제안합니다. 본 연구는 전처리 전략을 그들이 보존하는 논리적 동치성(logical equivalence)의 유형에 따라 체계적으로 평가합니다:

1. 동치 보존 기법(Equivalence-Preserving Techniques): 여기에는 vivification, backbone identification, 그리고 occurrence reduction이 포함됩니다. 이러한 방법들은 전체 모델 집합을 보존하며($Mod(\Sigma_1) = Mod(\Sigma_2)$), 일반적으로 모든 쿼리 유형에 적용 가능합니다.
2. 만족 가능성 보존 기법(Satisfiability-Preserving Techniques): 변수 제거(variable elimination) 및 **차단 절 제거(blocked clause elimination)**와 같은 기법은 만족 가능성은 보존하지만 모델의 수는 보존하지 않습니다. 저자들은 (명제 1을 통해) 이러한 기법들이 원래의 모델을 검색하는 능력을 파괴하기 때문에 직접 접근, 균등 샘플링, 모델 열거에 부적합함을 증명합니다.
3. 모델 수 보존 기법(Model-Count-Preserving Techniques): 본 논문은 정의된 변수(defined variables)(다른 변수들에 의해 암시적 또는 명시적으로 기능적으로 결정되는 변수)의 제거에 집중합니다. 이러한 기법들은 모델의 수는 보존하지만, 모델 집합 자체는 변경합니다.
   • 이론적 기여: 저자들은 단순히 정의된 변수를 제거하는 것만으로는 **호환 가능한 평가 함수(compatible evaluation function, $f$)**와 **호환 가능한 순서(compatible order, $\tau$)**가 없다면 직접 접근이나 균등 샘플링을 수행하기에 불충분함을 입증합니다(명제 2).
   • 해결책: 저자들은 호환 가능한 평가 함수($f$)와 호환 가능한 순서($\tau$)의 개념을 도입합니다.
     • 호환 가능한 평가 함수는 남은 변수들을 기반으로 제거된 변수의 값을 계산합니다.
     • 호환 가능한 순서는 제거된 변수 $o$에 대해, $o$를 정의하는 모든 변수가 사전식 순서에서 더 앞선 위치에 오도록 보장합니다.
   • 명제 4는 호환 가능한 순서가 사용된다면, 전처리된 공식 $\Phi'$의 $k$-번째 모델을 평가 함수를 사용하여 원래 공식 $\Phi$의 $k$-번째 모델로 매핑할 수 있음을 확립합니다.

주요 기여

• 전처리 적합성에 대한 이론적 분석: 본 논문은 전처리 기법을 엄격하게 분류하여, 만족 가능성 보존 방식(예: 표준 변수 제거)이 직접 접근 및 균형 샘플링과 호환되지 않음을 증명함으로써 이론적 근거를 제공합니다.
• 모델 수 보존 조건: 저자들은 모델 수를 보존하는 전처리 방법(특히 정의된 변수 제거)이 다음 조건을 충족할 경우 이러한 작업에 사용될 수 있음을 확립합니다:
  1. 제거된 변수를 재구성하기 위한 호환 가능한 평가 함수가 유지되어야 함.
  2. 쿼리 과정 중 모델의 사전식 순서가 보존되도록 호환 가능한 변수 순서가 강제되어야 함.
• 쿼리 유형 간의 구별: 본 논문은 **전체 모델 열거(complete model enumeration)**와 부분 모델 열거(partial model enumeration) 사이의 중요한 차이점을 강조합니다. 정의된 변수를 제거하는 것은 전체 열거에는 도움이 되지만, 부분 모델의 수에서 지수적인 격차를 만들 수 있습니다. 이는 단순화된 공식의 압축된 표현이 필요한 부분 정보를 인코딩하지 못할 경우, 부분 열거를 비효율적으로 만들거나 불가능하게 만들 수 있습니다(예시 10).
• 의사 균등 샘플링(Pseudo-Uniform Sampling): 저자들은 선택 순서를 제로(control)함으로써 재현 가능한 샘플링을 가능하게 하는 시드(seed)를 포함하는 의사 균등 샘플러를 구축할 수 있음을 보여줍니다.

실험 결과

저자들은 1,425개의 벤치마크 인스턴스를 대상으로 네 가지 전처리 전략을 비교하는 광범위한 실험을 수행했습니다:

• no: 전처리 없음.
• equiv: 동치 보존 기법만 사용.
• #equiv-explicit: 동치 보존 + 명시적으로 정의된 변수 제거 (순서 제약 없음).
• #equiv-explicit-ordered: 동치 보존 + 명시적으로 정의된 변수 제거 + 강제된 호환 순서 적용.

주요 결과:

• 컴파일 효율성: #equiv-explicit-ordered 전략은 d4 컴파일러의 성능을 크게 향상시켜, 전처리를 하지 않은 베이스라인보다 47개의 인스턴스를 더 해결했습니다. 순서 제약이 없는 #equiv-explicit 전략은 이보다 더 많은 인스턴스(ordered 버전보다 8개 더 많음)를 해결했으나, 이는 엄격한 사전식 순서를 요구하지 않는 작업(표준 균등 샘플링 등)으로 제한됩니다.
• 쿼리 효율성:
  • 균등 샘플링: #equiv-explicit을 사용하면 equiv에 비해 최대 10배(an order of magnitude)의 속도 향상을 얻었습니다. 또한 메모리 사용량을 줄여 equiv 방식에서 메모리 타임아웃이 발생했던 인스턴스들을 해결했습니다.
  • 모델 열거: #equiv-explicit은 더 빠른 열거 시간을 제공했지만, 열거는 여전히 모든 모델을 생성해야 하므로 샘플링만큼의 뚜렷한 이득은 나타나지 않았습니다.
  • 직접 접근 / 시드를 이용한 샘플링: 이러한 작업을 위해서는 #equiv-explicit-ordered 전략이 필수적이었습니다. 이 전략은 타임아웃을 크게 감소시켰으며(equiv의 391회 대비 173회), 런타임 효율성을 개선하여, 호환 가능한 순서를 강제하는 것이 이러한 특정 쿼리에 대한 전처리의 이점을 상쇄하지 않음을 입증했습니다.

의의 및 주장

본 논문은 많은 표준 전처리 기법이 모델 기반 쿼리에 해로울 수 있지만, 필요한 정보(평가 함수 및 변수 순서)가 유지된다면 모델 수를 보존하는 전처리가 매우 효과적일 수 있음을 주장합니다.

저자들은 실용적인 트레이드오프를 강조합니다. 즉, 전처리 기법(특히 호환 순서가 적용된 정의된 변수 제거)을 신중하게 선택함으로써, 정답의 정확성을 희생하지 않고도 직접 접근, 균등 샘플링 및 모델 열거에서 상당한 성능 이득을 얻을 수 있습니다. 이 연구는 SAT 해결에 사용되는 전처리 전략과 확률적 및 열거적 작업을 위한 지식 컴파일(knowledge compilation)의 요구 사항 사이의 간극을 메웁니다.

본 논문은 향-후 연구에서 이러한 기법을 다른 고급 샘플링 방법에도 적용하고, 현재의 equivalence, AND, OR, XOR 게이트 중심의 연구를 넘어 다른 유형의 명시적 정의(예: NOR 및 NAND 게이트)를 조사할 것임을 언급하며 겸허하게 결론을 맺습니다.