열거된 솔루션을 통한 CNN 패턴 인식을 활용한 효율적인 제약 추론

제약 프로그래밍 (Constraint programming) 실무자들은 위험도 순서에 따라 적용되는 계층적 기술 세트를 통해 어려운 문제들을 가속화합니다. 표준 강화 (Standard hardening, 대칭성 깨기 및 함축적 제약)는 가장 먼저 적용되며 만족 가능성 (satisfiability)을 보존합니다. 솔루션의 구조적 하위 가족 (structural sub-family)으로 탐색을 제한하는 스트림라이너 제약 (Streamliner constraints)은 만족 가능성을 보존하지 않으므로 마지막 수단으로 남겨둡니다. 기존의 자동화된 스트림라이너 합성 (streamliner-synthesis) 접근 방식은 제약 문법 (constraint grammar)을 검색하거나 문제 모델에 대해 대규모 언어 모델 (Large Language Model, LLM)에 직접 프롬프트를 제공합니다. 우리는 다른 접근 방식을 제안합니다: 가능한 솔루션을 열거하고, 구조적 패턴을 탐지하기 위해 섭동된 비솔루션 (perturbed non-solutions)과 대조적으로 합성곱 신경망 (Convolutional Neural Network, CNN)을 대조 학습 (contrastively)시키며, CNN의 판별 신호 (discriminative signal)를 LLM 기반 합성을 통해 후보 MiniZinc 스트림라이너로 변환합니다. CNN은 LLM의 제약 생성 과정을 모델 텍스트뿐만 아니라 관찰된 솔루션 구조에 근거하게 합니다. 우리는 스트림라이너 발견이 잔여 성능 레버인 강화된 벤치마크 모델들을 대상으로 평가합니다. 우리의 파이프라인은 강화된 Vessel Loading에서 98.8%, 강화된 Social Golfers에서 98.6%, Black Hole에서 89.4%의 포트폴리오 시간 단축을 달성하였으며, 최상의 단일 스트림라이너는 각각 기하 평균 속도 향상(geometric-mean speedups)이 932배, 356배, 1103배에 달했습니다. 발견된 스트림라이너에는 Vessel Loading에 대한 클래스 기반 패킹 제약 (class-based packing constraints), Social Golfers에 대한 강화 이상의 정준화 (beyond-hardening canonicalisations), 그리고 Black Hole에 대한 레이아웃 좌표 경계 (layout-coordinate bounds)가 포함됩니다.