FLINGO -- Instilling ASP Expressiveness into Linear Integer Constraints

"flingo — 선형 정수 제약에 ASP 표현력 주입"의 기술 요약

문제 제기
제약 답 집합 프로그래밍 (CASP) 은 표준 답 집합 프로그래밍 (ASP) 도구의 확장성을 초과하는 수치 계산을 처리하도록 설계된 하이브리드 패러다임입니다. 표준 ASP 는 그라운딩 (grounding) 단계를 거친 후 해를 구하는 방식에 의존하는 반면, CASP 는 대규모 수치 도메인으로 인한 그라운딩 폭발을 피하기 위해 수치 제약을 백엔드 솔버 (대개 Satisfiability Modulo Theory 원칙을 따름) 에 위임합니다. 그러나 clingcon 과 같은 현재 CASP 솔버들은 상당한 모델링 간극을 겪고 있습니다: 제약 원자 (constraint atoms) 의 명세는 종종 ASP 패러다임의 고수준 선언적 기능보다는 수치 백엔드의 운영 요구 사항과 정렬되어 있습니다.

구체적으로, 기존 시스템에서 수치 속성을 제약 변수로 표현할 때, 몇 가지 핵심 ASP 기능이 손실되거나 표현하기 어려워집니다:

1. 미정의성 (Undefinedness): 속성에 기본 값을 할당하는 대신 미정으로 남겨둘 수 있는 능력.
2. 기본 값 (Default Values): 예외에 의해 재정의될 수 있는 기본 값을 선언할 수 있는 능력.
3. 비결정적 할당: 선택 규칙을 통해 속성 값에 관한 비결정적 선택을 할 수 있는 능력.
4. 집계 (Aggregates): 특히 해당 변수가 미정일 수 있을 때, 제약 변수에 대한 집계 (예: 합계, 최소값) 를 사용할 수 있는 능력.

HTc(Here-and-There with constraints) 논리와 같은 기존 접근 방식은 미정의성과 집계에 대한 의미론적 기초를 마련했으나, 이러한 기능을 표준 CASP 워크플로우에 완전히 통합하는 포괄적인 언어 정의와 도구 구현은 부족했습니다.

방법론
저자들은 앞서 언급한 ASP 표현력을 선형 정수 제약에 직접 통합하는 새로운 CASP 시스템 및 언어인 flingo를 소개합니다. 이 방법론은 다음과 같은 구성 요소에 기반합니다:

1. 의미론적 기초 (HTc): flingo의 의미론은 제약이 포함된 Here-and-There 논리 (HTc) 를 사용하여 형식화됩니다. 이 프레임워크는 "Here"(현재 지식) 와 "There"(잠재적 지식) 사이의 구분을 가능하게 하여 미정 변수의 표현을 지원합니다.

   • 미정의성: 정수 변수는 기본적으로 미정으로 정의됩니다. 변수는 프로그램의 규칙을 통해 "기반 (founded)"되어 유도될 때만 정의됩니다.
   • 엄격한 vs 비엄격한 집계: 언어는 엄격한 (&sus) 과 비엄격한 (&sum) 연산을 구분합니다.
     • &sus(엄격한 합계): 모든 항이 정의되어야 합니다. 어떤 변수라도 미정인 경우, 제약 원자는 거짓으로 평가됩니다.
     • &sum(비엄격한 합계): 계산에서 미정 항을 제거 (중립 요소인 0 으로 간주) 하여 표준 ASP 집계 행동을 모방합니다.
   • 조건부 항: flingo는 s : l1, ..., ln 형태의 조건부 항을 지원합니다. 여기서 리터럴의 논리곱이 성립하면 곱셈 항 s가 사용되고, 그렇지 않으면 기본 항 (맥락에 따라 다름) 이 사용됩니다.

2. 구문 및 기능:

   • 제약 원자: &sum, &sus, &min, &max, 그리고 &df(defined) 원자를 지원합니다.
   • 할당 규칙: &fun{t1; ...; tn} =: s :- l1, ..., lm 형태의 규칙을 도입하여, 조건이 충족되고 소스 변수가 정의된 경우에만 항 t1...tn에 기반하여 변수 s를 정의합니다.
   • 정수를 위한 선택 규칙: 정수 변수의 비결정적 할당을 허용하는 범위 기반 선택 규칙 (예: &in{s1..s2} =: x) 을 지원합니다.

3. 구현 및 번역:

   • flingo 솔버는 clingo의 이론 인터페이스를 확장하여 구현되었습니다.
   • 핵심적으로, flingo는 백엔드로 clingcon을 사용합니다. 이를 위해 시스템은 flingo 프로그램을 표준 clingcon 프로그램으로 변환하기 위해 8 가지 선형 시간 재작성 변환을 수행합니다.
   • 이 번역 과정은 다음을 포함합니다:
     • 조건부 항을 명제 원자와 보조 규칙으로 대체.
     • 미정 변수를 처리하는 규칙과 결합하여 &sum(비엄격한) 연산을 &sus(엄격한) 연산으로 변환하되, 백엔드에 필요할 때만 중립 값 (0) 을 할당.
     • &sus와 보조 명제 원자를 사용하여 &min 및 &max 연산 인코딩.
     • 백엔드에서 여러 개의 안정 모델이 생성되지 않도록 flingo의 미정 변수를 명시적으로 "미정" 상태로 처리.

주요 기여

1. 언어 설계: 기본값, 미정의성, 선택, 집계와 같은 ASP 의 선언적 기능과 수치 제약 해결의 효율성을 통합하는 flingo 언어의 도입.
2. 의미론 형식화: 미정 정수 변수의 처리와 엄격한 및 비엄격한 집계 간의 구분을 특히 다루는 HTc 기반의 flingo 의미론에 대한 엄밀한 정의.
3. 번역 메커니즘: flingo 구문을 clingcon 입력 형식으로 변환하는 검증된 번역으로, 향상된 표현력이 기존 고성능 CASP 백엔드를 사용하여 실현될 수 있음을 입증.
4. 이론적 속성: 이 논문은 flingo와 clingcon 모델 간의 관계를 보여주는 명제들을 제시합니다. 특히, flingo가 정수 변수에 대한 비단조 추론을 허용함을 보여줍니다 (예: x = 1 :- &sus{y} = 1 규칙은 y가 미정일 때 x를 미정으로 만듭니다. 반면 사실 &sus{y} = 1을 추가하면 x가 정의됩니다). 이는 표준 clingcon에서는 불가능한 기능입니다.

결과 및 평가
이 논문은 flingo의 유용성을 보여주는 예시들을 제공합니다:

• 관세 예시: 기본 관세와 예외를 포함하는 문제를 재검토합니다. flingo는 특정 예외 (예: 철강) 가 정의되지 않는 한 기본 값을 할당하고, 미정 관세를 무시하는 비엄격한 합계를 사용하여 세수 (tax income) 를 계산하는 자연스러운 인코딩을 가능하게 합니다.
• 자전거 구성: 프레임과 가격 계산이 포함된 선택적 가방을 다루는 구성 문제입니다. 이 예시는 flingo가 표준 ASP 의 "외관과 느낌"을 유지하면서 선택적 구성 요소, 기본 가격 범위, 그리고 가격의 집합을 어떻게 처리하는지 보여줍니다.
• 경험적 주장: 저자들은 flingo가 Coom 구성 언어에서 구성 문제를 모델링하는 데 사용되었다고 명시합니다. 이러한 경우, flingo는 큰 도메인을 가진 수치 속성을 포함하는 문제에서 clingo(제약 없음) 보다 현저히 우수한 성능을 보입니다.

의의
이 논문은 flingo가 고수준 ASP 모델링과 수치 제약 해결의 운영 요구 사항 사이의 간극을 메운다고 주장합니다. 그 의의는 다음과 같습니다:

• ASP 패러다임 보존: 수치 제약과 작업할 때조차 기본값과 집계와 같은 표준 ASP 모델링 기능을 유지할 수 있게 하여, 제약 백엔드의 제한 사항에 맞춰 모델을 적응시킬 필요가 없습니다.
• 미정의성 처리: 제약 설정에서 미정 변수의 개념을 공식적으로 지원하여, 불완전한 정보와 기본값을 모델링하는 데 필수적입니다.
• 실용적 구현: clingcon으로 번역함으로써 완전히 새로운 솔버 아키텍처 없이도 최첨단 CASP 솔버의 효율성을 활용하여, 이 접근 방식을 즉시 적용 가능하게 합니다.

저자들은 현재 구현이 clingo의 이론 문법에 의존하지만, 향후 작업은 입력 언어를 정교화하고 번역 과정을 최적화하여 확장성을 더욱 향상시키는 데 초점을 맞출 것이라고 언급합니다. 이 시스템은 공개적으로 이용 가능합니다.