제약 로직 프로그래밍

제약 논리 프로그래밍은 제약 조건 프로그래밍의 한 형태로, 제약 조건 만족으로부터의 개념을 포함하도록 논리 프로그래밍을 확장합니다.제약조건 논리 프로그램은 절 본문에 제약조건을 포함하는 논리 프로그램입니다.제약조건을 포함하는 절의 예는 다음과 같습니다.A(X,Y) :- X+Y>0, B(X), C(Y)이 조항에서X+Y>0제약이 됩니다.A(X,Y),B(X),그리고.C(Y)일반 로직 프로그래밍과 같은 리터럴입니다.이 조항은 진술이 다음과 같은 조건을 명시하고 있다.A(X,Y)유지:X+Y0보다 크고 둘 다B(X)그리고.C(Y)사실이야.

정규 논리 프로그래밍과 마찬가지로 프로그램은 리터럴 외에 제약조건을 포함할 수 있는 목표의 실현 가능성에 대해 질문됩니다.목표에 대한 증명은 본문이 만족할 수 있는 제약조건인 절과 다른 절을 사용하여 증명될 수 있는 리터럴로 구성됩니다.실행은 인터프리터에 의해 실행됩니다.인터프리터는 목표에서 시작하여 목표를 증명하려는 구를 재귀적으로 스캔합니다.이 검색 중에 발생한 제약 조건은 제약 조건 저장소라는 세트에 배치됩니다.이 세트가 만족스럽지 못한 것으로 판명되면 통역사는 역추적하여 목표를 증명하기 위해 다른 절을 사용하려고 합니다.실제로 제약조건 저장소의 만족도는 항상 불일치를 검출하는 것은 아닌 불완전한 알고리즘을 사용하여 확인할 수 있습니다.

개요

형식적으로는 제약 로직 프로그램은 일반 로직 프로그램과 같지만, 절의 본문은 정규 로직 프로그래밍 리터럴 외에 제약을 포함할 수 있습니다.예를 들면,X>0는 제약조건이며 다음 제약조건 논리 프로그램의 마지막 절에 포함되어 있습니다.

B(X,1):- X< >0. B(X,Y):- X=1, Y>0. A(X,Y):- X>0, B(X,Y).

일반 로직 프로그래밍과 마찬가지로 다음과 같은 목표를 평가합니다.A(X,1)마지막 절의 본문을 평가할 필요가 있다Y=1일반 로직 프로그래밍과 마찬가지로 목표를 증명해야 합니다.B(X,1)일반 로직 프로그래밍과는 달리, 이것은 또한 충족되어야 하는 제약이 필요합니다.X>0마지막 절 본문의 제약조건(일반 로직프로그래밍에서는 X가 완전히 그라운드 용어에 바인드되지 않는 한 X>0을 증명할 수 없으며 그렇지 않은 경우에는 프로그램 실행이 실패합니다).

제약 조건이 충족되는지 여부는 제약 조건이 충족될 때 항상 결정될 수 없습니다.예를 들어, 이 경우 다음과 같은 값이X마지막 구가 평가될 때 결정되지 않습니다.그 결과, 제약은X>0이 시점에서 만족하지도 위반하지도 않습니다.의 평가를 진행하기보다는B(X,1)그리고 그 결과 값(예측값)이X그 후, 인터프리터는 제약 조건을 저장합니다.X>0그리고 나서 평가로 넘어갑니다.B(X,1); 이렇게 하면 인터프리터는 제약조건 위반을 검출할 수 있습니다.X>0평가 중에B(X,1)이 경우 평가를 기다리지 않고 즉시 역추적합니다.B(X,1)결론짓다.

일반적으로 제약논리 프로그램의 평가는 일반논리 프로그램과 마찬가지로 진행된다.그러나 평가 중에 발생하는 제약조건은 제약조건 스토어라는 세트에 배치됩니다.예를 들어, 목표에 대한 평가A(X,1)첫 번째 절의 본문을 평가함으로써 진행되다Y=1; 이 평가에서는X>0목표를 필요로 하는 제약 조건 스토어B(X,1)증명될 것입니다.이 목표를 증명하기 위해 노력하는 동안 첫 번째 조항이 적용되지만 그 평가는 추가된다.X<0제약 조건 저장소로 이동합니다.이 추가에 의해 제약 스토어가 불만족스러워집니다.그런 다음 인터프리터가 역추적하여 제약 조건 저장소에서 마지막 추가를 제거합니다.두 번째 절의 평가는 다음과 같다.X=1그리고.Y>0제약 조건 저장소로 이동합니다.제약 조건 스토어가 만족스럽고 증명할 다른 리터럴이 남아 있지 않기 때문에 인터프리터는 솔루션을 사용하여 정지합니다.X=1, Y=1.

의미론

제약 로직 프로그램의 의미론은 실행 중 쌍 execution $\langle G,S\rangle$ $\langle G,S\rangle$ ${\$ \ $displaystyle$ \ $langle$ G $, S$ \ $rangle }$ 를 $\langle G,S\rangle$ 유지하는 가상 인터프리터의 관점에서 정의할 수 있습니다.이 쌍의 첫 번째 요소는 현재 목표라고 하며 두 번째 요소는 제약 조건 저장이라고 합니다.현재 목표에는 해석자가 증명하려고 하는 리터럴이 포함되며, 일부 제약 조건도 포함될 수 있습니다. 제약 조건 저장소에는 해석자가 지금까지 만족할 수 있다고 가정한 모든 제약 조건이 포함됩니다.

처음에 현재 목표는 목표이며 제약 조건 저장소는 비어 있습니다.통역자는 현재 목표에서 첫 번째 요소를 제거하고 분석하여 진행합니다.이 분석에 대한 자세한 내용은 아래에 설명되어 있지만, 결국 이 분석은 성공적인 종료 또는 실패를 초래할 수 있습니다.이 분석에는 재귀 호출과 현재 목표에 대한 새로운 리터럴 추가 및 제약 조건 저장소에 대한 새로운 제약 조건이 포함될 수 있습니다.인터프리터는 장애가 발생했을 경우 역추적합니다.현재 목표가 비어 있고 제약 스토어가 충족될 수 있을 때 성공적인 종료가 생성된다.

목표에서 제거된 리터럴의 분석 내용은 다음과 같습니다.골문 앞에서 이 리터럴을 제거한 후 구속조건인지 리터럴인지를 확인합니다.제약 조건인 경우 제약 조건 저장소에 추가됩니다.리터럴의 경우, 리터럴의 동일한 술어를 가진 구가 선택됩니다.구절은 변수를 새로운 변수로 대체함으로써 다시 작성됩니다(목표에서 발생하지 않는 변수). 결과는 절의 새로운 변종이라고 불립니다.그 후 절의 새로운 변종 본문은 목표 앞에 배치됩니다.ea의 동등성새로운 변형 헤드와 대응하는 리터럴의 ch 인수도 목표 앞에 배치한다.

이러한 조작중에 몇개의 체크가 행해집니다.특히 제약조건 스토어는 새로운 제약조건이 추가될 때마다 일관성이 체크됩니다.원칙적으로 제약조건 스토어가 만족스럽지 못할 때마다 알고리즘은 역추적을 할 수 있습니다.그러나 각 단계에서 불만족 여부를 확인하는 것은 비효율적입니다.따라서 불완전한 만족도 체커를 대신 사용할 수 있다.실제로, 만족도는 제약 조건 저장소를 단순화하는 방법, 즉 동등하지만 해결이 용이한 형태로 다시 쓰는 방법을 사용하여 검사됩니다.이러한 방법은 때때로 불만족한 제약 조건 저장소의 만족도를 항상 입증하는 것은 아닙니다.

통역은 현재 목표가 비어 있고 제약조건 스토어가 만족스럽지 못한 것으로 감지되지 않을 때 목표를 증명합니다.실행 결과는 현재 (간소화된) 제약 조건 세트입니다.이 세트에는 변수를 특정 값으로 강제하는 X $X=2$ (\ $displaystyle$ X $=2$ )와 $X=2$ 같은 제약 조건이 포함될 수 있지만 특정 값을 지정하지 않고 변수만 바인딩하는 X $X>2$ > $X>2$ (\ $displaystyle$ X $>2)$ 와 $X>2$ $X>2$ 제약 조건이 포함될 수도 있습니다.

형식적으로 제약 논리 프로그래밍의 의미는 파생이라는 관점에서 정의된다.트랜지션은 " $\langle G,S\rangle \rightarrow \langle G',S'\rangle$ " $"$ " $\langle G,S\rangle \rightarrow \langle G',S'\rangle$ , "S" , " $\langle G,S\rangle \rightarrow \langle G',S'\rangle$ $"\$ $displaystyle$ $G,S\rangle \rightarrow \rightarrow$ \ $rangle$ G", " $S'\$ $rangle$ $"$ 와 같은 쌍으로, $\langle G,S\rangle$ " $\langle G,S\rangle$ " 에서 "state G $"$ 로 이행할 가능성을 $나타냅니다$ 다음과 같은 세 가지 경우에 랜스가 가능합니다.

G의 $요소$ 는 $제약조건$ C, $G'=G\backslash \{C\}$ $G'=G\backslash \{C\}$ $G'=G\backslash \{C\}$ $G'=G\backslash \{C\}$ { $G'=G\backslash \{C\}$ $}$ { $style$ G' $= G$ \ $backslash$ \ { $C$ $G'=G\backslash \{C\}$ \ } $S'=S\cup \{C\}$ $S'=S\cup \{C\}$ S $S'=S\cup \{C\}$ { C $}$ { $display style$ S $S'=S\cup \{C\}$ = $S'=S\cup \{C\}$ S \ cup \ { C \ $S'=S\cup \{C\}$ } 、 즉 제약조건 스토어를 목표에서 이동할 수 있습니다.
G의 $요소$ 는 $L(t_{1},\ldots ,t_{n})$ L ( $L(t_{1},\ldots ,t_{n})$ 1 , $L(t_{1},\ldots ,t_{n})$ , $L(t_{1},\ldots ,t_{n})$ $){$ $displaystyle$ L ( t $_$ { $1}$ , \ $ldots$ , $t$ _ { $n$ } $L(t_{1},\ldots ,t_{n})$ 입니다. $L(t_{1}',\ldots ,t_{n}'):-B$ 변수를 사용하여 다시 쓴 $L(t_{1}',\ldots ,t_{n}'):-B$ ( $L(t_{1}',\ldots ,t_{n}'):-B$ 1 $L(t_{1}',\ldots ,t_{n}'):-B$ $L(t_{1}',\ldots ,t_{n}'):-B$ , $L(t_{1}',\ldots ,t_{n}'):-B$ n $L(t_{1}',\ldots ,t_{n}'):-B$ ) $L(t_{1}',\ldots ,t_{n}'):-B$ ) : - B $L(t_{1}',\ldots ,t_{n}'):-B$ ( \ $displaystyle$ L ( $t$ _ {1 $}$ , \ $ldots ,$ t $_$ { n $L(t_{1}',\ldots ,t_{n}'):-B$ ) : { n } } $L(t_{1}',\ldots ,t_{n}'):-B$ $L(t_{1},\ldots,t_{n}}$ 은 $L(t_{1},\ldots ,t_{n})$ (는) $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ 1 $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ , $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ , $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ n $= t$ , $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ { $display t$ _ {1 $}$ 、 $\ldots$ , $t$ _ { n } $S'=S$ = $t$ _ { n } , $S'=S$ 、 S $S'=S$ $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B$ ′ s s $S'=S$ $=$ S { $display style$ S $S'=S$ 。개미와 위의 조건과 목표의 동등성
$S'$ 와 S{\(\ $displaystyle$ S $')$ 는 $S'$ 특정 제약 의미에 따라 동등합니다.

일련의 전환은 파생된 것입니다. $목표$ G는 어떤 만족할 수 있는 제약 $스토어$ S에 대해 $\langle \emptyset ,S\rangle$ $\langle G,\emptyset \rangle$ G $\langle G,\emptyset \rangle$ θ G $,$ $θ$ $\langle \emptyset ,S\rangle$ $S$ $\langle \emptyset ,S\rangle$ , S $\langle \emptyset ,S\rangle$ θ $,$ $θ$ , S, $θ,$ S $\rangle$ 에 $\langle \emptyset ,S\rangle$ 대한 파생물이 존재하면 증명할 수 있다.이 의미론은 처리할 목표의 리터럴과 리터럴을 대체할 절을 임의로 선택하는 해석자의 가능한 진화를 공식화한다.다시 말해, 목표는 빈 목표와 만족스러운 저장소로 이어지는 리터럴과 절의 선택 순서가 존재하는 경우 이 의미론 하에서 증명된다.

실제 인터프리터는 목표 요소를 LIFO 순서로 처리합니다.즉, 요소가 전면에 추가되고 전면에서 처리됩니다.또한 두 번째 규칙의 절은 작성된 순서에 따라 선택하고 제약 조건 저장소가 변경되면 다시 씁니다.

세 번째 가능한 전환 유형은 구속조건 저장소를 동등한 것으로 교체하는 것입니다.이 대체는 제약 조건 전파와 같은 특정 방법에 의해 수행되는 것으로 제한됩니다.제약조건 논리 프로그래밍의 의미는 사용되는 제약조건의 종류뿐만 아니라 제약조건 저장소를 다시 쓰는 방법에 대해서도 파라메트릭합니다.실제로 사용되는 특정 방법은 제약 조건 저장소를 보다 쉽게 해결할 수 있는 방법으로 대체합니다.제약 조건 스토어가 만족스럽지 못한 경우, 이 단순화를 통해 이러한 만족스럽지 못한 점이 검출될 수 있지만 항상 검출되는 것은 아닙니다.

목표가 증명되면 제약 논리 프로그램에 대한 목표 평가 결과가 정의된다.이 경우, 초기 쌍에서 목표가 비어 있는 쌍으로의 파생이 존재합니다.이 두 번째 쌍의 제약 조건 저장소는 평가 결과로 간주됩니다.이는 제약 조건 저장소가 목표를 증명하는 데 적합하다고 가정한 모든 제약 조건을 포함하기 때문입니다.즉, 이러한 제약을 충족하는 모든 변수 평가에 대해 목표가 증명됩니다.

두 리터럴의 쌍방향 동일성은 종종 L $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ( $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ 1, $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ … , $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ n ) $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ( $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ 1 $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ , , $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ , $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ n $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ) { $displaystyle$ L ( t $_$ {1 $}$ , \ $ldots$ , $t_{n$ } ) $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'$ $L$ ( $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'$ ${1}$ , \ $ldots$ , $t_n}$ $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ 로 간략하게 표현된다. $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'$ $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ 의 일반적인 의미론은 L $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ( $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ 1 $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ , ... $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ , t $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ n ) $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ( t 1 $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ... , $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ $L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')$ ){ $displaystyle$ L $( t$ _ { $1}$ , $\ldots$ , $t_{n$ } = $L$ ( t _ {1} , $\ldots$ , $t_n}$ )를 제약 로직접적으로 저장합니다.

조건

다양한 용어의 정의를 사용하여 다양한 종류의 제약조건 논리 프로그래밍(트리, 실 또는 유한 도메인)을 생성합니다.항상 존재하는 제약의 종류는 용어의 평등이다.이러한 제약이 필요한 이유는 통역사가 다음과 같이 덧붙이기 때문입니다.t1=t2문자 그대로가 될 때마다 목표를 향해P(...t1...)머리 부분이 다음과 같은 절의 신선 변종 본문으로 대체됩니다.P(...t2...).

트리 용어

트리 용어를 사용한 제약조건 논리 프로그래밍은 대체를 제약조건 저장소의 제약조건으로 저장함으로써 정규 논리 프로그래밍을 에뮬레이트합니다.항은 다른 항에 적용되는 변수, 상수 및 함수 기호입니다.고려되는 유일한 제약조건은 용어 간의 동등성과 불일치이다.평등은 다음과 같은 제약 조건과 같이 특히 중요하다.t1=t2는 통역에 의해 생성되는 경우가 많습니다.용어의 동등성 제약은 통합을 통해 단순화할 수 있으며, 이를 통해 해결됩니다.

제약 사항t1=t2두 용어가 다른 용어에 적용되는 함수 기호인 경우 를 단순화할 수 있습니다.두 함수 기호가 동일하고 하위 조건의 수 또한 동일할 경우 이 제약조건은 하위 조건의 쌍방향 동등성으로 대체될 수 있습니다.항이 서로 다른 함수 기호 또는 동일한 함수자로 구성되어 있지만 용어의 수가 다른 경우에는 제약 조건이 충족되지 않습니다.

두 항 중 하나가 변수인 경우 변수가 사용할 수 있는 유일한 값은 다른 항입니다.그 결과, 다른 항은 현재 목표 및 제약 조건 저장소의 변수를 대체할 수 있으며, 따라서 고려 대상에서 변수를 실질적으로 제거할 수 있습니다.변수 자체와 동일한 특정 경우에는 항상 만족하는 대로 구속조건을 제거할 수 있습니다.

이러한 형태의 제약 조건 만족에서 변수 값은 항입니다.

리얼

실수에 의한 제약 로직 프로그래밍에서는, 실식을 용어로 사용합니다.함수 기호가 사용되지 않는 경우 항은 변수를 포함하여 실수에 대한 표현식입니다.이 경우 각 변수는 값으로 사용할 수 있는 것은 실수뿐입니다.

정확히 말하면 항은 변수와 실제 상수에 대한 표현식입니다.용어 간 동일성은 해석자가 실행 중에 용어의 동일성을 생성하기 때문에 항상 존재하는 제약 조건의 일종입니다.예를 들어, 현재 목표의 첫 번째 리터럴이A(X+1)통역사가 선택한 조항은 다음과 같습니다.A(Y-1):-Y=1개서가 변수인 후 현재 목표에 추가된 제약조건은 다음과 같습니다.X+1=Y-1 $Y=1$ Y $Y=1$ {\ $displaystyle Y=$ 1 $Y=1$ 함수 기호에 사용되는 단순화 규칙은 분명히 사용되지 않습니다.X+1=Y-1첫 번째 표현이 다음과 같이 만들어졌다고 해서 불만족스러운 것은 아니다.+그리고 두 번째 사용-.

실수와 함수 기호를 조합하여 실수에 대한 표현식 및 함수 기호를 다른 용어에 적용할 수 있습니다.형식적으로 변수와 실수 상수는 다른 식에 대한 산술 연산자와 마찬가지로 식입니다.변수, 상수(영역함수 기호) 및 식은 항에 적용되는 함수 기호와 마찬가지로 항입니다.즉, 항은 식 위에 작성되고 식은 숫자와 변수 위에 작성됩니다.이 경우 변수는 실수와 항에 걸쳐 있습니다.즉, 변수는 실수를 값으로 사용하고 다른 변수는 항을 사용할 수 있습니다.

두 항 중 어느 것도 실제 식이 아닌 경우 트리 항에 대한 규칙을 사용하여 두 항의 동일성을 단순화할 수 있습니다.예를 들어, 두 용어의 함수 기호와 하위 용어의 수가 같으면 동일 제약 조건을 하위 용어의 동일성으로 대체할 수 있습니다.

유한 도메인

제약조건 논리 프로그래밍에서 사용되는 제약조건의 세 번째 클래스는 유한 도메인의 제약조건입니다.이 경우 변수 값은 유한 도메인(종종 정수 도메인)에서 가져옵니다.변수마다 다른 도메인을 지정할 수 있습니다.X::[1..5]예를 들어의 가치를 의미한다.X사이에 있다.1그리고.5. 변수의 영역 또한 모든 변수를 취할 수 있는 가치를 열거하기에 의해;그러므로, 이 모든 선언문은 또 쓸 수 있습니다가 주어질 수 있다.X::[1,2,3,4,5]. 도메인을 명시하는 이 두번째 방법 같은 정수의 작곡되지 않고 있도메인을 허용하고 있다.X::[george,mary,john]만약 변수의 도메인 지정되지 않는다., 정수 언어로 대표의 집합으로 추정된다.변수의 한 단체는 같은 도메인 같은 선언을 사용하여 주어질 수 있다.[X,Y,Z]::[1..5].

실행 중에 변수의 도메인이 축소될 수 있습니다.실제로 인터프리터는 제약조건 스토어에 제약조건을 추가할 때 로컬 일관성의 형식을 적용하기 위해 제약조건 전파를 수행하며 이러한 연산은 변수의 영역을 줄일 수 있습니다.변수의 도메인이 비어 있으면 제약 조건 저장소가 일관되지 않고 알고리즘이 역추적됩니다.변수의 도메인이 싱글톤이 되면 해당 도메인에서 변수에 원하는 값을 할당할 수 있습니다.일반적으로 적용되는 일관성의 형태는 아크 일관성, 하이퍼 아크 일관성 및 제한 일관성입니다.변수의 현재 도메인은 다음과 같은 특정 리터럴을 사용하여 검사할 수 있습니다.dom(X,D)현재 도메인을 검색합니다.D변수의X.

실의 도메인에 대해서는, 정수의 도메인과 함께 펑터를 사용할 수 있다.이 경우 항은 정수 표현식, 상수 또는 다른 항에 대한 펑터의 적용일 수 있습니다.변수는 도메인이 정수 또는 상수 집합으로 지정되지 않은 경우 임의 용어를 값으로 사용할 수 있습니다.

제약 조건 저장소

제약 조건 저장소에는 현재 만족할 수 있다고 가정된 제약 조건이 포함되어 있습니다.정규 로직 프로그래밍의 현재 대체가 무엇인지를 고려할 수 있습니다.트리 용어만 허용되는 경우 제약 조건 저장소에 제약 조건이 포함됩니다.t1=t2; 이러한 제약조건은 통일에 의해 단순화되며, 결과적으로 형태의 제약조건이 발생한다.variable=term; 이러한 제약조건은 치환과 동등하다.

그러나 제약 조건 저장소는 다음 형식의 제약 조건을 포함할 수도 있습니다.t1!=t2차이점일 경우!=조건 간은 허용됩니다.Real 또는 유한 도메인에 대한 제약이 허용되는 경우 제약 조건 저장소는 다음과 같은 도메인별 제약 조건을 포함할 수도 있습니다.X+2=Y/2,기타.

제약 조건 저장소는 전류 치환 개념을 두 가지 방법으로 확장합니다.첫째, 그것은 리터럴을 절의 새로운 변형 선두와 동일시함으로써 파생된 제약조건뿐만 아니라 절 본문의 제약조건도 포함한다.둘째, 형태 제약만을 포함하는 것이 아닙니다.variable=value고려된 제약조건 언어에 대한 제약도 있습니다.정규 논리 프로그램의 성공적인 평가 결과가 최종 대체인 반면, 제약 논리 프로그램의 결과는 형식 변수=값의 제약을 포함할 수 있지만 일반적으로 임의 제약을 포함할 수 있는 최종 제약 저장소입니다.

도메인 고유의 제약조건은 구 본문 및 구 헤드와 리터럴을 동등하게 함으로써 제약조건 스토어에 도달할 수 있습니다.예를 들어 인터프리터가 리터럴을 다시 쓰는 경우A(X+2)새로운 변종 머리글을 가진 조항과 함께A(Y/2), 제약사항X+2=Y/2제약조건 저장소에 추가됩니다.변수가 실제 도메인 식 또는 유한 도메인 식에 나타나는 경우 해당 변수는 실제 도메인 또는 유한 도메인 값만 취할 수 있습니다.이러한 변수는 다른 용어에 적용되는 함수로 만든 항을 값으로 사용할 수 없습니다.변수가 특정 도메인의 값과 용어에 적용되는 함수의 값을 모두 취할 수밖에 없는 경우 제약 조건 저장소는 만족스럽지 않습니다.

제약조건 스토어에 제약조건을 추가한 후 제약조건 스토어에서 일부 작업이 수행됩니다.어떤 작업을 수행할지는 고려된 도메인과 제약 조건에 따라 달라집니다.예를 들어, 통일은 유한한 트리 등식, 실수에 대한 다항식 변수 제거, 유한한 도메인에 대한 국소 일관성의 형태를 강제하기 위한 제약 전파에 사용된다.이러한 작업은 제약 조건 저장소의 만족도를 보다 쉽게 확인하고 해결할 수 있도록 하기 위한 것입니다.

이러한 작업의 결과, 새로운 제약 조건을 추가하면 이전 제약 조건이 변경될 수 있습니다.역추적 시 인터프리터가 이러한 변경을 원래대로 되돌릴 수 있는 것이 중요합니다.가장 간단한 경우 방법은 인터프리터가 선택할 때마다 스토어의 완전한 상태를 저장하는 것입니다(목표를 다시 쓰는 절을 선택합니다).제약 조건 저장소를 이전 상태로 되돌릴 수 있는 보다 효율적인 방법이 있습니다.특히, 오래된 제약조건에 대한 변경을 포함하여 두 가지 선택 포인트 사이에서 이루어진 제약조건 스토어에 대한 변경 사항을 저장할 수 있습니다.이것은 변경된 제약조건의 오래된 값을 저장하는 것만으로 실행할 수 있습니다.이 방법을 후행이라고 합니다.더 고급 방법은 수정된 제약 조건에 대해 수행된 변경 사항을 저장하는 것입니다.예를 들어, 선형 제약 조건은 계수를 수정하여 변경됩니다. 즉, 이전 계수와 새 계수 간의 차이를 저장하면 변경 사항을 되돌릴 수 있습니다.이 두 번째 방법은 시멘틱 백트랙킹이라고 불리는데, 그 이유는 변경의 시멘틱이 오래된 버전의 제약 조건만 저장되기 때문입니다.

라벨링

라벨링 리터럴은 제약조건 저장소의 만족도 또는 부분 만족도를 확인하고 만족스러운 할당을 찾기 위해 유한 도메인에 걸친 변수에 사용됩니다.라벨링 리터럴은 다음 형식입니다.labeling([variables])여기서 인수는 유한 도메인에 걸친 변수 목록입니다.인터프리터는 이러한 리터럴을 평가할 때마다 리스트 변수 도메인에 대해 검색을 수행하여 관련된 모든 제약 조건을 충족하는 할당을 찾습니다.일반적으로 이것은 백트래킹 형식으로 이루어집니다.변수는 순서대로 평가되며 각 변수에 대해 가능한 모든 값을 시도하고 불일치가 검출되면 백트래킹합니다.

레이블 지정 리터럴의 첫 번째 용도는 제약 조건 저장소의 만족도 또는 부분 만족도를 실제로 확인하는 것입니다.인터프리터는 제약조건 저장소에 제약을 추가할 때 로컬 일관성 형식만 적용합니다.이 작업은 제약 조건 저장소가 만족스럽지 않더라도 불일치를 감지하지 못할 수 있습니다.변수 집합 위에 레이블 지정 리터럴을 지정하면 이러한 변수에 대한 제약 조건의 만족도가 검사됩니다.따라서 제약 조건 저장소에서 언급된 모든 변수를 사용하면 저장소의 만족도를 확인할 수 있습니다.

레이블 지정 리터럴의 두 번째 용도는 제약 조건 저장소를 충족하는 변수의 평가를 실제로 결정하는 것입니다.레이블 지정 리터럴이 없으면 제약 조건 저장소에 형식의 제약 조건이 포함된 경우에만 변수가 값이 할당됩니다.X=value로컬 일관성에 의해 변수의 도메인이 단일 값으로 감소하는 경우.일부 변수에 레이블 지정 리터럴을 지정하면 이러한 변수를 강제로 평가해야 합니다.즉, 레이블 지정 리터럴을 검토한 후에는 모든 변수에 값이 할당됩니다.

일반적으로 제약 로직 프로그램은 가능한 한 많은 제약이 제약 스토어에 누적된 후에만 라벨링 리터럴이 평가되는 방식으로 작성된다.이는 리터럴 레이블 지정이 검색을 강제하고 충족해야 할 제약 조건이 더 많을 경우 검색이 더 효율적이기 때문입니다.제약 만족 문제는 일반적으로 다음과 같은 구조를 가진 제약 로직 프로그램에 의해 해결된다.

풀다(X):-제약(X), 라벨링(X) 제약(X):- (모든. 제약 의 그 CSP)

통역사가 목표를 평가할 때solve(args)첫 번째 절의 새로운 변형 본문을 현재 목표에 배치합니다.첫 번째 목표는constraints(X')두 번째 절이 평가되고 이 연산은 현재 목표와 최종적으로 제약조건 저장소로 모든 제약조건을 이동합니다.문자 그대로labeling(X')그런 다음 평가하여 제약조건 저장소의 솔루션을 강제로 검색합니다.제약 조건 저장소에는 원래 제약 조건 만족 문제의 제약 조건이 정확히 포함되어 있으므로 이 작업은 원래 문제의 해결책을 검색합니다.

프로그램 리폼

소정의 제약논리 프로그램은 효율을 향상시키기 위해 재구성할 수 있다.첫 번째 규칙은 레이블이 지정된 리터럴에 대한 제약 조건이 제약 조건 저장소에 누적된 만큼 레이블이 지정된 리터럴에 배치되어야 한다는 것이다.이론상으로는A(X):-labeling(X),X>0와 동등하다A(X):-X>0,labeling(X)인터프리터가 라벨 리터럴을 검출했을 때 실행되는 검색은 제약조건을 포함하지 않는 제약조건 스토어에 있습니다.X>0그 결과, 다음과 같은 솔루션이 생성될 수 있습니다.X=-1이 제약조건을 충족하지 못하는 것으로 나중에 판명되었습니다.한편, 두 번째 공식에서는 제약조건이 이미 제약조건 저장소에 있는 경우에만 검색이 수행됩니다.따라서 검색은 추가 제약 조건이 검색 공간을 감소시킨다는 사실을 이용하여 일치하는 솔루션만 반환합니다.

효율성을 높일 수 있는 두 번째 개혁은 조항 본문에서 리터럴 앞에 제약을 두는 것이다.다시.A(X):-B(X),X>0그리고.A(X):-X>0,B(X)원칙적으로 동등합니다.그러나 첫 번째 방법은 더 많은 계산이 필요할 수 있습니다.예를 들어, 제약 조건 저장소에 제약 조건이 포함된 경우X<-2인터프리터는 재귀적으로 평가합니다.B(X)첫 번째 경우: 성공 시 제약조건 저장소가 일관성이 없다는 것을 알게 됩니다.X>0두 번째 경우, 그 절을 평가할 때, 통역자는 먼저 다음을 추가합니다.X>0제약 조건 저장소로 이동한 다음 가능한 한B(X). 의 추가 후 제약조건 스토어가 있기 때문에X>0일관성이 없는 것으로 판명되었습니다.재귀적 평가B(X)전혀 수행되지 않습니다.

효율성을 높일 수 있는 세 번째 개혁은 중복 제약 조건의 추가입니다.만약 프로그래머가 (어떤 수단을 통해서든) 문제의 해결책이 특정 제약조건을 충족한다는 것을 알고 있다면, 그들은 가능한 한 빨리 제약조건 저장소의 불일치를 야기하기 위해 그 제약조건을 포함할 수 있다.예를 들어, 사전에 알고 있는 경우, 그 평가는B(X)에 대해 양의 값을 얻을 수 있다X프로그래머는 다음과 같이 추가할 수 있습니다.X>0가 발생하기 전에B(X)예를 들면,A(X,Y):-B(X),C(X)목표에 실패하다A(-2,Z)단, 이것은 서브목표 평가 시에만 발견됩니다.B(X)한편, 상기 조항이 다음 조항으로 대체될 경우A(X,Y):-X>0,A(X),B(X)인터프리터는 제약이 있는 즉시 역추적합니다.X>0제약 스토어에 추가되며, 이는 평가 전에 발생합니다.B(X)짝수 시작.

제약 조건 처리 규칙

제약 조건 처리 규칙은 처음에 제약 조건 해결자를 지정하기 위한 독립형 형식주의로 정의되었고, 나중에 논리 프로그래밍에 포함되었습니다.제약조건 처리 규칙에는 2종류가 있습니다.첫 번째 종류의 규칙은 주어진 조건 하에서 일련의 제약조건이 다른 제약조건과 동등하다는 것을 명시한다.두 번째 종류의 규칙은 주어진 조건 하에서 일련의 제약이 다른 제약 조건을 의미함을 명시합니다.제약처리 규칙을 지원하는 제약논리 프로그래밍 언어에서 프로그래머는 제약스토어의 가능한 개서 및 제약스토어에 대한 가능한 추가사항을 특정하기 위해 이들 규칙을 사용할 수 있다.다음은 규칙의 예를 제시하겠습니다.

A(X) <=> B(X) C(X) A(X) ==> B(X) C(X)

첫 번째 규칙에 따르면B(X)스토어, 제약조건에 의해 부수됩니다.A(X)라고 고쳐 쓸 수 있다C(X)예를 들면,N*X>0라고 고쳐 쓸 수 있다X>0가게가 암시하고 있다면N>0. 기호<=>는 로직의 동등성과 유사하며 첫 번째 제약조건이 후자와 동등함을 나타냅니다.실제로 이는 첫 번째 제약조건을 후자로 대체할 수 있음을 의미합니다.

대신 두 번째 규칙은 중간에 있는 제약조건이 제약조건 저장소에 의해 부수되는 경우 후자의 제약조건이 첫 번째 제약조건의 결과임을 지정합니다.그 결과, 만약A(X)제약조건 스토어에 있습니다.B(X)제약조건 스토어에 의해 부가됩니다.C(X)스토어에 추가할 수 있습니다.동등성의 경우와 달리, 이것은 대체가 아닌 추가입니다.새로운 제약조건이 추가되지만 오래된 제약조건은 그대로 유지됩니다.

동등성은 일부 제약 조건을 단순한 제약 조건으로 대체함으로써 제약 조건 저장소를 단순화할 수 있습니다. 특히, 동등성 규칙에서 세 번째 제약 조건이 다음과 같은 경우true두 번째 제약조건이 추가되고 첫 번째 제약조건이 제약조건 저장소에서 삭제됩니다.추론은 제약조건 저장소의 불일치를 증명할 수 있는 새로운 제약조건을 추가할 수 있으며, 일반적으로 그 만족도를 확립하는 데 필요한 검색량을 줄일 수 있다.

제약사항 처리 규칙과 함께 논리 프로그래밍 절을 사용하여 제약조건 스토어의 만족도를 확립하는 방법을 지정할 수 있다.메서드의 다양한 선택지를 구현하기 위해 다른 구가 사용됩니다.또한 제약조건 처리 규칙은 실행 중 제약조건 스토어를 다시 쓰는 데 사용됩니다.예를 들어 유닛 전파에 의한 백트래킹을 이 방법으로 구현할 수 있습니다.허락하다holds(L)명제 절을 나타내며, 리스트의 리터럴은L평가된 순서와 동일합니다.이 알고리즘은 리터럴을 true 또는 false에 할당하는 것을 선택하는 구와 전파를 지정하는 제약조건 처리 규칙을 사용하여 구현할 수 있습니다.이 규칙들은 다음과 같이 규정하고 있다.holds([l L])만약 그렇다면 제거될 수 있다l=true스토어에서 팔로우하면, 라고 고쳐 쓸 수 있습니다.holds(L)한다면l=false스토어에서 팔로우합니다.유사하게,holds([l])대체할 수 있다l=true이 예에서 변수의 값 선택은 논리 프로그래밍의 절을 사용하여 구현되지만, 분리 제약 처리 규칙 또는^∨ CHR이라고 불리는 확장을 사용하여 제약 처리 규칙으로 인코딩될 수 있습니다.

상향식 평가

논리 프로그램의 평가의 표준 전략은 하향식이고 깊이 우선이다: 목표에서 많은 절이 목표를 증명할 수 있는 것으로 식별되며, 그 본문의 리터럴에 대한 재귀가 수행된다.대안 전략은 사실에서 시작하여 새로운 사실을 도출하기 위해 조항을 사용하는 것입니다. 이 전략은 상향식 전략이라고 불립니다.단일 목표를 증명하는 것이 아니라 특정 프로그램의 모든 결과를 생성하는 것이 목표일 경우 하향식보다 낫다고 간주한다.특히, 프로그램의 모든 결과를 표준 하향식 및 깊이 우선 방식으로 찾는 것은 상향식 평가 전략이 종료되는 동안 종료되지 않을 수 있다.

상향식 평가 전략은 평가 과정에서 지금까지 증명된 일련의 사실을 유지한다.이 세트는 처음에 비어 있습니다.각 단계에서 프로그램 조항을 기존 사실에 적용하여 새로운 사실을 도출하고 세트에 추가한다.예를 들어, 다음 프로그램의 상향식 평가에는 두 가지 단계가 필요합니다.

A(q). B(X):-A(X).

결과 집합은 처음에는 비어 있습니다.첫 번째 단계에서A(q)(비어있기 때문에) 본문을 증명할 수 있는 유일한 절입니다.A(q)따라서 현재의 결과 집합에 추가됩니다.두 번째 단계에서는A(q)증명된 두 번째 절을 사용할 수 있습니다.B(q)결과에 추가됩니다.다른 결과는 에서 증명될 수 없기 때문에{A(q),B(q)}, 실행이 종료됩니다.

하향식 평가보다 상향식 평가의 장점은 파생 사이클이 무한 루프를 생성하지 않는다는 것입니다.그 이유는 이미 그 결과를 포함하고 있는 현재의 결과 집합에 결과를 더해도 아무런 영향이 없기 때문이다.예를 들어, 위의 프로그램에 세 번째 절을 추가하면 하향식 평가에서 파생 사이클이 생성됩니다.

A(q). B(X):-A(X).A(X):-B(X)

예를 들어, 목표에 대한 모든 답을 평가하는 동안A(X)하향식 전략은 다음과 같은 파생 결과를 도출합니다.

A(q):-B(q), B(q):-A(q), A(q) A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q)

바꿔 말하면, 유일한 결과는A(q)먼저 생성되지만 알고리즘은 다른 답을 생성하지 않는 파생 모델에 대해 순환합니다.보다 일반적으로, 하향식 평가 전략은 가능한 파생상품(다른 파생상품이 존재하는 경우)에 걸쳐 순환할 수 있다.

상향식 전략은 이미 도출된 결과가 효과가 없기 때문에 동일한 단점을 가지고 있지 않다.위 프로그램에서는 상향식 전략이 추가되기 시작합니다.A(q)결과에 영향을 미치기 때문입니다. 두 번째 단계에서는B(X):-A(X)를 도출하는 데 사용됩니다.B(q)세 번째 단계에서, 현재의 결과로부터 도출할 수 있는 유일한 사실은 다음과 같다.A(q)그리고.B(q)그러나 이미 일련의 결과에 있습니다.그 결과 알고리즘이 정지됩니다.

위의 예에서 사용된 사실은 그라운드 리터럴뿐이었다.일반적으로 본문에 제약 조건만 있는 모든 절은 사실로 간주됩니다.예를 들어, 절은A(X):-X>0,X<10사실로 간주됩니다.이 확장된 사실의 정의를 위해, 일부 사실은 동일하지만 구문적으로는 동일하지 않을 수 있다.예를들면,A(q)와 동등하다A(X):-X=q그리고 둘 다 에 상당합니다.A(X):-X=Y, Y=q이 문제를 해결하기 위해, 사실들은 머리에 모든 다른 변수들의 태플을 포함하는 정상적인 형태로 변환된다. 두 개의 사실은 그들의 몸이 머리 변수들과 같다면, 즉, 이러한 변수들로 제한될 때 그들의 해법은 동일하다.

위에서 설명한 바와 같이 상향식 접근법은 이미 도출된 결과를 고려하지 않는다는 장점이 있다.그러나, 이러한 결과는 그 어느 것과도 동일하지 않지만 이미 도출된 결과들에 의해 수반되는 결과를 도출할 수 있다.예를 들어, 다음 프로그램의 보텀업 평가는 무한합니다.

A(0). A(X):-X>0. A(X):-X=Y+1, A(Y).

상향식 평가 알고리즘은 먼저 다음을 도출합니다.A(X)에 해당됩니다.X=0그리고.X>0두 번째 단계에서, 세 번째 절이 있는 첫 번째 사실은 다음 조항의 도출을 허용한다.A(1)세 번째 단계에서는A(2)파생되는 등하지만, 이러한 사실들은 이미 ...라는 사실에 의해 부수되었다.A(X)음이 아닌 모든 경우에 해당됩니다.X이 단점은 현재의 결과에 추가되는 수반 사실을 확인함으로써 극복할 수 있다.새 결과가 세트에 이미 포함되어 있으면 추가되지 않습니다.사실들은 절로 저장되기 때문에, 아마도 "로컬 변수"와 함께 저장되기 때문에, 그 머리들의 변수들에 대한 수반은 제한된다.

동시 제약 로직 프로그래밍

제약조건 논리 프로그래밍의 동시 버전은 제약조건 만족 문제를 해결하기보다는 동시 프로세스를 프로그래밍하는 것을 목적으로 합니다.제약 로직 프로그래밍의 목표는 동시에 평가되므로 동시 프로세스는 해석자에 의한 목표 평가로서 프로그래밍된다.

구문적으로 동시 제약 논리 프로그램은 비 동시 프로그램과 유사하지만, 유일한 예외는 절이 가드를 포함한다는 것입니다. 가드는 어떤 조건 하에서 절의 적용 가능성을 차단할 수 있는 제약 조건입니다.의미론적으로 동시 제약 논리 프로그래밍은 비동시 버전과 다릅니다. 왜냐하면 목표 평가는 문제에 대한 해결책을 찾는 것이 아니라 동시 프로세스를 실현하는 것을 목적으로 하기 때문입니다.특히 이 차이는 여러 절이 적용 가능한 경우의 인터프리터의 동작에 영향을 줍니다.비동시 제약 로직 프로그래밍은 모든 절을 재귀적으로 시도합니다.동시 제약 로직 프로그래밍은 1개만 선택합니다.이는 통역자가 의도한 방향성의 가장 명백한 효과이며, 이는 이전에 취했던 선택을 수정하지 않습니다.이것의 다른 효과로는 전체 평가가 실패하지 않는 동안 입증될 수 없는 목표를 갖는 의미론적 가능성, 그리고 목표와 절 헤드를 동등하게 하는 특별한 방법이 있다.

적용들

제약 로직 프로그래밍은 자동 스케줄링,^[1] 유형 추론,^[2] 토목 공학, 기계 공학, 디지털 회로 검증, 항공 교통 제어, 금융 ^{[citation needed]}등과 같은 많은 분야에 적용되어 왔습니다.

역사

제약 논리 프로그래밍은 1987년에 ^[3]Jaffar와 Lassez에 의해 도입되었습니다.그들은 Prolog II의 방정식과 질병이라는 용어가 제약의 특정 형태라는 관찰을 일반화했고, 이 아이디어를 임의의 제약 언어로 일반화했다.이 개념의 첫 번째 구현은 Prolog III, CLP(R) 및 ^{[citation needed]}CHIP입니다.

「」를 참조해 주세요.

레퍼런스

Dechter, Rina (2003). Constraint processing. Morgan Kaufmann. ISBN 1-55860-890-7. ISBN 1-55860-890-7
Apt, Krzysztof (2003). Principles of constraint programming. Cambridge University Press. ISBN 0-521-82583-0. ISBN 0-521-82583-0
Marriott, Kim; Peter J. Stuckey (1998). Programming with constraints: An introduction. MIT Press. ISBN 0-262-13341-5
Frühwirth, Thom; Slim Abdennadher (2003). Essentials of constraint programming. Springer. ISBN 3-540-67623-6. ISBN 3-540-67623-6
Jaffar, Joxan; Michael J. Maher (1994). "Constraint logic programming: a survey". Journal of Logic Programming. 19/20: 503–581. doi:10.1016/0743-1066(94)90033-7.
Colmerauer, Alain (1987). "Opening the Prolog III Universe". Byte. August.

레퍼런스

^ 아브덴나더, 슬림, 한스 슐렌커."제약 로직 프로그래밍을 사용한 간호사 스케줄링"AAAI/IAAI. 1999년
^ 마이클로프, 스피로, 그리고 프랭크 페닝이요"제약 논리 프로그래밍으로서의 고차 논리 프로그래밍." PPCP. Vol. 93. 1993.
^ Jaffar, Joxan, 그리고 J-L. Lassez."제한 로직 프로그래밍"제14회 프로그래밍 언어의 원리에 관한 ACM SIGACT-SIGPLAN 심포지엄의 진행.ACM, 1987.

[1] 아브덴나더, 슬림, 한스 슐렌커."제약 로직 프로그래밍을 사용한 간호사 스케줄링"AAAI/IAAI. 1999년

[2] 마이클로프, 스피로, 그리고 프랭크 페닝이요"제약 논리 프로그래밍으로서의 고차 논리 프로그래밍." PPCP. Vol. 93. 1993.

[3] Jaffar, Joxan, 그리고 J-L. Lassez."제한 로직 프로그래밍"제14회 프로그래밍 언어의 원리에 관한 ACM SIGACT-SIGPLAN 심포지엄의 진행.ACM, 1987.

[1]

[2]

[3]

Search

제약 로직 프로그래밍

네임스페이스

더

목차

개요

의미론

조건

트리 용어

리얼

유한 도메인

제약 조건 저장소

라벨링

프로그램 리폼

제약 조건 처리 규칙

상향식 평가

동시 제약 로직 프로그래밍

적용들

역사

「」를 참조해 주세요.

레퍼런스

레퍼런스

Search

제약 로직 프로그래밍

개요

의미론

조건

트리 용어

리얼

유한 도메인

제약 조건 저장소

라벨링

프로그램 리폼

제약 조건 처리 규칙

상향식 평가

동시 제약 로직 프로그래밍

적용들

역사

「 」를 참조해 주세요.

레퍼런스

레퍼런스

「」를 참조해 주세요.