유한 도메인 소개

유한 도메인 소개

유한 도메인(FD) 제약 솔버의 개요와 FD 변수의 표현을 설명해요.

출처: GNU Prolog Manual - Introduction

본문

유한 도메인(FD) 제약 솔버는 Prolog를 FD에 대한 제약으로 확장해요. 이 기능은 GNU Prolog의 FD 부분이 설치된 경우에만 사용할 수 있어요. 솔버는 1987년 Jaffar와 Lassez가 도입한 Constraint Logic Programming 기법의 한 인스턴스예요 [7]. FD에 대한 제약은 전파(propagation) 기법, 특히 호 일관성(arc-consistency, AC)을 사용해 해결돼요. 관심 있는 독자는 P. Van Hentenryck의 "Constraint Satisfaction in Logic Programming"(1989)을 참조할 수 있어요 [8]. 솔버는 clp(FD) 솔버를 기반으로 해요 [4]. GNU Prolog FD 솔버는 새 종류의 변수인 유한 도메인(FD) 변수에 대해 산술 제약, 불리언 제약, 반영(reified) 제약, 기호 제약을 제공해요.

유한 도메인 변수

새로운 데이터 유형이 도입돼요: FD 변수는 자신의 도메인 안의 값만 취할 수 있어요. FD 변수의 초기 도메인은 0..fd_max_integer이며, 여기서 fd_max_integer는 어떤 FD 변수가 취할 수 있는 가장 큰 값을 나타내요. fd_max_integer/1 술어는 이 값을 반환하는데, 이 값은 max_integer Prolog 플래그(8.22.1절)와 다를 수 있어요.

FD 변수 X의 도메인은 제약에 의해 단조로운 방식으로 단계별로 축소돼요: 값이 X의 도메인에서 제거되면 다시 X의 도메인에 나타나지 않아요.

FD 변수는 Prolog 정수와 Prolog 변수 모두와 완전히 호환돼요. 즉 FD 제약이 FD 변수를 기대할 때 Prolog 정수(도메인이 싱글턴인 FD 변수로 간주)나 Prolog 변수(즉시 초기 범위 0..fd_max_integer에 바인딩)를 전달할 수 있어요. 이는 특정 유형 선언의 필요성을 피하게 해줘요.

FD 변수의 초기 도메인을 선언할 필요는 없지만(제약에 처음 나타날 때 0..fd_max_integer에 바인딩될 것이므로), 선언하는 것이 유리하며 가능한 한 빨리 도메인의 크기를 줄여줘요. 특히 GNU Prolog는 효율성 때문에 오버플로를 확인하지 않기 때문이에요. 예를 들어 X, Y, Z에 대한 예비 도메인 정의 없이 비선형 제약 X*Y#=Z는 Z의 도메인 상한을 계산할 때 fd_max_integer × fd_max_integer의 오버플로로 인해 실패할 거예요. 이 오버플로는 상한에 대해 음수 결과를 일으키고 제약은 그런 다음 실패해요.

FD 변수에는 두 가지 내부 표현이 있어요:

• 구간 표현: 변수의 min과 max만 유지. 이 표현에서는 0..fd_max_integer에 포함된 값을 저장할 수 있어요.
• 희소 표현: 추가 비트-벡터가 변수의 가능한 값 집합(즉 도메인)을 저장하는 데 사용. 이 표현에서는 0..vector_max에 포함된 값을 저장할 수 있어요. 기본적으로 vector_max는 127로 설정돼요. 이 값은 VECTORMAX 환경 변수나 내장 술어 fd_set_vector_max/1(9.2.3절)로 재정의될 수 있어요. fd_vector_max/1 술어는 vector_max의 현재 값을 반환해요(9.2.1절).

FD 변수 X의 초기 표현은 항상 구간 표현이고, 도메인에 "구멍(hole)"이 나타날 때(예: 부등식 제약으로 인해) 희소 표현으로 전환돼요. 변수가 희소 표현을 사용하면 도메인에 더 이상 구멍이 없어도 구간 표현으로 전환되지 않아요. 이 전환이 발생하면 vector_max가 fd_max_integer보다 작으므로 X의 도메인에 있는 일부 값이 손실될 수 있어요. X는 솔버에 의해 도메인 0..vector_max로 제약되므로(가상 제약 X #=< vector_max을 통해) "추가 제약됨(extra-constrained)"이라고 말해요. 각 FD 변수에는 희소 표현으로의 전환으로 인해 값이 손실되었음을 나타내는 extra_cstr이 연관돼요. 이 플래그는 모든 연산에서 갱신돼요. 추가 제약된 FD 변수의 도메인은 @ 기호가 뒤따라 출력돼요. 추가 제약된 변수에서 제약이 실패하면 Warning: Vector too small - maybe lost solutions (FD Var: N) 메시지가 표시돼요(N은 관련 변수의 주소).

예제 1(vector_max = 127):

이 예에서 제약 X #\= 10이 게시되면 일부 값이 손실되고 extra_cstr이 켜져요. 그러나 제약 X #=< 100을 게시하면 플래그가 꺼져요(값 손실 없음).

예제 2:

이 예에서 제약 X #>= 256은 128..512의 손실로 인해 실패하므로 터미널에 메시지가 표시돼요. 해법은 VECTORMAX 환경 변수를 설정(예: 512로)하거나 fd_set_vector_max(512)를 사용해 벡터의 크기를 늘리는 것으로 구성돼요.

마지막으로 비트-벡터는 동적이 아니에요. 즉 모든 벡터는 같은 크기(0..vector_max)를 가져요. 따라서 fd_set_vector_max/1의 사용은 벡터 크기의 초기 정의로 제한되고 어떤 제약보다 먼저 발생해야 해요. 앞서 본 것처럼 솔버는 너무 짧은 vector_max로 인해 실패가 발생할 때 메시지를 표시하려 해요. 불행히도 어떤 경우에는 값의 손실을 감지할 수 없고 메시지가 발행되지 않아요. 따라서 사용자는 이 매개변수가 어떤 벡터도 인코딩할 만큼 큰지 항상 주의해야 해요.

더 알아보기

• FD 변수 매개변수
• FD 솔버와 내장 술어