연속 지역 탐색(CLS, Continuous Local Search)을 기반으로 유사 부울 충족 가능성(pseudo-Boolean satisfiability) 문제를 GPU에서 가속 처리하는 솔버 AFSAT(Accelerated Fourier SAT)가 arXiv에 공개됐다. Cody J Christopher와 Charles Gretton이 저술한 이 논문은 기존 개념 증명 수준의 접근법을 완전한 공학적 구현체로 발전시킨 결과물이다. 단일 문제 인스턴스 안에서 대칭 제약 조건 유형과 길이의 이질적 조합을 모두 지원하는 것이 이전 연구와의 핵심 차이다.
AFSAT는 JAX 컴파일러의 자동 벡터화, 자동 미분, JIT(Just-In-Time) 컴파일 기능을 활용해 후보 할당 배치 전반에 걸쳐 대규모 병렬 CLS를 수행한다. 기존 개념 증명 대비 수치 안정성, 런타임 성능, 메모리 효율성이 크게 향상됐다고 저자들은 밝혔다. 성능 개선의 배경에는 메모리 레이턴시와 부동소수점 표현에서 비롯된 여러 한계를 식별하고 해결한 작업이 있으며, 자동 병렬화와 압축 표현 방식도 활용됐다. 부동소수점의 본질적 표현 한계는 맞춤형 이산 푸리에 변환 구현으로 부분적으로 보완했다.
다중 가속기로 규모를 확장할 때는 JAX 배열 샤딩(array sharding)을 활용해 거의 선형에 가까운 처리량을 달성했다. 충족 가능성(SAT) 문제는 AI 추론, 하드웨어 검증, 최적화, 프로그램 합성 등 다양한 분야의 핵심 계산 문제에 해당한다. 특히 유사 부울 제약 조건은 단순 이진 SAT보다 표현력이 높아 실세계 최적화 문제에 더 적합하지만, 그만큼 계산 부담도 크다.
AFSAT는 이 계산 부담을 GPU의 병렬 처리 능력으로 분산시키는 접근을 취함으로써, 기존 CPU 기반 SAT 솔버가 다루기 어렵던 대규모 문제를 실용적인 시간 안에 풀 수 있는 가능성을 보여준다. JAX 생태계와의 긴밀한 통합 덕분에 AI 연구자들이 기존 머신러닝 워크플로우에 SAT 솔버를 자연스럽게 결합할 수 있다는 점도 주목된다.
