기술 요약: 배제 방정식의 논리합으로 확장된 CDCL

문제 제기

충격 주도 절 학습 (CDCL) 은 SAT 해결을 위한 지배적인 방법이지만, 근본적으로 배제 증명 시스템에 의해 제한받습니다. 배제에서 지수적인 증명 크기를 요구하는 문제들 (예: Tseitin 공식이나 일대일 비둘기집 원리) 은 CDCL 에 대해 증명적으로 어렵습니다. 일부 해결사들은 절단 평면을 사용하는 의사-부울 해결사나 배제 방정식을 처리하는 CNF-XOR 해결사와 같은 더 강력한 증명 시스템의 일부 조각을 통합하지만, 이러한 접근 방식들은 종종 배제 추론을 별도의 모듈로 취급하거나 특정 정규형 (예: CNF-XOR) 에만 국한합니다.

이 연구가 다루는 구체적인 간극은 XNF(XOR-OR-AND 정규형) 공식을 본질적으로 처리하는 CDCL 스타일 알고리즘의 부재입니다. XNF 공식은 선형 절들의 논리곱으로 구성되며, 선형 절은 배제 방정식들의 논리합입니다 (예: $(x \oplus y) \lor \neg(y \oplus z)$). Res(⊕) 증명 시스템 (XNF 로 일반화된 배제) 은 특정 문제들에 대해 배제보다 지수적으로 강력하다는 것이 알려져 있지만, 기존 해결사들은 Res(⊕) 추론을 CDCL 루프에 완전히 통합하지도 않으며, CDCL 스타일 알고리즘이 Res(⊕) 를 다항식적으로 시뮬레이션할 수 있다는 이론적 증명을 제공하지도 않습니다.

방법론

저자들은 XNF 공식에서 직접 작동하도록 설계된 CDCL 알고리즘의 일반화인 **CDCL(⊕)**을 제안합니다. 방법론은 세 가지 핵심 구성 요소에 의존합니다:

1. Res(⊕) 를 위한 새로운 추론 규칙:
   저자들은 표준 배제 및 약화 규칙을 덧셈 및 기저 변경으로 대체하는 Res(⊕) 증명 시스템의 새로운 특징을 제시합니다.

   • 덧셈: $C \lor f$와 $D \lor g$로부터 $C \lor D \lor (f + g)$를 추론합니다.
   • 기저 변경: $C$로부터 $C \equiv D$ (의미론적으로 동등) 인 임의의 $D$를 추론합니다.
     결정적으로, 저자들은 방정식들이 (기저 변경을 통해) '분리'되어 덧셈을 통한 상쇄가 가능하도록 하는 아핀 배제 규칙을 정의합니다. 이는 약화 규칙과 관련된 지수적인 탐색 공간의 필요성을 제거하여 다항식 시뮬레이션을 가능하게 합니다.

2. 선형 대수를 통한 단위 전파:
   문자 할당을 기반으로 전파하는 고전적 CDCL 과 달리, CDCL(⊕) 은 $\mathbb{F}_2$ 위의 선형 대수를 사용하여 단위 전파를 수행합니다.

   • 해결사는 알려진 단위 (방정식) 집합 $U$를 유지합니다.
   • 전파는 주어진 $U$에 대해 선형 절 $C$가 새로운 방정식 $f$나 모순 ($1$) 을 함의하는지 확인합니다.
   • 이는 절의 '선형 부정' (절이 거짓이 되는 할당의 부분 공간) 을 $U$의 스패인에 대해 축소함으로써 구현됩니다. 절의 부정이 $U$의 스패인과 단일 방정식 $f$의 합에 포함되면, $f$가 추론됩니다.

3. 충격 분석을 통한 절 학습:
   이 논문은 1-UIP(첫 번째 고유 함의점) 절 학습 전략을 XNF 설정에 적응시킵니다. 함의 그래프가 선형 방정식으로 직접 번역되지 않기 때문에, 학습 알고리즘은 의미론적으로 작동합니다:

   • 충돌 절 (모순의 원인) 로 시작합니다.
   • 가장 최근의 결정을 담당하는 방정식을 분리하기 위해 기저 변경을 반복적으로 적용합니다.
   • 분리된 절과 충돌의 원인을 결합하여 결정 변수를 효과적으로 상쇄하기 위해 덧셈 규칙을 적용합니다.
   • 이 과정은 현재 결정 수준에서 전파를 강제하는 단언 절이 발견될 때까지 반복됩니다.

주요 기여

이론적 기여

• 양방향 연결: 이 논문은 CDCL(⊕) 이 Res(⊕) 증명을 생성할 뿐만 아니라, 비결정적 결정과 재시작이 주어지면 Res(⊕) 증명 시스템을 다항식적으로 시뮬레이션함을 증명합니다. 이는 고전적인 CDCL 과 배제 사이의 관계를 반영합니다.
• 새로운 증명 시스템 특징: 저자들은 Res(⊕) 와 다항식적으로 동등하지만 약화 규칙이 없는 새로운 추론 규칙 집합 (덧셈 및 기저 변경) 을 제공하여 알고리즘 구현에 적합하게 만듭니다.
• 입력 Res(⊕) 동등성: 이 논문은 CDCL(⊕) 의 단위 전파가 *입력 Res(⊕)*로 알려진 Res(⊕) 의 조각과 동등함을 증명하여 고전적 CDCL 에 대한 알려진 결과를 일반화합니다.
• 개선된 시뮬레이션 계수: 절의 분해가 흡수되는 방식을 최적화함으로써 고전적 CDCL/배제 관계에 대한 다항식 계수를 개선한 시뮬레이션 증명을 제시합니다 (간단한 논증으로 [7] 의 결과와 일치).

실용적 기여

• Xorcle 구현: 저자들은 CDCL(⊕) 을 위한 개념 증명 해결사 Xorcle를 제시합니다.
  • 비트 패킹을 사용하여 $\mathbb{F}_2$ 위의 효율적인 선형 대수를 구현합니다.
  • VSIDS 와 CMTF 를 XNF 컨텍스트로 일반화하는 새로운 절 선택 휴리스틱인 CSIDS(절 상태 독립 감쇠 합) 를 도입합니다.
  • 배제 표현을 지원하도록 LRUP 증명 로깅 형식을 확장한 **LRUP(⊕)**을 도입합니다.
• XNF 를 위한 휴리스틱: 이 논문은 감시 구조 (선형 의존성으로 인해 복잡한 감시 목록을 유지하는 대신 절을 순환), 결정 절차 (절의 부정에서 무작위 방정식에 분기), 그리고 위상 선택 (절이 거짓이 되도록 선호) 에 대한 적응 사항을 상세히 설명합니다.

실험 결과

저자들은 다음 벤치마크 세트를 사용하여 Xorcle 를 평가했습니다:

• Ascon-128: 암호학 관련 2-XNF 계열.
• 무작위 및 제한된 k-XNF: 다양한 변수 및 방정식 수를 가진 합성 공식.
• Tseitin 공식: 배제에 대해 어려운 것으로 알려진 CNF 인코딩된 배제 문제.

주요 발견:

• XNF 성능: Xorcle 는 네이티브 XNF 벤치마크에서 기존 해결사 (Kissat, CryptoMiniSAT, 2-Xornado) 보다 우수한 성능을 보였습니다. 특히, 일반적인 XNF 추론을 사용함에도 불구하고 Ascon-128 인스턴스에서 전용 2-XNF 해결사인 2-Xornado 보다 우수한 성능을 보였습니다.
• Tseitin 공식 성능: CNF 로 인코딩된 Tseitin 공식에서 Xorcle 는 실행 시간에 거의 다항식적인 확장성을 보인 반면, 배제 기반 해결사들은 지수 시간이 필요한 것으로 알려져 있습니다. 이는 전처리 없이 오직 핵심 CDCL(⊕) 추론에만 의존하여 달성되었습니다.
• 결정 품질: Xorcle 는 경쟁 해결사보다 훨씬 적은 결정을 요구했는데, 이는 배제 기반 분기 및 추론 메커니즘이 이러한 문제 클래스에 대해 더 효과적임을 시사합니다.

중요성 및 주장

이 논문은 CDCL(⊕) 이 배제 추론을 CDCL 패러다임에 완전히 통합하는 최초의 엄격한 이론적 프레임워크와 실용적 구현을 제공한다고 주장합니다.

• 이론적 중요성: CDCL 의 한계가 알고리즘 구조 자체에 내재된 것이 아니라 근본적인 증명 시스템 (배제) 에 있음을 확립합니다. Res(⊕) 로 전환함으로써 CDCL 은 이론적으로 표준 CDCL 에 대해 지수적으로 어려운 문제들을 해결할 수 있습니다.
• 실용적 중요성: 결과는 네이티브 XNF 해결이 CNF 또는 CNF-XOR 로 변환하는 것보다 실현 가능하고 잠재적으로 우월함을 시사합니다. 전처리 없이 거의 다항식 시간에 Tseitin 공식을 해결할 수 있는 능력은 배제 추론이 SAT 해결에서 알려진 난이도 장벽을 극복할 수 있는 잠재력을 강조합니다.
• 미래 방향: 저자들은 Xorcle 가 개념 증명임을 겸손하게 지적합니다. 현재는 절 삭제, 고급 재시작, 동적 휴리스틱과 같은 여러 표준 CDCL 최적화가 부족하며, '1-UIP'나 '절 최소화'와 같은 개념을 의미론적 XNF 설정으로 완전히 일반화하지는 못했습니다. 이 작업은 암묵적으로 배제 추론이 필요한 CNF 공식을 대상으로 하는 휴리스틱에 대한 추가 연구를 위한 문을 엽니다.