선언적 최적화를 통한 최적화의 최적화: egglog를 이용한 수학적 최적화 내 고차 함수 (Higher-Order Functions) 최적화

요약

JijModeling 2에서 egglog를 활용하여 수학적 모델링의 최적화를 개선하는 두 가지 사례를 소개합니다. 고차 함수를 엔슈가링하여 자연스러운 LaTeX 출력을 생성하고, Datalog 스타일의 규칙을 통해 복잡한 제약 조건 탐지 로직을 효율적으로 구현할 수 있음을 보여줍니다.

핵심 포인트

• egglog의 등식 포화(equality saturation)와 사용자 정의 비용 모델을 사용하여 고차 함수를 최적화된 수학적 표기법으로 재구성함
• Datalog 스타일의 규칙을 사용하여 외부 코드 없이 egglog 내에서 다단계 제약 조건 탐지 로직을 직접 구현 가능
• Henkin-like constants와 egglog 팩트를 활용하여 매개변수화된 제약 조건 및 부수 조건을 효과적으로 전파
• 엔슈가링 절차를 통해 대규모 도메인 집합 조건을 축소함으로써 탐지 성능을 수 분에서 수 초 단위로 대폭 단축