2023년 CHC-COMP 대회 보고서

Core Concepts

2023년 CHC-COMP 대회는 제6회 Constrained Horn Clauses 솔버 경쟁 대회로, 7개의 솔버(6개 경쟁 솔버, 1개 hors concours 솔버)와 6개의 트랙으로 구성되었다.

Abstract

CHC-COMP 2023은 Constrained Horn Clauses(CHCs) 솔버의 성능을 평가하는 연례 대회이다. 이번 대회에는 7개의 솔버(6개 경쟁 솔버, 1개 hors concours 솔버)가 참여했으며, 6개의 트랙이 진행되었다. 각 트랙은 선형/비선형 CHCs와 선형 정수 산술, 배열, 재귀/비재귀 대수적 데이터 유형 등의 제약 조건을 다루었다.
대회 조직:

6개 트랙: LIA-lin, LIA-nonlin, LIA-lin-Arrays, LIA-nonlin-Arrays, LIA-nonlin-Arrays-nonrecADT, ADT-LIA-nonlin
기술 자원: StarExec 플랫폼의 chc-seq.q 큐 사용
테스트 및 경쟁 실행: 테스트 실행(600s CPU/wall-clock, 64GB 메모리), 경쟁 실행(1800s CPU/wall-clock, 64GB 메모리)
평가 모델: 각 트랙별 sat/unsat 결과 점수, CPU 시간으로 순위 결정
벤치마크:

SMT-LIB 2.6 형식의 벤치마크 사용
7,500개 이상의 고유 벤치마크 중 선별
각 트랙별 422-446개 벤치마크 선정
참가 솔버:

Eldarica, Golem, LoAT, Theta, Ultimate TreeAutomizer, Ultimate Unihorn, Spacer(hors concours)
결과:

LIA-lin: Golem 1위, Eldarica 2위, Theta 3위
LIA-nonlin: Eldarica 1위, Golem 2위, Ultimate Unihorn 3위
LIA-lin-Arrays: Eldarica 1위, Theta 2위, Ultimate Unihorn 3위
LIA-nonlin-Arrays: Eldarica 1위, Ultimate Unihorn 2위, Theta 3위
LIA-nonlin-Arrays-nonrecADT: Eldarica 1위, Ultimate Unihorn 2위, Theta 3위
ADT-LIA-nonlin: Eldarica 1위, Theta 2위, Ultimate Unihorn 3위

Stats

Golem은 LIA-lin 트랙에서 422개 벤치마크 중 122개의 sat 결과와 48개의 unsat 결과를 얻었다.
Eldarica는 LIA-nonlin 트랙에서 428개 벤치마크 중 9개의 sat 결과와 30개의 unsat 결과를 얻었다.
Theta는 LIA-lin-Arrays 트랙에서 446개 벤치마크 중 135개의 sat 결과와 50개의 unsat 결과를 얻었다.

Quotes

"CHC-COMP 2023은 제6회 Constrained Horn Clauses 솔버 경쟁 대회로, 7개의 솔버(6개 경쟁 솔버, 1개 hors concours 솔버)와 6개의 트랙으로 구성되었다."
"CHC-COMP는 실제적이고 공개된 벤치마크를 사용하여 최신 CHC 솔버의 성능을 평가하는 것을 목표로 한다."
"이번 대회에서는 ADT-LIA-nonlin 트랙이 새로 도입되었고, LRA-TS와 LRA-TS-par 트랙은 더 이상 진행되지 않았다."

Key Insights Distilled From

CHC-COMP 2023: Competition Report

by Emanuele De ... at arxiv.org 04-24-2024

https://arxiv.org/pdf/2404.14923.pdf

Deeper Inquiries

CHC-COMP 대회에서 솔버의 결과 검증 방법에 대한 논의가 필요해 보입니다. 솔버가 생성한 증거(모델 또는 반례)를 표준화하고 이를 활용하는 방안을 고려해볼 수 있습니다. CHC 문제의 상태(sat/unsat)를 명시하는 표준화된 방법을 도입하면 솔버의 정확성 검증에 도움이 될 것 같습니다. 이를 통해 대회 결과의 신뢰성을 높일 수 있을 것입니다. 병렬 트랙을 도입하면 솔버의 성능을 다각도로 평가할 수 있을 것 같습니다. CPU 시간 제한 대신 wall-clock 시간 제한을 두는 방식으로 병렬 처리 능력을 측정할 수 있습니다.

CHC-COMP 대회에서 솔버의 결과를 검증하기 위해 증거(모델 또는 반례)를 표준화하는 것은 매우 중요합니다. 이를 통해 솔버가 생성한 증거의 형식이 일관되고 이해하기 쉬워지며, 결과의 신뢰성을 높일 수 있습니다. 증거의 표준화를 위해 모든 솔버가 생성한 증거를 동일한 형식으로 제공하도록 요구할 수 있습니다. 예를 들어, 모델의 경우 변수와 조건을 명확히 표시하고, 반례의 경우 잘못된 부분을 명확히 나타내는 방식을 정의할 수 있습니다. 이렇게 하면 대회 결과를 분석하고 비교하는 데 도움이 될 것입니다.

CHC 문제의 상태를 명시하는 표준화된 방법을 도입하는 것은 CHC-COMP 대회의 결과를 더욱 신뢰할 수 있게 만들 수 있습니다. 각 문제에 대해 sat 또는 unsat 상태를 명시하는 표준 형식을 도입함으로써, 솔버의 결과를 쉽게 이해하고 비교할 수 있습니다. 이를 통해 솔버의 정확성을 검증하고 대회 결과의 일관성을 높일 수 있을 것입니다.

병렬 트랙을 도입함으로써 솔버의 성능을 다각도로 평가할 수 있습니다. CPU 시간 제한 대신 wall-clock 시간 제한을 두는 방식으로 병렬 처리 능력을 측정할 수 있습니다. 이를 통해 솔버의 병렬 처리 능력과 효율성을 평가하고, 다양한 환경에서의 성능을 비교할 수 있을 것입니다. 이를 통해 솔버의 다양한 측면을 평가하고 대회의 결과를 보다 다양한 관점에서 분석할 수 있을 것입니다.