assign(domain_size, 9).
set(prolog_style_variables).

formulas(assumptions).

% 範囲の定義
all X (r1(X) <-> (X=1 | X=2 | X=3)).
all X (r2(X) <-> (X=4 | X=5 | X=6)).
all X (r3(X) <-> (X=7 | X=8 | X=0)).

% 任意の数が全ての行および列に存在する
all N all X exists Y (N=a(X,Y)) .
all N all Y exists X (N=a(X,Y)) .

% 任意の数が任意のブロックに存在する
all N (
(exists X exists Y (r1(X) & r1(Y) & N=a(X,Y))) &
(exists X exists Y (r1(X) & r2(Y) & N=a(X,Y))) &
(exists X exists Y (r1(X) & r3(Y) & N=a(X,Y))) &
(exists X exists Y (r2(X) & r1(Y) & N=a(X,Y))) &
(exists X exists Y (r2(X) & r2(Y) & N=a(X,Y))) &
(exists X exists Y (r2(X) & r3(Y) & N=a(X,Y))) &
(exists X exists Y (r3(X) & r1(Y) & N=a(X,Y))) &
(exists X exists Y (r3(X) & r2(Y) & N=a(X,Y))) &
(exists X exists Y (r3(X) & r3(Y) & N=a(X,Y)))
).

% 枝刈り用の規則
all X all Y all Z (a(X,Y)=a(X,Z) -> Y=Z) .
all X all Y all Z (a(X,Y)=a(Z,Y) -> X=Z) .
all X all Y all Z all W (
((r1(X) & r1(Y) & r1(Z) & r1(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r1(X) & r2(Y) & r1(Z) & r2(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r1(X) & r3(Y) & r1(Z) & r3(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r2(X) & r1(Y) & r2(Z) & r1(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r2(X) & r2(Y) & r2(Z) & r2(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r2(X) & r3(Y) & r2(Z) & r3(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r3(X) & r1(Y) & r3(Z) & r1(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r3(X) & r2(Y) & r3(Z) & r2(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W)) &
((r3(X) & r3(Y) & r3(Z) & r3(W) & a(X,Y)=a(Z,W)) -> (X=Z & Y=W))
).

% 既知の数字の定義
a(1,1)=1. a(1,4)=2. a(1,7)=3.
a(2,2)=2. a(2,5)=3. a(2,8)=4.
a(3,3)=3. a(3,6)=4. a(3,0)=5.
a(4,1)=6. a(4,4)=4. a(4,7)=5.
a(5,2)=7. a(5,5)=5. a(5,8)=6.
a(6,3)=8. a(6,6)=6. a(6,0)=7.
a(7,1)=8. a(7,4)=0. a(7,7)=7.
a(8,2)=0. a(8,5)=1. a(8,8)=8.
a(0,3)=1. a(0,6)=2. a(0,0)=4.

end_of_list.