반례 유도 양방향 합성을 조금씩 더해가기로 가속하기

윤용호, 이우석, 이광근

http://doi.org/10.5626/JOK.2023.50.12.1091

반례 유도 방식을 접목한 입출력 예제 기반 합성에는 반례가 추가될 때마다 입출력 예제 기반 합성 과정을 처음부터 다시 시작해야 하는 비효율적인 면이 있다. 이 연구에서는 반례 유도 방식을 접목한 입출력 예제 기반 양방향 합성 알고리즘에 적용할 수 있는 조금씩 더해가기 방식을 제안한다. 이 방식을 적용하면 반례가 추가되었을 때 기존의 탐색 결과를 재활용하여 불필요한 탐색을 줄이고 합성을 가속할 수 있다. 조금씩 더해가기를 통한 성능 개선 효과를 확인하기 위해서, 최근에 제안된 양방향 합성 방법인 정방향-역방향 요약 해석 기반 합성기 Simba에 이 연구에서 제안하는 조금씩 더해가기 방식을 적용하였다. 4가지 종류의 벤치마크에 속한 1,125개의 합성 문제에 대해 기본 알고리즘과 조금씩 더해가기 변형 알고리즘의 성능을 비교 실험한 결과, 합성 결과의 품질을 유지하면서도 합성 시간이 평균적으로 74.2%로 감소하는 것을 확인할 수 있었다.