初学者向けCHRの使い方まとめ/Constraint_Solver

例題目録 †

例題目録
boolean.pl
equations_gauss.pl
interval.pl
rationaltree.pl

boolean.pl †

コード

:- module(boolean, 
[boolean/1, and/3, or/3, xor/3, neg/2, imp/2, labeling/0, 
    half_adder/4, full_adder/5]).
:- use_module( library(chr)).

%% Deprecated syntax used for SICStus 3.x
%handler boolean.
%constraints boolean/1, and/3, or/3, xor/3, neg/2, imp/2, 
%   labeling/0, half_adder/4, full_adder/5.

%% Syntax for SWI / SICStus 4.x
:- chr_type bool ---> 0 ; 1.

:- chr_constraint
    boolean(?bool),
    and(?bool,?bool,?bool), 
    or(?bool,?bool,?bool), 
    xor(?bool,?bool,?bool),
    neg(?bool,?bool), 
    imp(?bool,?bool),
    labeling,
    half_adder(?bool,?bool,?bool,?bool),
    full_adder(?bool,?bool,?bool,?bool,?bool).


boolean(0) <=> true.
boolean(1) <=> true.

labeling \ boolean(A) <=> A=0 ; A=1.


%% and/3 specification
%%and(0,0,0).
%%and(0,1,0).
%%and(1,0,0).
%%and(1,1,1).

and(0,_,Y) <=> Y=0.
and(_,0,Y) <=> Y=0.
and(1,X,Y) <=> Y=X.
and(X,1,Y) <=> Y=X.
and(X,Y,1) <=> X=1,Y=1.
and(X,X,Z) <=> X=Z.
and(X,Y,A) \ and(X,Y,B) <=> A=B.
and(X,Y,A) \ and(Y,X,B) <=> A=B.

labeling \ and(A,B,C) <=> label_and(A,B,C).

label_and(0,_,0).
label_and(1,X,X).


%% or/3 specification
%%or(0,0,0).
%%or(0,1,1).
%%or(1,0,1).
%%or(1,1,1).

or(0,X,Y) <=> Y=X.
or(X,0,Y) <=> Y=X.
or(X,Y,0) <=> X=0,Y=0.
or(1,_,Y) <=> Y=1.
or(_,1,Y) <=> Y=1.
or(X,X,Z) <=> X=Z.
or(X,Y,A) \ or(X,Y,B) <=> A=B.
or(X,Y,A) \ or(Y,X,B) <=> A=B.

labeling \ or(A,B,C) <=> label_or(A,B,C).

label_or(0,X,X).
label_or(1,_,1).


%% xor/3 specification
%%xor(0,0,0).
%%xor(0,1,1).
%%xor(1,0,1).
%%xor(1,1,0).

xor(0,X,Y) <=> X=Y.
xor(X,0,Y) <=> X=Y.
xor(X,Y,0) <=> X=Y.
xor(1,X,Y) <=> neg(X,Y).
xor(X,1,Y) <=> neg(X,Y).
xor(X,Y,1) <=> neg(X,Y).
xor(X,X,Y) <=> Y=0.
xor(X,Y,X) <=> Y=0.
xor(Y,X,X) <=> Y=0.
xor(X,Y,A) \ xor(X,Y,B) <=> A=B.
xor(X,Y,A) \ xor(Y,X,B) <=> A=B.

labeling \ xor(A,B,C) <=> label_xor(A,B,C).

label_xor(0,X,X).
label_xor(1,X,Y) :- neg(X,Y).


%% neg/2 specification
%%neg(0,1).
%%neg(1,0).

neg(0,X) <=> X=1.
neg(X,0) <=> X=1.
neg(1,X) <=> X=0.
neg(X,1) <=> X=0.
neg(X,X) <=> fail.
neg(X,Y) \ neg(Y,Z) <=> X=Z.
neg(X,Y) \ neg(Z,Y) <=> X=Z.
neg(Y,X) \ neg(Y,Z) <=> X=Z.

%% Interaction with other boolean constraints
neg(X,Y) \ and(X,Y,Z) <=> Z=0.
neg(Y,X) \ and(X,Y,Z) <=> Z=0.
neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0.
neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0.
neg(X,Y) \ or(X,Y,Z) <=> Z=1.
neg(Y,X) \ or(X,Y,Z) <=> Z=1.
neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1.
neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1.
neg(X,Y) \ xor(X,Y,Z) <=> Z=1.
neg(Y,X) \ xor(X,Y,Z) <=> Z=1.
neg(X,Z) \ xor(X,Y,Z) <=> Y=1.
neg(Z,X) \ xor(X,Y,Z) <=> Y=1.
neg(Y,Z) \ xor(X,Y,Z) <=> X=1.
neg(Z,Y) \ xor(X,Y,Z) <=> X=1.
neg(X,Y) , imp(X,Y) <=> X=0,Y=1.
neg(Y,X) , imp(X,Y) <=> X=0,Y=1.

labeling \ neg(A,B) <=> label_neg(A,B).

label_neg(0,1).
label_neg(1,0).


%% imp/2 specification (implication)
%%imp(0,0).
%%imp(0,1).
%%imp(1,1).

imp(0,_) <=> true.
imp(X,0) <=> X=0.
imp(1,X) <=> X=1.
imp(_,1) <=> true.
imp(X,X) <=> true.
imp(X,Y),imp(Y,X) <=> X=Y.

labeling \ imp(A,B) <=> label_imp(A,B).

label_imp(0,_).
label_imp(1,1).


%% half_adder/4: add bits X and Y, result in S and carry in C
%% X+Y = S+2*C
half_adder(X,Y,S,C) <=>
    xor(X,Y,S), and(X,Y,C).


%% full_adder/5: add bits X, Y and Ci, result in S and carry in Co
%% X+Y+Ci = S+2*Co
full_adder(X,Y,Ci,S,Co) <=>
    half_adder(X,Y,S1,Co1), half_adder(Ci,S1,S,Co2), or(Co1,Co2,Co).

このプログラムは、各種の論理関数(boolean,and,or,xor,neg,imp,半加算器、全加算器)をシミュレートすることができ、入力に矛盾が無いことを確認しつつ、正しく解ける時の変数についての制約として得られたことを出力してくる。例えば

and(0,1,A), xor(1,1,B).

という入力に対しては、

and(0,_,A) <=> A=0.
xor(1,X,Y) <=> neg(X,Y).
neg(1,X) <=> X=0.

という3つのルールから

A=0, B=0.

という出力が得られる。

neg(A,A).

という入力に対しては、

neg(X,X) <=> fail.

というルールのみが発火するため

no.

という結果(解なし)が得られる。

また、

neg(A,B), or(A,B,C), labeling.

という制約を入力すれば、

labeling \ or(A,B,C) <=> label_or(A,B,C).

というルールで生成されたlabel_or制約が

label_or(0,X,X).
label_or(1,_,1).

という制約と矛盾しないように変数の値を選択されることになる。または、

neg(Y,X) \ or(X,Y,Z) <=> Z=1.

の記述によってor制約が消滅しC=1に変換される。

さらに、

labeling \ neg(A,B) <=> label_neg(A,B).
label_neg(0,1).
label_neg(1,0).

という規則及び公理(この名前の述語が合致しなければならない引数のパターン)も存在するため、結局出力は

A = 0, B = 1, C = 1, labeling.
A = 1, B = 0, C = 1, labeling.

の二通りになる。(SWI-prologはすべての解を網羅するため)

labeling制約がない場合、

neg(Y,X) \ or(X,Y,Z) <=> Z=1.

が発火したところで処理が止まり、

C = 1, neg(A,B).

を出力してくる。

↑

equations_gauss.pl †

コード

:- module(equations_gauss, [eq/2, {}/1]).
:- use_module(library(chr)).
:- use_module(library(lists)).
user:library_directory('.').
:- use_module(library(var_order)).

:- op(600,xfx,eq).

%% Deprecated syntax used for SICStus 3.x
%handler gauss.
%constraints eq/2, {}/1.

%% Syntax for SWI / SICStus 4.x
:- chr_constraint eq/2, {}/1.

%% Poly eq Const, where Poly is list of monomials Coefficient*Variable
%%    eq/2

%% curly brackets as wrapper to avoid name clash with built-in =
%%    {}/1   


%% split system of equations
split @     {E, F} <=> {E}, {F}.

%% convert arbitrary polynomial equation to eq-notation
normalize @ {A = B} <=> globalize([A-B]), 
    normpoly([A-B] eq 0, Poly eq Const), Poly eq Const.


%% 0=C
zero @      [] eq C <=> zero(C).

%% normalize first coefficient to 1
norm1 @     [A*X|P] eq C <=> notzero(A-1) | 
    multpoly(1/A,P eq C,P2 eq C2), [1*X|P2] eq C2.

%% const on left side (because of bound variable)
bound @     P eq C <=> select(A*X, P, P0), number(X) | C0 is C-A*X, P0 eq C0.

%% A*X = C  =>  bind variable
bind @      [A*X] eq C <=> var(X) | X is C/A.


%% Gaussian elimination 
elimate @   [A*X|P] eq C \ Q eq D <=>
    select(B*X, Q, Q1) |
    multpoly(-B/A, P eq C, E),
    addpoly(E, Q1 eq D, Q0 eq D0), 
    Q0 eq D0.


%% Auxiliary predicates

%% stable variable order based on chr/ordering by C. Holzbaur (var_order.pl)
%% compare variables with var_compare
ord_lss(X,Y) :- var_compare(<,X,Y).
%% otherwise use Prolog standard order
ord_lss(X,Y) :- nonvar(Y), X @< Y.


%% numerical stabilty
notzero(A) :- abs(A) >  0.000001.
zero(A)    :- abs(A) =< 0.000001.

%% safe_is(X,Exp): X is Exp; fails, if Exp is not an arith. expression
safe_is(X,Exp) :- on_exception(_, X is Exp, fail).


%% normalize polynomial equation
normpoly([X] eq C, [1*X] eq C) :- var(X), !.
normpoly([X] eq C, [1*X] eq C) :- simple(X), \+ number(X).
normpoly([A] eq C, [] eq C0) :- number(A), C0 is C-A.
normpoly([A,B|P] eq C, E0) :- 
    normpoly([A] eq 0,E1), normpoly([B|P] eq C,E2), addpoly(E1,E2,E0).
normpoly([+A] eq 0, E0) :- 
    normpoly([A] eq 0, E0).
normpoly([-A] eq 0, E0) :- 
    normpoly([A] eq 0, E1), multpoly(-1, E1, E0).
normpoly([A+B] eq C, E0) :- 
    normpoly([A] eq C,E), normpoly([B] eq 0,F), addpoly(E,F,E0).
normpoly([A-B] eq C, E0) :- normpoly([A] eq C,E), normpoly([B] eq 0,F),
    multpoly(-1,F,F1), addpoly(E,F1,E0).
normpoly([A*X] eq 0, E0) :-
    safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,E0).
normpoly([X*A] eq 0, E0) :-
    safe_is(A1,A), normpoly([X] eq 0, E), multpoly(A1,E,E0).
normpoly([X/A] eq 0, E0) :-
    safe_is(A1,1/A), normpoly([X] eq 0, E), multpoly(A1,E,E0).
normpoly([A] eq C, P0 eq C0) :- 
    C\==0, normpoly([A] eq 0, P0 eq C1), C0 is C+C1.


%% addpoly(E,F, E0): add polynomial equations
%% requires: polynomials ordered + duplicate free; retains properties
addpoly(P eq C, [] eq D, P eq C0) :- !, C0 is C+D.
addpoly([] eq C, Q eq D, Q eq C0) :- !, C0 is C+D.
addpoly([A*X|P] eq C, [B*Y|Q] eq D, E0) :- X==Y, !,
    A1 is A+B, addpoly(P eq C, Q eq D, P1 eq C1),
    (zero(A1) -> E0 = P1 eq C1 ; E0 = [A1*X|P1] eq C1).
addpoly([A*X|P] eq C, [B*Y|Q] eq D, [A*X|P0] eq C0) :- ord_lss(X,Y), !,
    addpoly(P eq C, [B*Y|Q] eq D, P0 eq C0).
addpoly([A*X|P] eq C, [B*Y|Q] eq D, [B*Y|P0] eq C0) :- ord_lss(Y,X), !,
    addpoly([A*X|P] eq C, Q eq D, P0 eq C0).
   
%% multpoly(M,E, E0): multiply polynomial equation with scalar
multpoly(M, [] eq C, [] eq C0) :- C0 is M*C. 
multpoly(M, [A*X|P] eq C, E0) :- 
    A1 is M*A, multpoly(M,P eq C,P1 eq C1),
    (zero(A1) -> E0 = P1 eq C1 ; E0 = [A1*X|P1] eq C1).

こちらはガウスの消去法により連立一次方程式を解くSolverである。

%% Auxiliary predicates

以降の記述はSWI-prologの述語(CHRで言う伝播規則のような動作をするルールのような何か、とにかく別言語の記法)であり、このSolverはPrologの動作に大きく依存している。ここで行う動作解説はCHRに関するものであり、また動作もPrologの知識に属するものなため、Auxilliary predicatesの内容(AP)による変化は結果を簡単に記述する以外は説明しない。興味がある場合は自分でprologの勉強をしてほしい。

入力例1として、

{2+2*X+4*Y+2*Z=0, 4+2*X+4*Y+4*Z=0, 1+2*X+3*Z=0}.

を与える。この入力はまず、splitルールによって

{2+2*X+4*Y+2*Z=0},
{4+2*X+4*Y+4*Z=0},
{1+2*X+3*Z=0}.

と変換される。その後、normalizeルール及びAPによって

[2*X,4*Y,2*Z] eq -2,
[2*X,4*Y,4*Z] eq -4,
[2*X,3*Z] eq -1.

となり、eliminateルールとAPによって

[2*X,4*Y,2*Z] eq -2,
[2*Z] eq -2,
[2*X,3*Z] eq -1.

に変換されて、bindルール及びprologのライブラリにあるis/2 (第一引数が第二引数と等しいとtrue)により、Z = -1.0で束縛される。制約は

[2*X,4*Y,2*Z] eq -2,
[2*X,3*Z] eq-1.

となり、boundルールによってZ項は右辺に移項され、

[2*X,4*Y] eq 0,
[2*X] eq 2.

となる。再びbindルール及びboundルールが発火して、X=1.0で束縛されるとともに、制約が

[4*Y] eq -2.

となる。当然これもbindルールで変換され、Y=-0.5で束縛される。結果、束縛された変数である

X=1.0, Y=-0.5, Z=-1.0.

が解として出力される。このようにしてこのSolverは連立一次方程式を解く。

↑

interval.pl †

コード

:- module(interval, [(::)/2, le/2, eq/2, ne/2, add/3, mult/3, int/1, bool/1, 
    split0/1, split/1, label/1]).
:- use_module( library(chr)).

% for domain constraints
:- op( 700,xfx,'::').
:- op( 600,xfx,':').
% for inequality constraints
:- op( 700,xfx,le).
:- op( 700,xfx,ne).
:- op( 700,xfx,eq). 

%% Deprecated syntax used for SICStus 3.x
%handler interval.
%constraints 

%% Syntax for SWI / SICStus 4.x
:- chr_constraint

% X::Min:Max - X is between the numbers Min and Max, inclusively
% X must always be an unbound variable(!), and Min and Max evaluable
% (i.e. ground) arithmetic expressions (or numbers)
    (::)/2, 
    le/2, eq/2, ne/2, add/3, mult/3,
% int(X) says that X is an integer (default is a real)
    int/1,
% bool(X) says that X is a boolean (default is a real)
    bool/1,

    split0/1,
    split/1,
    label/1,    % repeated split/1

    browse/1.   % watch how domain of X evolves


% Auxiliary -----------------------------------

browse(X), X::A:B ==> write((X::A:B)),nl.

% define the smallest intervals you want to get:
% the smaller, the more precise, the longer the computation
small(A:B) :- A+2.0e-05>=B. 

% is zero part of A:B ?
withzero(A:B) :- A=<0, 0=<B.


% Intersection  -------------------------------

redundant @ X::A:B \ X::C:D <=>
        (C=<A, B=<D ; A<B,small(A:B), C<D,small(C:D)) | true.

intersect @ X::A:B , X::C:D <=>
        X::max(A,C):min(B,D).


% Special Cases  -------------------------------

failure @ _::A:B <=> A>B | fail.

compute @ X::A:B <=> \+ (number(A),number(B)) | C is A, D is B, X::C:D.

integer @ int(X), X::A:B ==> \+ (integer(A),integer(B)) | 
      C is integer(ceiling(A)), D is integer(floor(B)), X::C:D.

bool @ bool(X), X::_:B ==> B<1 | X::0:0.
bool @ bool(X), X::A:_ ==> A>0 | X::1:1.
bool @ bool(X) ==> X::0:1.


% Inequality -------------------------------

(le) @ X le Y, X::A:_, Y::_:D ==> Y::A:D, X::A:D.
(eq) @ X eq Y, X::A:B, Y::C:D ==> Y::A:B, X::C:D.
(ne) @ X ne Y, X::A:A, Y::A:A <=> fail.

(ne_int) @ int(X) \ X ne Y, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ X ne Y, X::A:B <=> B=Y | X::A:B-1.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> A=Y | X::A+1:B.
(ne_int) @ int(X) \ Y ne X, X::A:B <=> B=Y | X::A:B-1.


% Addition X+Y=Z -------------------------------

add @ add(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
        X::E-D:F-C, Y::E-B:F-A, Z::A+C:B+D.


% Multiplication X*Y=Z -------------------------------

mult_z @ mult(X,Y,Z), X::A:B, Y::C:D ==> 
         M1 is A*C, M2 is A*D, M3 is B*C, M4 is B*D,
         Z::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),max(M3,M4)).

mult_y @ mult(X,Y,Z), X::A:B, Z::E:F ==>
         \+ withzero(A:B) |
         M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
         Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),max(M3,M4)).
mult_x @ mult(Y,X,Z), X::A:B, Z::E:F ==>
         \+ withzero(A:B) |
         M1 is E/A, M2 is E/B, M3 is F/A, M4 is F/B,
         Y::min(min(M1,M2),min(M3,M4)):max(max(M1,M2),max(M3,M4)).

mult_xyz @ mult(X,Y,Z), X::A:B, Y::C:D, Z::E:F ==>
         withzero(A:B), withzero(C:D), \+ withzero(E:F) |
         (A*C<E -> D>0, X::E/D:B ; true),
         (B*D<E -> C<0, X::A:E/C ; true),
         (F<A*D -> C<0, X::F/C:B ; true),
         (F<B*C -> D>0, X::A:F/D ; true).


% Labeling --------------------------------------------------------

label @ split0(X), X::A:B <=> \+ small(A:B), A<0,0<B |
           (X::A:0 ; X::0:B). 

label @ split(X), X::A:B <=> \+ small(A:B) |
           Half is (A+B)/2,
           (X::A:Half ; X::Half:B).

label @ label(X), X::A:B <=> \+ small(A:B) |
           Half is (A+B)/2,
           (X::A:Half ; X::Half:B), 
           label(X).

これは数値に幅のある整数または実数の変数を扱うSolverである。例えば、1~3まであり得るXと2~4まであり得るYの和X+Yは3~7まであり得るというような計算を処理することになる。以下、入力例とその場合の動作である。

input
X::3:5, X::2:4.

intersectルールにより、二つの制約は X::max(3,2):min(5,4) 則ち X::3:4 に書き換えられ出力される。

input
X le Y, X::3:5, Y::2:4.

le/2はless or equalを表す制約で、X=<Yの意味になる。今回は伝播規則(le)が発火して、

Y::3:4, X::3:4

という制約が新たに生成される。ここでintersectルールまたはrebundantルールが発火し、

X::3:4, X::3:5

という制約は

X::3:4

に書き換えられる。また、

Y::3:4, Y::2:4

という制約も同じ2つのルールのどちらかによって

Y::3:4

に書き換えられる。従って出力は

X le Y, X::3:4, Y::3:4

となる。

input
add(X,Y,Z), X::2:5, Y::3:4, Z::1:7

addは X+Y=Z の関係を表す制約である。

この入力に対しては伝播規則addが発火し、

X::1-4:7-3, Y::1-5:7-2, Z::2+3:4+5

則ち

X:: -3:4, Y:: -4:5, Z::5:9

という制約を生成する。これが元々あった制約群と合わせてintersectルールまたはrebundantルールによって X::2:4, Y::3:4, Z::5:7 となる。数値が変化したためもう一度addルールは発火するが、結局intersectルールまたはrebundantルールが発火して生成された制約は消去される。これ以上は伝播規則の性質によりaddルールは発火しない。従って出力は add(X,Y,Z), X::2:4, Y::3:4, Z::5:7 となる。

mult(X,Y,Z), X:: -2:3, Y:: -3:4, Z:: -12: -9.

multはX*Y=Zの関係を表す制約である。半角スペースが入っているのは - が :: と結合して違う名前の制約扱いされないようにである。

この入力に対して4つの伝播規則mult_z, mult_y, mult_xが一度ずつ発火する。 mult_zにより、

M1=-2*-3=6, M2=-2*4=-8, M3=3*-3=-9, M4=3*4=12

を使って

Z:: -9:12

が生成され、 mult_yにより、

M1=-12/-2=6, M2=-12/3=-4, M3=-9/-2=4.5, M4=-9/3=-3

を使って

Y:: -4:6

が生成され、 mult_xにより、

M1=-12/-3=4, M2=-12/4=-3, M3=-9/-3=3, M4=-9/4=-2.25

を使って

X:: -3: 4

が生成される。 mult_xyzはwithzero制約がないので発火しない。ここからintersectルールまたはrebundantルールによって、

X:: -2:3, X:: -3:4,
Y:: -3:4, Y:: -4:6,
Z:: -12: -9, Z:: -9:12,

という制約は

X:: -2:3, Y:: -3:4, Z:: -9: -9

に単純化される。これが出力となる。

input
A::(-3):3, B::(-3):3, C::4:4, mult(A,B,C), A eq B, label(A).

label/1はprologのライブラリにある述語でもあり、引数に与えられた変数に何か値が代入されていればtrueとなる。

3番目のlabelルールにより、Aの範囲は上限・下限の平均値でわけたどちらかから選択される。また、(eq)ルールとintersectまたはrebundantルールが実行されればBの範囲はAに合わせられることになる。その前後でmult(A,B,C)が発火し、結果Cが4を含まない範囲であるという制約が生成されればバックトラックが発生してAの範囲を選び直すことになる。それを繰り返してでA,Bの範囲が狭まっていく。これだけだと無限ループになるが、ある程度範囲が狭くなると述語

small(A:B) :- A+2.0e-05>=B

が成功し、3番目のlabelルールが発火しなくなって止まる。具体的に何回繰り返しているかは不明確なのでここでは省略する。

↑

rationaltree.pl †

コード

:- module(rationaltree, [(~)/2, (#~)/2, neq_list/2, label/0]).
:- use_module(library(chr)).
:- use_module(library(lists)).
user:library_directory('.').
:- use_module(library(var_order)).    % need stable order on variables

:- op(700,xfx,(~)).
:- op(700,xfx,(#~)).

%% Deprecated syntax used for SICStus 3.x
%handler rationaltree.
%constraints (~)/2, (#~)/2, eq_list/2, neq_list/2, label/0.

%% Syntax for SWI / SICStus 4.x
:- chr_constraint (~)/2, (#~)/2, eq_list/2, neq_list/2, label/0.

% T1 ~ T2 means: term T1 is syntactically equal to term T2
% T1 #~ T2 means: term T1 is syntactically different from term T2


eq_globalize        @ T1 ~ T2   ==> var_order:globalize(T1), var_order:globalize(T2).
neq_globalize       @ T1 #~ T2  ==> var_order:globalize(T1), var_order:globalize (T2).


eq_reflexivity      @ X ~ X     <=> true.
eq_orientation      @ T ~ X     <=> var(X), lss(X,T) | X ~ T.   
eq_decomposition    @ T1 ~ T2   <=> nonvar(T1),nonvar(T2) | 
                                    same_functions(T1,T2).
eq_confrontation    @ X ~ T1 \ X ~ T2   <=> var(X), lss(X,T1), leq(T1,T2) | 
                                            T1 ~ T2.


neq_reflexivity     @ X #~ X    <=> fail.
neq_orientation     @ T #~ X    <=> var(X), lss(X,T) | X #~ T. 
neq_decomposition   @ T1 #~ T2  <=> nonvar(T1), nonvar(T2) | 
                                    different_functions(T1,T2).
neq_confrontation   @ X ~ T1 \ X #~ T2  <=> T1 #~ T2. 


% two same-length lists must be equal, 
% i.e., every pair of elements must be equal
eq_list([],[])                <=> true.
eq_list([X|L1],[Y|L2])        <=> X ~ Y, eq_list(L1,L2).

% two same-length lists must not be equal, 
% i.e., at least one pair of elements must be different
neq_list([],[])               <=> fail.
neq_list([X],[Y])             <=> X #~ Y.
neq_list([X|L1],[X|L2])       <=> neq_list(L1,L2).
neq_list([X|L1],[Y|L2]), X~Y  <=> neq_list(L1,L2).

% label
label \ neq_list([X|L1],[Y|L2])#Id <=> true |  
                    (X #~ Y ; X ~ Y, neq_list(L1,L2))
                    pragma passive(Id).


%% Auxiliary

% lss(X,Y): X is smaller than Y by term-size order
lss(X,Y) :- var(X),var(Y), var_order:var_compare(<,X,Y).      % stable var order
lss(X,Y) :- var(X),nonvar(Y).
lss(X,Y) :- nonvar(X),nonvar(Y), termsize(X,M),termsize(Y,N),M<N.

% leq(X,Y): X is smaller-eq than Y by term-size order
leq(X,Y) :- \+ lss(Y,X).


% functions must be equal
same_functions(T1,T2) :-
    T1=..[F|L1], T2=..[F|L2], same_length(L1,L2), eq_list(L1,L2).

% functions must be different
different_functions(T1,T2) :-
    T1=..[F|L1], T2=..[F|L2], same_length(L1,L2), !, neq_list(L1,L2).
different_functions(_,_).

% termsize
termsize_list([],0).
termsize_list([X|L],N) :- termsize(X,N1), termsize_list(L,N2), N is N1+N2.
termsize(X,0) :- var(X).
termsize(T,1) :- atom(T).
termsize(T,N) :- compound(T), T=..L, termsize_list(L,N).

このコードは、「RationalTree?」の同一性、筆者が読んだ限りでは関数を引数に取る関数を木構造として見た場合に二つの関数が同じ構造をしているかどうか、を解くSolverである。関数の名前が同じで、引数の数と、その引数が同じ構造の関数または変数であれば同じ構造と判定される。以下入力と動作の例。

入力

f(X,b)~f(a,Y).

「~」は二つの関数が同じ構造であることを示す制約である。 eq_globalizeルールによって変数にid属性(順序付けのための性質)が付けられた後、eq_decompositionルールによって

f(X,b)~f(a,Y).

は

same_functions(T1,T2).

に変換され、prolog述語によって関数名を先頭、引数が後に続くリストに成形したT1,T2についてリストの引数部分L1,L2の長さが同じであることと、eq_list(L1,L2)制約を満たすという条件を要求される。 eq_list(L1,L2)制約の判定は

eq_list([],[]) <=> true.
eq_list([X|L1],[Y|L2]) <=> X~Y, eq_list(L1,L2).

の二つのルールで定義されていて、各変数について X~Y であることを要求している。これについては

eq_reflexivity @ X~X <=> true.

というルールが存在し、それによって判定される。入力中の変数X,Yについてもこれを満たすように束縛が行われ、

X~a, Y~b.

が出力される。

入力

f(a,b)~f(X).

に対しては、上と同様の流れでsame_functions(f(a,b),f(X))の述語に辿り着き、

same_length([a,b],[X])がfailしてnoを出力される。

入力

X~f(X), X~f(f(X)).

に対しては、eq_confrontationルールが発火して

X~f(X), f(X)~f(f(X)).

と変換され、eq_decomposition,same_functions及びeq_listルールにより

X~f(X), X~f(X).

となる。これがさらにeq_confrontationルールにより、

X~f(X), f(X)~f(X).

となった上で、eq_decomposition,same_functions,eq_list,eq_reflexivityルールによりf(X)~f(X)はtrueとなるため、出力は

X~f(X).

となる。

入力

f(a,X,c)#~f(a,b,Y), X#~Y, label.

に対しては、関数は変数でないため、 neq_decompositionルールが発火。

different_functions(f(a,X,c),f(a,b,Y)), X#~Y, label.

からprolog記述を経由して

neq_list([a,X,c],[a,b,Y]), X#~Y, label.

となる。 neq_listに関する規則とeq_reflexivityルールにより、

neq_list([X,c],[b,Y]), X#~Y, label.

となったところで

label \ neq_list([X|L1],[Y|L2])#Id <=> true | (X#~Y ; X~Y, neq_list(L1,L2))
pragma passive(Id).

の記述(pragma以下はprologの記述と思われるが詳細不明、とにかく重要なのはCHRルールの部分)により、X#~Y, または X~Y,neq_list(L1,L2) 制約が生成される。X#~Y、今回はYにbが入っているので X#~b が生成された場合にはそこで処理が終わり、

label, X#~b, X#~Y.

が出力され、別解を探させるとバックトラックしX#~bではなく X~b, neq_list([c],[Y]) を生成する。ここから、

neq_list([c],[Y]), X#~Y, X~b, label.
X#~Y, X~b, c#~Y, label.

となった後、neq_orientationルールにより、

X#~Y, X~b, Y#~c, label.

そしてneq_confrontationルールにより

b#~Y, X~b, Y#~c, label.

もう一度のneq_orientationルールにより

Y#~b, Y#~c, X~b, label.

という解を出力して解を網羅し終わる。

初学者向けCHRの使い方まとめ/Constraint_Solver

最新の20件

例題目録 †

boolean.pl †

equations_gauss.pl †

interval.pl †

rationaltree.pl †