Zykov 트리를 모방한 인코딩을 기반으로 그래프 채색 문제를 해결하는 새로운 SAT 기반 알고리즘인 ZykovColor를 소개합니다. Hebrard와 Katsirelos (2020)의 접근 방식을 기반으로 하며, 추이 제약 조건을 적용하고, 탐색 트리 가지치기를 위한 하한을 통합하며, 추론된 전파를 가능하게 하는 전파자를 사용합니다. CaDiCaL을 위한 최근에 도입된 IPASIR-UP 인터페이스를 활용하여 SAT 솔버로 이러한 기술을 구현합니다. 또한, 정점 지배 힌트를 사용한 통합 결정 전략 수정 및 이전 호출에서 학습된 절을 재사용할 수 있는 점진적 하향식 검색과 같은 SAT 솔버를 활용하는 새로운 기능을 제안합니다. 추가적으로, 검색 중 가지치기에 사용되는 하한을 개선하기 위해 더 효과적인 클릭 계산과 분수 채색수를 계산하는 알고리즘을 통합합니다. DIMACS 벤치마크 세트에서 다른 최첨단 그래프 채색 구현보다 ZykovColor가 우수함을 보입니다. 또한, 무작위 Erd\H{o}s-Renyi 그래프에 대한 추가 실험을 통해 매우 희소하거나 매우 조밀한 그래프 모두에서 최첨단 SAT 기반 방법을 능가하거나 일치함을 보입니다. Erd\H{o}s-Renyi 그래프에서 다른 SAT 기반 방법을 능가하는 ZykovColor의 추가 구성을 제공합니다.
