/////////////// This is the input file for Sudoku (9 times 9) ///////



////下記の数独の問題は、L1-L15 は、IQナンプレ300 Vol.4, タイムインターメディア著/////、学研出版からとったものです。L16とL17は、インカーラ博士の作成した「世界で
////一番難しい数独////の2010年度版と2012年度版です。




//// the clues of L1 -L17 /////

L1:=[a12+e4,a17+e9,a18+e3,a21+e7,a29+e4,a31+e8,a34+e7,a35+e5,a44+e9,a46+e8,a47+e7,a53+e3,a57+e6,a63+e6,a64+e5,a66+e2,a75+e2,a76+e3,a79+e6,a81+e4,a89+e5,a92+e2,a93+e1,a98+e4];

L2:=[a15+e7,a24+e2,a27+e8,a33+e3,a36+e5,a38+e4,a42+e7,a45+e8,a47+e4,
a51+e8,a54+e4,a55+e9,a56+e7,a59+e1,a63+e5,a65+e1,a68+e3,a72+e4,a74+e8,a77+e5,a83+e2,a86+e9,a95+e3];

L3:=[a11+e1,a17+e6,a25+e9,a26+e2,a34+e3,a39+e1,a44+e9,a49+e2,
a52+e5,a53+e6,a57+e4,a58+e8,a61+e8,a66+e3,a71+e4,a76+e6,a84+e2,a85+e8,a93+e9,a99+e3];

L4:=[a13+e4,a22+e8,a26+e4,a31+e2,a35+e3,a37+e6,a44+e8,a48+e2,
a53+e5,a57+e3,a62+e6,a66+e9,a71+e8,a75+e2,a79+e6,a84+e5,a88+e4,a93+e1,a97+e5];

L5:=[a14+e7,a18+e1,a19+e8,a23+e8,a26+e1,a29+e3,a32+e5,a37+e9,a48+e4,
a51+e7,a55+e8,a59+e1,a62+e4,a73+e1,a78+e2,a81+e2,a84+e9,a87+e5,a91+e4,a92+e7,a96+e3];

L6:=[a16+e2,a18+e7,a19+e5,a25+e4,a29+e6,a39+e9,a43+e9,a44+e6,
a53+e6,a57+e4,a66+e8,a67+e1,a71+e8,a81+e7,a85+e9,a91+e1,a92+e2,a94+e3];

L7:=[a16+e3,a18+e7,a27+e1,a31+e6,a33+e9,a38+e4,a42+e3,a46+e5,
a51+e4,a55+e7,a59+e9,a64+e9,a68+e2,a72+e5,a77+e3,a79+e8,a83+e2,a92+e7,a94+e6];

L8:=[a11+e3,a18+e1,a25+e8,a26+e6,a29+e4,a36+e4,a42+e4,a43+e8,
a52+e7,a58+e3,a67+e2,a68+e9,a74+e5,a81+e9,a84+e1,a85+e2,a92+e6,a99+e7];

L9:=[a12+e9,a14+e4,a23+e4,a25+e1,a32+e5,a34+e6,a41+e2,a43+e6,
a52+e7,a54+e9,a56+e2,a58+e3,a67+e8,a69+e1,a76+e3,a78+e5,a85+e8,a87+e4,a96+e9,a98+e7];

L10:=[a14+e5,a17+e3,a23+e7,a26+e6,a29+e2,a35+e1,a38+e5,a42+e2,a47+e9,
a51+e8,a54+e9,a56+e4,a59+e6,a63+e1,a68+e3,a72+e7,a75+e3,a81+e4,a84+e1,a87+e8,a93+e6,a96+e2];

L11:=[a11+e8,a16+e3,a19+e9,a22+e5,a25+e2,a28+e7,a33+e6,a44+e9,a49+e4,
a52+e2,a55+e8,a58+e5,a61+e3,a66+e4,a77+e7,a82+e3,a85+e5,a88+e1,a91+e9,a94+e6,a99+e2];

L12:=[a14+e8,a19+e6,a22+e3,a23+e1,a24+e2,a32+e2,a37+e4,a41+e5,a42+e7,
a55+e6,a68+e8,a69+e9,a73+e4,a78+e7,a86+e3,a87+e1,a88+e2,a91+e6,a96+e5];

L13:=[a14+e7,a16+e1,a17+e8,a23+e3,a28+e4,a32+e5,a39+e1,a41+e2,a45+e3,a49+e8,
a54+e1,a55+e5,a56+e9,a61+e1,a65+e6,a69+e7,a71+e5,a78+e2,a82+e6,a87+e9,a93+e1,a94+e2,a96+e5];

L14:=[a11+e2,a13+e5,a17+e3,a19+e8,a22+e9,a34+e8,a36+e1,a42+e4,a45+e1,
a51+e7,a53+e1,a57+e8,a59+e2,a65+e4,a68+e7,a74+e3,a76+e6,a88+e6,a91+e8,a93+e3,a97+e7,a99+e5];

L15:=[a15+e5,a17+e4,a22+e2,a24+e4,a26+e6,a28+e1,a31+e9,a42+e3,a48+e9,
a51+e4,a55+e7,a59+e3,a62+e6,a68+e8,a79+e6,a82+e4,a84+e1,a86+e2,a88+e3,a93+e5,a95+e9];

L16:= [a13+e5,a14+e3,a21+e8,a28+e2,a32+e7,a35+e1,a37+e5,a41+e4,a46+e5,a47+e3,a52+e1,a55+e7,a59+e6,a63+e3,a64+e2,a68+e8,a72+e6,a74+e5,a79+e9,a83+e4,a88+e3,a96+e9,a97+e7];

L17 := [a11+e8,a23+e3,a24+e6,a32+e7,a35+e9,a37+e2,a42+e5,a46+e7,a55+e4,a56+e5,a57+e7,a64+e1,a68+e3,a73+e1,a78+e6,a79+e8,a83+e8,a84+e5,a88+e1,a92+e9,a97+e4];



///////////////////////////////////////////////////////
////// the Boolean equations for Sudoku /////////// 
///////////////////////////////////////////////////////////

E:= e1+e2+e3+e4+e5+e6+e7+e8+e9;

F:=[a11+a21+a31+a41+a51+a61+a71+a81+a91+E,a12+a22+a32+a42+a52+a62+a72+a82+a92+E,a13+a23+a33+a43+a53+a63+a73+a83+a93+E,
a14+a24+a34+a44+a54+a64+a74+a84+a94+E,a15+a25+a35+a45+a55+a65+a75+a85+a95+E,a16+a26+a36+a46+a56+a66+a76+a86+a96+E,
a17+a27+a37+a47+a57+a67+a77+a87+a97+E,a18+a28+a38+a48+a58+a68+a78+a88+a98+E,a19+a29+a39+a49+a59+a69+a79+a89+a99+E,

a11+a12+a13+a14+a15+a16+a17+a18+a19+E,a21+a22+a23+a24+a25+a26+a27+a28+a29+E,a31+a32+a33+a34+a35+a36+a37+a38+a39+E,
a41+a42+a43+a44+a45+a46+a47+a48+a49+E,a51+a52+a53+a54+a55+a56+a57+a58+a59+E,a61+a62+a63+a64+a65+a66+a67+a68+a69+E,
a71+a72+a73+a74+a75+a76+a77+a78+a79+E,a81+a82+a83+a84+a85+a86+a87+a88+a89+E,a91+a92+a93+a94+a95+a96+a97+a98+a99+E,

a11+a12+a13+a21+a22+a23+a31+a32+a33+E,a41+a42+a43+a51+a52+a53+a61+a62+a63+E,a71+a72+a73+a81+a82+a83+a91+a92+a93+E,

a14+a15+a16+a24+a25+a26+a34+a35+a36+E,a44+a45+a46+a54+a55+a56+a64+a65+a66+E,a74+a75+a76+a84+a85+a86+a94+a95+a96+E,

a17+a18+a19+a27+a28+a29+a37+a38+a39+E,a47+a48+a49+a57+a58+a59+a67+a68+a69+E,a77+a78+a79+a87+a88+a89+a97+a98+a99+E,

a11*a12,a11*a13,a11*a14,a11*a15,a11*a16,a11*a17,a11*a18,a11*a19,
a12*a13,a12*a14,a12*a15,a12*a16,a12*a17,a12*a18,a12*a19,
a13*a14,a13*a15,a13*a16,a13*a17,a13*a18,a13*a19,
a14*a15,a14*a16,a14*a17,a14*a18,a14*a19,
a15*a16,a15*a17,a15*a18,a15*a19,
a16*a17,a16*a18,a16*a19,
a17*a18,a17*a19,
a18*a19,

a21*a22,a21*a23,a21*a24,a21*a25,a21*a26,a21*a27,a21*a28,a21*a29,
a22*a23,a22*a24,a22*a25,a22*a26,a22*a27,a22*a28,a22*a29,
a23*a24,a23*a25,a23*a26,a23*a27,a23*a28,a23*a29,
a24*a25,a24*a26,a24*a27,a24*a28,a24*a29,
a25*a26,a25*a27,a25*a28,a25*a29,
a26*a27,a26*a28,a26*a29,
a27*a28,a27*a29,
a28*a29,

a31*a32,a31*a33,a31*a34,a31*a35,a31*a36,a31*a37,a31*a38,a31*a39,
a32*a33,a32*a34,a32*a35,a32*a36,a32*a37,a32*a38,a32*a39,
a33*a34,a33*a35,a33*a36,a33*a37,a33*a38,a33*a39,
a34*a35,a34*a36,a34*a37,a34*a38,a34*a39,
a35*a36,a35*a37,a35*a38,a35*a39,
a36*a37,a36*a38,a36*a39,
a37*a38,a37*a39,
a38*a39,

a41*a42,a41*a43,a41*a44,a41*a45,a41*a46,a41*a47,a41*a48,a41*a49,
a42*a43,a42*a44,a42*a45,a42*a46,a42*a47,a42*a48,a42*a49,
a43*a44,a43*a45,a43*a46,a43*a47,a43*a48,a43*a49,
a44*a45,a44*a46,a44*a47,a44*a48,a44*a49,
a45*a46,a45*a47,a45*a48,a45*a49,
a46*a47,a46*a48,a46*a49,
a47*a48,a47*a49,
a48*a49,

a51*a52,a51*a53,a51*a54,a51*a55,a51*a56,a51*a57,a51*a58,a51*a59,
a52*a53,a52*a54,a52*a55,a52*a56,a52*a57,a52*a58,a52*a59,
a53*a54,a53*a55,a53*a56,a53*a57,a53*a58,a53*a59,
a54*a55,a54*a56,a54*a57,a54*a58,a54*a59,
a55*a56,a55*a57,a55*a58,a55*a59,
a56*a57,a56*a58,a56*a59,
a57*a58,a57*a59,
a58*a59,

a61*a62,a61*a63,a61*a64,a61*a65,a61*a66,a61*a67,a61*a68,a61*a69,
a62*a63,a62*a64,a62*a65,a62*a66,a62*a67,a62*a68,a62*a69,
a63*a64,a63*a65,a63*a66,a63*a67,a63*a68,a63*a69,
a64*a65,a64*a66,a64*a67,a64*a68,a64*a69,
a65*a66,a65*a67,a65*a68,a65*a69,
a66*a67,a66*a68,a66*a69,
a67*a68,a67*a69,
a68*a69,

a71*a72,a71*a73,a71*a74,a71*a75,a71*a76,a71*a77,a71*a78,a71*a79,
a72*a73,a72*a74,a72*a75,a72*a76,a72*a77,a72*a78,a72*a79,
a73*a74,a73*a75,a73*a76,a73*a77,a73*a78,a73*a79,
a74*a75,a74*a76,a74*a77,a74*a78,a74*a79,
a75*a76,a75*a77,a75*a78,a75*a79,
a76*a77,a76*a78,a76*a79,
a77*a78,a77*a79,
a78*a79,

a81*a82,a81*a83,a81*a84,a81*a85,a81*a86,a81*a87,a81*a88,a81*a89,
a82*a83,a82*a84,a82*a85,a82*a86,a82*a87,a82*a88,a82*a89,
a83*a84,a83*a85,a83*a86,a83*a87,a83*a88,a83*a89,
a84*a85,a84*a86,a84*a87,a84*a88,a84*a89,
a85*a86,a85*a87,a85*a88,a85*a89,
a86*a87,a86*a88,a86*a89,
a87*a88,a87*a89,
a88*a89,

a91*a92,a91*a93,a91*a94,a91*a95,a91*a96,a91*a97,a91*a98,a91*a99,
a92*a93,a92*a94,a92*a95,a92*a96,a92*a97,a92*a98,a92*a99,
a93*a94,a93*a95,a93*a96,a93*a97,a93*a98,a93*a99,
a94*a95,a94*a96,a94*a97,a94*a98,a94*a99,
a95*a96,a95*a97,a95*a98,a95*a99,
a96*a97,a96*a98,a96*a99,
a97*a98,a97*a99,
a98*a99,


a11*a21,a11*a31,a11*a41,a11*a51,a11*a61,a11*a71,a11*a81,a11*a91,
a21*a31,a21*a41,a21*a51,a21*a61,a21*a71,a21*a81,a21*a91,
a31*a41,a31*a51,a31*a61,a31*a71,a31*a81,a31*a91,
a41*a51,a41*a61,a41*a71,a41*a81,a41*a91,
a51*a61,a51*a71,a51*a81,a51*a91,
a61*a71,a61*a81,a61*a91,
a71*a81,a71*a91,
a81*a91,

a12*a22,a12*a32,a12*a42,a12*a52,a12*a62,a12*a72,a12*a82,a12*a92,
a22*a32,a22*a42,a22*a52,a22*a62,a22*a72,a22*a82,a22*a92,
a32*a42,a32*a52,a32*a62,a32*a72,a32*a82,a32*a92,
a42*a52,a42*a62,a42*a72,a42*a82,a42*a92,
a52*a62,a52*a72,a52*a82,a52*a92,
a62*a72,a62*a82,a62*a92,
a72*a82,a72*a92,
a82*a92,

a13*a23,a13*a33,a13*a43,a13*a53,a13*a63,a13*a73,a13*a83,a13*a93,
a23*a33,a23*a43,a23*a53,a23*a63,a23*a73,a23*a83,a23*a93,
a33*a43,a33*a53,a33*a63,a33*a73,a33*a83,a33*a93,
a43*a53,a43*a63,a43*a73,a43*a83,a43*a93,
a53*a63,a53*a73,a53*a83,a53*a93,
a63*a73,a63*a83,a63*a93,
a73*a83,a73*a93,
a83*a93,

a14*a24,a14*a34,a14*a44,a14*a54,a14*a64,a14*a74,a14*a84,a14*a94,
a24*a34,a24*a44,a24*a54,a24*a64,a24*a74,a24*a84,a24*a94,
a34*a44,a34*a54,a34*a64,a34*a74,a34*a84,a34*a94,
a44*a54,a44*a64,a44*a74,a44*a84,a44*a94,
a54*a64,a54*a74,a54*a84,a54*a94,
a64*a74,a64*a84,a64*a94,
a74*a84,a74*a94,
a84*a94,

a15*a25,a15*a35,a15*a45,a15*a55,a15*a65,a15*a75,a15*a85,a15*a95,
a25*a35,a25*a45,a25*a55,a25*a65,a25*a75,a25*a85,a25*a95,
a35*a45,a35*a55,a35*a65,a35*a75,a35*a85,a35*a95,
a45*a55,a45*a65,a45*a75,a45*a85,a45*a95,
a55*a65,a55*a75,a55*a85,a55*a95,
a65*a75,a65*a85,a65*a95,
a75*a85,a75*a95,
a85*a95,

a16*a26,a16*a36,a16*a46,a16*a56,a16*a66,a16*a76,a16*a86,a16*a96,
a26*a36,a26*a46,a26*a56,a26*a66,a26*a76,a26*a86,a26*a96,
a36*a46,a36*a56,a36*a66,a36*a76,a36*a86,a36*a96,
a46*a56,a46*a66,a46*a76,a46*a86,a46*a96,
a56*a66,a56*a76,a56*a86,a56*a96,
a66*a76,a66*a86,a66*a96,
a76*a86,a76*a96,
a86*a96,

a17*a27,a17*a37,a17*a47,a17*a57,a17*a67,a17*a77,a17*a87,a17*a97,
a27*a37,a27*a47,a27*a57,a27*a67,a27*a77,a27*a87,a27*a97,
a37*a47,a37*a57,a37*a67,a37*a77,a37*a87,a37*a97,
a47*a57,a47*a67,a47*a77,a47*a87,a47*a97,
a57*a67,a57*a77,a57*a87,a57*a97,
a67*a77,a67*a87,a67*a97,
a77*a87,a77*a97,
a87*a97,

a18*a28,a18*a38,a18*a48,a18*a58,a18*a68,a18*a78,a18*a88,a18*a98,
a28*a38,a28*a48,a28*a58,a28*a68,a28*a78,a28*a88,a28*a98,
a38*a48,a38*a58,a38*a68,a38*a78,a38*a88,a38*a98,
a48*a58,a48*a68,a48*a78,a48*a88,a48*a98,
a58*a68,a58*a78,a58*a88,a58*a98,
a68*a78,a68*a88,a68*a98,
a78*a88,a78*a98,
a88*a98,

a19*a29,a19*a39,a19*a49,a19*a59,a19*a69,a19*a79,a19*a89,a19*a99,
a29*a39,a29*a49,a29*a59,a29*a69,a29*a79,a29*a89,a29*a99,
a39*a49,a39*a59,a39*a69,a39*a79,a39*a89,a39*a99,
a49*a59,a49*a69,a49*a79,a49*a89,a49*a99,
a59*a69,a59*a79,a59*a89,a59*a99,
a69*a79,a69*a89,a69*a99,
a79*a89,a79*a99,
a89*a99,

a11*a12,a11*a13,a11*a21,a11*a22,a11*a23,a11*a31,a11*a32,a11*a33,
a12*a13,a12*a21,a12*a22,a12*a23,a12*a31,a12*a32,a12*a33,
a13*a21,a13*a22,a13*a23,a13*a31,a13*a32,a13*a33,
a21*a22,a21*a23,a21*a31,a21*a32,a21*a33,
a22*a23,a22*a31,a22*a32,a22*a33,
a23*a31,a23*a32,a23*a33,
a31*a32,a31*a33,
a32*a33,

a41*a42,a41*a43,a41*a51,a41*a52,a41*a53,a41*a61,a41*a62,a41*a63,
a42*a43,a42*a51,a42*a52,a42*a53,a42*a61,a42*a62,a42*a63,
a43*a51,a43*a52,a43*a53,a43*a61,a43*a62,a43*a63,
a51*a52,a51*a53,a51*a61,a51*a62,a51*a63,
a52*a53,a52*a61,a52*a62,a52*a63,
a53*a61,a53*a62,a53*a63,
a61*a62,a61*a63,
a62*a63,

a71*a72,a71*a73,a71*a81,a71*a82,a71*a83,a71*a91,a71*a92,a71*a93,
a72*a73,a72*a81,a72*a82,a72*a83,a72*a91,a72*a92,a72*a93,
a73*a81,a73*a82,a73*a83,a73*a91,a73*a92,a73*a93,
a81*a82,a81*a83,a81*a91,a81*a92,a81*a93,
a82*a83,a82*a91,a82*a92,a82*a93,
a83*a91,a83*a92,a83*a93,
a91*a92,a91*a93,
a92*a93,

a14*a15,a14*a16,a14*a24,a14*a25,a14*a26,a14*a34,a14*a35,a14*a36,
a15*a16,a15*a24,a15*a25,a15*a26,a15*a34,a15*a35,a15*a36,
a16*a24,a16*a25,a16*a26,a16*a34,a16*a35,a16*a36,
a24*a25,a24*a26,a24*a34,a24*a35,a24*a36,
a25*a26,a25*a34,a25*a35,a25*a36,
a26*a34,a26*a35,a26*a36,
a34*a35,a34*a36,
a35*a36,

a44*a45,a44*a46,a44*a54,a44*a55,a44*a56,a44*a64,a44*a65,a44*a66,
a45*a46,a45*a54,a45*a55,a45*a56,a45*a64,a45*a65,a45*a66,
a46*a54,a46*a55,a46*a56,a46*a64,a46*a65,a46*a66,
a54*a55,a54*a56,a54*a64,a54*a65,a54*a66,
a55*a56,a55*a64,a55*a65,a55*a66,
a56*a64,a56*a65,a56*a66,
a64*a65,a64*a66,
a65*a66,

a74*a75,a74*a76,a74*a84,a74*a85,a74*a86,a74*a94,a74*a95,a74*a96,
a75*a76,a75*a84,a75*a85,a75*a86,a75*a94,a75*a95,a75*a96,
a76*a84,a76*a85,a76*a86,a76*a94,a76*a95,a76*a96,
a84*a85,a84*a86,a84*a94,a84*a95,a84*a96,
a85*a86,a85*a94,a85*a95,a85*a96,
a86*a94,a86*a95,a86*a96,
a94*a95,a94*a96,
a95*a96,

a17*a18,a17*a19,a17*a27,a17*a28,a17*a29,a17*a37,a17*a38,a17*a39,
a18*a19,a18*a27,a18*a28,a18*a29,a18*a37,a18*a38,a18*a39,
a19*a27,a19*a28,a19*a29,a19*a37,a19*a38,a19*a39,
a27*a28,a27*a29,a27*a37,a27*a38,a27*a39,
a28*a29,a28*a37,a28*a38,a28*a39,
a29*a37,a29*a38,a29*a39,
a37*a38,a37*a39,
a38*a39,

a47*a48,a47*a49,a47*a57,a47*a58,a47*a59,a47*a67,a47*a68,a47*a69,
a48*a49,a48*a57,a48*a58,a48*a59,a48*a67,a48*a68,a48*a69,
a49*a57,a49*a58,a49*a59,a49*a67,a49*a68,a49*a69,
a57*a58,a57*a59,a57*a67,a57*a68,a57*a69,
a58*a59,a58*a67,a58*a68,a58*a69,
a59*a67,a59*a68,a59*a69,
a67*a68,a67*a69,
a68*a69,

a77*a78,a77*a79,a77*a87,a77*a88,a77*a89,a77*a97,a77*a98,a77*a99,
a78*a79,a78*a87,a78*a88,a78*a89,a78*a97,a78*a98,a78*a99,
a79*a87,a79*a88,a79*a89,a79*a97,a79*a98,a79*a99,
a87*a88,a87*a89,a87*a97,a87*a98,a87*a99,
a88*a89,a88*a97,a88*a98,a88*a99,
a89*a97,a89*a98,a89*a99,
a97*a98,a97*a99,
a98*a99,


a11^2+a11,a12^2+a12,a13^2+a13,a14^2+a14,a15^2+a15,a16^2+a16,a17^2+a17,a18^2+a18,a19^2+a19,
a21^2+a21,a22^2+a22,a23^2+a23,a24^2+a24,a25^2+a25,a26^2+a26,a27^2+a27,a28^2+a28,a29^2+a29,
a31^2+a31,a32^2+a32,a33^2+a33,a34^2+a34,a35^2+a35,a36^2+a36,a37^2+a37,a38^2+a38,a39^2+a39,
a41^2+a41,a42^2+a42,a43^2+a43,a44^2+a44,a45^2+a45,a46^2+a46,a47^2+a47,a48^2+a48,a49^2+a49,
a51^2+a51,a52^2+a52,a53^2+a53,a54^2+a54,a55^2+a55,a56^2+a56,a57^2+a57,a58^2+a58,a59^2+a59,
a61^2+a61,a62^2+a62,a63^2+a63,a64^2+a64,a65^2+a65,a66^2+a66,a67^2+a67,a68^2+a68,a69^2+a69,
a71^2+a71,a72^2+a72,a73^2+a73,a74^2+a74,a75^2+a75,a76^2+a76,a77^2+a77,a78^2+a78,a79^2+a79,
a81^2+a81,a82^2+a82,a83^2+a83,a84^2+a84,a85^2+a85,a86^2+a86,a87^2+a87,a88^2+a88,a89^2+a89,
a91^2+a91,a92^2+a92,a93^2+a93,a94^2+a94,a95^2+a95,a96^2+a96,a97^2+a97,a98^2+a98,a99^2+a99
];

////////////////////////////////////////////////////////
/////////////////////////////////////////////////////////
//// clues + Boolean equations の登録

L1:= F cat L1;
L2:= F cat L2;
L3:= F cat L3;
L4:= F cat L4;
L5:= F cat L5;
L6:= F cat L6;
L7:= F cat L7;
L8:= F cat L8;
L9:= F cat L9;
L10:= F cat L10;
L11:= F cat L11;
L12:= F cat L12;
L13:= F cat L13;
L14:= F cat L14;
L15:= F cat L15;
L16:= F cat L16;
L17:= F cat L17;

//////////////////////////////////////////////////////
//////////////////////////////////////////////////////