Given: // 数の定義 type int N = {1..9} // 既知のマスを表す三項関係の宣言 G (N,N,N) Find: // 求める解の宣言 A (N,N) : N Declare: // 述語の宣言 R1 (N) R2 (N) R3 (N) Satisfying: // 範囲の定義 { R1(n) <- n=1 | n=2 | n=3. } { R2(n) <- n=4 | n=5 | n=6. } { R3(n) <- n=7 | n=8 | n=9. } // 全ての数が全ての行,列,ブロックに存在する ! n x : ? y : n=A(x,y) . ! n y : ? x : n=A(x,y) . ! n : (? x y : R1(x) & R1(y) & n=A(x,y)) & (? x y : R1(x) & R2(y) & n=A(x,y)) & (? x y : R1(x) & R3(y) & n=A(x,y)) & (? x y : R2(x) & R1(y) & n=A(x,y)) & (? x y : R2(x) & R2(y) & n=A(x,y)) & (? x y : R2(x) & R3(y) & n=A(x,y)) & (? x y : R3(x) & R1(y) & n=A(x,y)) & (? x y : R3(x) & R2(y) & n=A(x,y)) & (? x y : R3(x) & R3(y) & n=A(x,y)) . // 既知のマスはそのまま ! x y n : G(x,y,n) => A(x,y)=n . // 枝刈り用の規則 ! x y z : A(x,y)=A(x,z) => y=z . ! x y z : A(x,y)=A(z,y) => x=z . ! x y z 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)) . Data: // 既知のマスの具体的なデータ G = { 1,1,1; 1,4,2; 1,7,3; 2,2,2; 2,5,3; 2,8,4; 3,3,3; 3,6,4; 3,9,5; 4,1,6; 4,4,4; 4,7,5; 5,2,7; 5,5,5; 5,8,6; 6,3,8; 6,6,6; 6,9,7; 7,1,8; 7,4,9; 7,7,7; 8,2,9; 8,5,1; 8,8,8; 9,3,1; 9,6,2; 9,9,4; }