ジュニア算数オリンピックにおけるユークリッド幾何学の問題の解答の自動化を模索している。まず三角形定理ループを回し、回答できなかったら1ステップの作図を試していって、それらで回答できるか探る。それでも駄目だったら2ステップ、3ステップと増やしていく。交点の確認はこの方法を使う。
『右の図の四角形ABCDと四角形EFCGは合同な平行四辺形で、辺EGを延長した線は点Dを通り、辺CBを延長した線は点Eを通ります。
このとき、角BACの[ア]倍と角CADの[イ]倍の和は180度となります。
[ア]、[イ]に入る整数をそれぞれ答えなさい。
』
前回の続き。最近は自動化におけるデータの移り変わりを手作業でやってみている。
初期入力はできるだけ、graph、adjacent_angle_lst(名称を元に戻した)、の2つから立ち上げて、cluster_lstはどの程度必要なのか探っていきたい。まあもちろん、それ以外にも何と何がイコールかだとか、今回だと平行線を登録する必要があるわけだが、主眼はそこのつもりだ。
名付けられていない交点を、上からH、Iと名付ける。
graph := [ A : [ [[B, I], []], [[C, H], []], [[D], []] ] , B : [ [[A, I], []], [[C], [E]] ] , C : [ [[A, H], []], [[B, E], []], [[D], []], [[F], []], [[G], []] ] , D : [ [[A], []], [[C], []], [[E, G, H, I], []] ] , E : [ [[B, C], []], [[D, G, H, I], []], [[F], []] ] , F : [ [[C], []], [[E], []] ] , G : [ [[C], []], [[D], [E, H, I]] ] , H : [ [[A], [C]], [[D, G], [E, I]] ] , I : [ [[A], [B]], [[D, G, H], [E]] ] ]; adjacent_angle_lst := [ #[0] + [1] == [2]。隣接を足し算で表現してみた [BAC_p, CAD_p, BAD_p], #平行四辺形だからポジティブと判断できる、がそれも自動化すべきなのか? [BAC_p, BAD_n, CAD_n], [CAD_p, BAD_n, BAC_n], [ABE_p, ABC_p, CBE_h], [ABE_p, CBE_h, ABC_n], [ABC_p, CBE_h, ABE_n], [ACB_p, ACG_p, BCG_p], [ACG_p, DCG_p, ACD_p], [DCG_p, DCF_1, FCG_n], [DCF_1, BCF_p, BCD_n], [BCF_p, ACB_p, ACF_p], [BCG_p, DCG_p, BCD_p], [BCG_p, BCF_p, FCG_p], [ACD_p, DCF_1, ACF_n], [ACD_p, ACB_p, BCD_p], [FCG_n, ACG_p, ACF_n], [FCG_n, BCF_p, BCG_n], [BCD_n, DCG_p, BCG_n], [BCD_n, ACB_p, ACD_n], [ACF_p, ACG_p, FCG_p], [ACF_p, DCF_1, ACD_n], [BCG_p, FCG_n, BCF_n], [BCG_p, BCD_n, DCG_n], [ACD_p, BCD_n, ACB_n], [ACD_p, ACF_p, DCF_2], [FCG_n, ACF_p, ACG_n], [FCG_n, BCG_p, BCF_n], [BCD_n, BCG_p, DCG_n], [BCD_n, ACD_p, ACB_n], [ACF_p, FCG_n, ACG_n], [ACF_p, ACD_p, DCF_p], ~~~~~~~~~~~~~~~~ ];
いや駄目だ。どんなに論理的に正しくても、入力したくない。どうにかグラフから自動化しよう。
…そもそも、隣り合うとは何だろうか。辺と辺を1本の辺で共有するだけで無く、もう一方側の点と点の関係も問わなければいけないのではないか。
もう一方側の点と点で三角形を作って、その頂点が、隣り合っていると言われる二つの角の和になった時に、初めて隣り合っていると言えるのではないか。
クラスターも、ネガティブなものは考えないようにしよう。クラスターの、ネガティブな辺と辺を貼り合わせるというのは、問題としてありそうにない。
一方で、クラスターは拡大でなく、やはり平面的に貼り合わせていると考えることにしよう。1角が90°以上の三角形の角同士を貼り合わせる必要がある問題は、いかにもありそうだ。その時に、角の和がそれぞれ180°以下だったら、クラスターとして登録する。
graph → triangle_lst → cluster_lst、という順番で展開していこう。
この問題においては、平行線を登録しておけば、それだけで平行四辺形の分はクラスタとして登録される。それで結果的に、この問題の角の和は弾き出すことができる。
直線を二分した場合は、そのまま角の和として登録しよう。また、1辺を共有する三角形同士が、もう一方の点・共有する辺の底辺側の点・もう一方の点、という風に直線で繋がっている時にも、クラスタや角の和として登録しよう。
じゃあ一回やってみようかな。
graph := [ A : [ [[B, I], []], [[C, H], []], [[D], []] ] , B : [ [[A, I], []], [[C], [E]] ] , C : [ [[A, H], []], [[B, E], []], [[D], []], [[F], []], [[G], []] ] , D : [ [[A], []], [[C], []], [[E, G, H, I], []] ] , E : [ [[B, C], []], [[D, G, H, I], []], [[F], []] ] , F : [ [[C], []], [[E], []] ] , G : [ [[C], []], [[D], [E, H, I]] ] , H : [ [[A], [C]], [[D, G], [E, I]] ] , I : [ [[A], [B]], [[D, G, H], [E]] ] ]; triangle_lst := [ ]; cluster_lst := [ ]; parallel_lines_lst := [ #どうやって表現しようかな。ADとCE、ABとCD、DEとCF、EFとCG、なんだけど。例えば。 [[A, D], [E, B, C]], [[A, I, B], [D, C]], [[D, G, H, I, E], [C, F]], [[E, F], [G, C]] ]; always { AD == BC; AB == CD; BAD_p == BCD_p; ADC_p == ABC_p; EG == CF; EF == CG; DEF_p == FCG_p; CGE_p == CFE_p; AD == EG; #やや手抜き EF == AB; BAD_p == DEF_p; ADC_p == CGE_p; }
ここからスタート。で、triangle_lstを更新。ある点と繋がっている点が更に別の繋がっている点と繋がっているか。
点に着目して対頂角でのイコールを登録。点に着目して辺の和も登録。
graph := [ A : [ [[B, I], []], [[C, H], []], [[D], []] ] , B : [ [[A, I], []], [[C], [E]] ] , C : [ [[A, H], []], [[B, E], []], [[D], []], [[F], []], [[G], []] ] , D : [ [[A], []], [[C], []], [[E, G, H, I], []] ] , E : [ [[B, C], []], [[D, G, H, I], []], [[F], []] ] , F : [ [[C], []], [[E], []] ] , G : [ [[C], []], [[D], [E, H, I]] ] , H : [ [[A], [C]], [[D, G], [E, I]] ] , I : [ [[A], [B]], [[D, G, H], [E]] ] ]; triangle_lst := [ △ABC : [BAC_p, AB, ABC_p, BC, ACB_p, AC], △ADI : [BAD_p, AD, ADE_p, DI, AID_p, AI], △AHI : [ABC_p, AH, AHE_p, HI, AID_p, AI], △ACD : [CAD_p, AC, ACD_p, CD, ADC_p, AD], △ADH : [CAD_p, AD, ADE_p, DH, AHD_p, AH], △BEI : [ABE_p, BE, BED_p, EI, BIE_p, BI], △CDH : [ACD_p, CD, CDE_p, DH, CHD_p, CH], △CGH : [BCG_p, CG, CGE_p, GH, CHD_p, CH], △CEH : [ACB_p, CE, BED_p, EH, CHE_p, CH], △CDE : [BCD_p, CD, CDE_p, DE, BED_p, CE], △CEG : [BCG_p, CE, BED_p, EG, CGE_p, CG], △CEF : [BCF_p, CE, BEF_p, EF, CFE_p, CF], △CDG : [DCG_p, CD, CDE_p, DG, CGD_p, CG] ]; cluster_lst := [ ]; parallel_lines_lst := [ #どうやって表現しようかな。ADとCE、ABとCD、DEとCF、EFとCG、なんだけど。例えば。 [[A, D], [E, B, C]], [[A, I, B], [D, C]], [[D, G, H, I, E], [C, F]], [[E, F], [G, C]] ]; always { AD == BC; AB == CD; BAD_p == BCD_p; ADC_p == ABC_p; EG == CF; EF == CG; DEF_p == FCG_p; CGE_p == CFE_p; AD == EG; #やや手抜き EF == AB; BAD_p == DEF_p; ADC_p == CGE_p; AHD_p == CHE_p; AHE_p == CHD_p; AID_p == BIE_p; AIE_p == BID_p; BC + BE == CE; DG + EG == DE; DG + GH == DH; DG + GI == DI; AH + CH == AC; DH + EH == DE; DH + HI == DI; GH + EH == EG; GH + HI == GI; AI + BI == AB; DI + EI == DE; GI + EI == EG; HI + EI == EH; }
平行線のセットの一方を一つ一つ確認して、何とか更新。クラスターもついでに更新した。
graph := [ A : [ [[B, I], []], [[C, H], []], [[D], []] ] , B : [ [[A, I], []], [[C], [E]] ] , C : [ [[A, H], []], [[B, E], []], [[D], []], [[F], []], [[G], []] ] , D : [ [[A], []], [[C], []], [[E, G, H, I], []] ] , E : [ [[B, C], []], [[D, G, H, I], []], [[F], []] ] , F : [ [[C], []], [[E], []] ] , G : [ [[C], []], [[D], [E, H, I]] ] , H : [ [[A], [C]], [[D, G], [E, I]] ] , I : [ [[A], [B]], [[D, G, H], [E]] ] ]; triangle_lst := [ △ABC : [BAC_p, AB, ABC_p, BC, ACB_p, AC], △ADI : [BAD_p, AD, ADE_p, DI, AID_p, AI], △AHI : [ABC_p, AH, AHE_p, HI, AID_p, AI], △ACD : [CAD_p, AC, ACD_p, CD, ADC_p, AD], △ADH : [CAD_p, AD, ADE_p, DH, AHD_p, AH], △BEI : [ABE_p, BE, BED_p, EI, BIE_p, BI], △CDH : [ACD_p, CD, CDE_p, DH, CHD_p, CH], △CGH : [BCG_p, CG, CGE_p, GH, CHD_p, CH], △CEH : [ACB_p, CE, BED_p, EH, CHE_p, CH], △CDE : [BCD_p, CD, CDE_p, DE, BED_p, CE], △CEG : [BCG_p, CE, BED_p, EG, CGE_p, CG], △CEF : [BCF_p, CE, BEF_p, EF, CFE_p, CF], △CDG : [DCG_p, CD, CDE_p, DG, CGD_p, CG] ]; cluster_lst := [ [[A, B, C], [BAC_p, AB, ABC_p, BC, ACB_p, AC]], [[A, D, I], [BAD_p, AD, ADE_p, DI, AID_p, AI]], [[A, H, I], [ABC_p, AH, AHE_p, HI, AID_p, AI]], [[A, C, D], [CAD_p, AC, ACD_p, CD, ADC_p, AD]], [[A, D, H], [CAD_p, AD, ADE_p, DH, AHD_p, AH]], [[B, E, I], [ABE_p, BE, BED_p, EI, BIE_p, BI]], [[C, D, H], [ACD_p, CD, CDE_p, DH, CHD_p, CH]], [[C, G, H], [BCG_p, CG, CGE_p, GH, CHD_p, CH]], [[C, E, H], [ACB_p, CE, BED_p, EH, CHE_p, CH]], [[C, D, E], [BCD_p, CD, CDE_p, DE, BED_p, CE]], [[C, E, G], [BCG_p, CE, BED_p, EG, CGE_p, CG]], [[C, E, F], [BCF_p, CE, BEF_p, EF, CFE_p, CF]], [[C, D, G], [DCG_p, CD, CDE_p, DG, CGD_p, CG]] ]; parallel_lines_lst := [ #どうやって表現しようかな。ADとCE、ABとCD、DEとCF、EFとCG、なんだけど。例えば。 [[A, D], [E, B, C]], [[A, I, B], [D, C]], [[D, G, H, I, E], [C, F]], [[E, F], [G, C]] ]; always { AD == BC; AB == CD; BAD_p == BCD_p; ADC_p == ABC_p; EG == CF; EF == CG; DEF_p == FCG_p; CGE_p == CFE_p; AD == EG; #やや手抜き EF == AB; BAD_p == DEF_p; ADC_p == CGE_p; AHD_p == CHE_p; AHE == CHD_p; AID_p == BIE_p; AIE_p == BID_p; BC + BE == CE; DG + EG == DE; DG + GH == DH; DG + GI == DI; AH + CH == AC; DH + EH == DE; DH + HI == DI; GH + EH == EG; GH + HI == GI; AI + BI == AB; DI + EI == DE; GI + EI == EG; HI + EI == EH; BAD_p == ABE_p; CAD_p == ACB_p; ADE_p == BED_p; BAC_p == ACD_p; AID_p == CDE_p; BIE_p == CDE_p; ABE_p == BCD_p; CGD_p == GCF_p; CHD_p == ACF_p; AHE_p == ACF_p; CED_p == ECF_p; DEF_p == CGD_p; CEF_p == BCG_p; }
ここまでは予定通りで、このまま三角形定理ループを回すこともできる。ただ問題はここからで、角の和を弾き出す必要がある。
まず、点に着目して、辺にそのまま辺が当たっていて、足したら180°になるような分かれ方をしているのを探す。
あと、三角形に着目して外角による足し算も更新していく。
更には、これがメインなわけだが、2点を共有しているような三角形で、そうじゃない点同士が共有しているどちらか1点を挟んで直線だったら、共有しているもう一方の点の角の和を登録していく。
graph := [ A : [ [[B, I], []], [[C, H], []], [[D], []] ] , B : [ [[A, I], []], [[C], [E]] ] , C : [ [[A, H], []], [[B, E], []], [[D], []], [[F], []], [[G], []] ] , D : [ [[A], []], [[C], []], [[E, G, H, I], []] ] , E : [ [[B, C], []], [[D, G, H, I], []], [[F], []] ] , F : [ [[C], []], [[E], []] ] , G : [ [[C], []], [[D], [E, H, I]] ] , H : [ [[A], [C]], [[D, G], [E, I]] ] , I : [ [[A], [B]], [[D, G, H], [E]] ] ]; triangle_lst := [ △ABC : [BAC_p, AB, ABC_p, BC, ACB_p, AC], △ADI : [BAD_p, AD, ADE_p, DI, AID_p, AI], △AHI : [BAC_p, AH, AHE_p, HI, AID_p, AI], △ACD : [CAD_p, AC, ACD_p, CD, ADC_p, AD], △ADH : [CAD_p, AD, ADE_p, DH, AHD_p, AH], △BEI : [ABE_p, BE, BED_p, EI, BIE_p, BI], △CDH : [ACD_p, CD, CDE_p, DH, CHD_p, CH], △CGH : [BCG_p, CG, CGE_p, GH, CHD_p, CH], △CEH : [ACB_p, CE, BED_p, EH, CHE_p, CH], △CDE : [BCD_p, CD, CDE_p, DE, BED_p, CE], △CEG : [BCG_p, CE, BED_p, EG, CGE_p, CG], △CEF : [BCF_p, CE, BEF_p, EF, CFE_p, CF], △CDG : [DCG_p, CD, CDE_p, DG, CGD_p, CG] ]; cluster_lst := [ [[A, B, C], [BAC_p, AB, ABC_p, BC, ACB_p, AC]], [[A, D, I], [BAD_p, AD, ADE_p, DI, AID_p, AI]], [[A, H, I], [ABC_p, AH, AHE_p, HI, AID_p, AI]], [[A, C, D], [CAD_p, AC, ACD_p, CD, ADC_p, AD]], [[A, D, H], [CAD_p, AD, ADE_p, DH, AHD_p, AH]], [[B, E, I], [ABE_p, BE, BED_p, EI, BIE_p, BI]], [[C, D, H], [ACD_p, CD, CDE_p, DH, CHD_p, CH]], [[C, G, H], [BCG_p, CG, CGE_p, GH, CHD_p, CH]], [[C, E, H], [ACB_p, CE, BED_p, EH, CHE_p, CH]], [[C, D, E], [BCD_p, CD, CDE_p, DE, BED_p, CE]], [[C, E, G], [BCG_p, CE, BED_p, EG, CGE_p, CG]], [[C, E, F], [BCF_p, CE, BEF_p, EF, CFE_p, CF]], [[C, D, G], [DCG_p, CD, CDE_p, DG, CGD_p, CG]] ]; parallel_lines_lst := [ #どうやって表現しようかな。ADとCE、ABとCD、DEとCF、EFとCG、なんだけど。例えば。 [[A, D], [E, B, C]], [[A, I, B], [D, C]], [[D, G, H, I, E], [C, F]], [[E, F], [G, C]] ]; always { AD == BC; AB == CD; BAD_p == BCD_p; ADC_p == ABC_p; EG == CF; EF == CG; DEF_p == FCG_p; CGE_p == CFE_p; AD == EG; #やや手抜き EF == AB; BAD_p == DEF_p; ADC_p == CGE_p; AHD_p == CHE_p; AHE == CHD_p; AID_p == BIE_p; AIE_p == BID_p; BC + BE == CE; DG + EG == DE; DG + GH == DH; DG + GI == DI; AH + CH == AC; DH + EH == DE; DH + HI == DI; GH + EH == EG; GH + HI == GI; AI + BI == AB; DI + EI == DE; GI + EI == EG; HI + EI == EH; BAD_p == ABE_p; CAD_p == ACB_p; ADE_p == BED_p; BAC_p == ACD_p; AID_p == CDE_p; BIE_p == CDE_p; ABE_p == BCD_p; CGD_p == GCF_p; CHD_p == ACF_p; AHE_p == ACF_p; CED_p == ECF_p; DEF_p == CGD_p; CEF_p == BCG_p; ABC_p + ABE_p == 180; CGD_p + CGE_p == 180; AHD_p + AHE_p == 180; AID_p + AIE_p == 180; BAC_p + ACB_p == ABE_p; BAD_p + ADE_p == AIE_p; BAD_p + ADE_p == BID_p; #同じ角に二つある場合は対頂角なので次回からは省く BAC_p + AID_p == AHD_p; BAC_p + AHE_p == AIE_p; CAD_p + ADE_p == AHE_p; BED_p + BIE_p == ABC_p; ABE_p + BED_p == AIE_p; ACD_p + CDE_p == CHE_p; ACG_p + CHD_p == CGD_p; ACG_p + CGE_p == AHD_p; ACB_p + BED_p == CHD_p; BCG_p + BED_p == CGD_p; DCG_p + CDE_p == CGE_p; DCG_p + BCG_p == ACD_p; #CDG, CGH DCG_p + BCG_p == BCD_p; #CDG, CEG ADH_p + CDH_p == ADC_p; #ADH, CDH DCH_p + ECH_p == BCD_p; #CDH, CEH CAD_p + BAC_p == BAD_p; #ADH, AHI BCG_p + ACB_p == ACG_p; #CGH, CEH }
いや大変だった。今振り返ると、辺の和に着目したら良かったのかな?
で、こうなって一つ一つ見てみると、点Fが絡む角の和が登録されていないことが分かる。
まず、GとFに辺を引く作画をする。そうすると、例えば角DEF全体が錯角だとかで180-CFEだと分かる。で、まあその角があるような三角形CEFを見ると、180-角CFEの残りの2角が、錯角だとかでDEFを構成する2つの角だと分かる。
クラスタ同士で辺を共有するものを探し、更に頂点同士でもう一対のクラスタも探し、角の和が頂点と頂点の角と同じになっているような、かな?
更に、DとFに辺を引く作画をする。
…これは、まずDが一つ前のクラスタの外側にあることは分かる。直線で伸ばしているので外側だし、そちら側は180°なので、クラスタとしての条件はクリアしている。
問題は逆側で、どう考えれば良いのかなあ。どちら側も180°だったら四角形になってしまうので、という説明では駄目だろうか。どちらかが180°だったら、繋げるのが三角形だったら180°以下だ。
そうすると、クラスタの拡大に成功して、DからFは角を割っているし、CからGも角を割っていて、しかもクラスタの順番的に交点が発生して、みたいな感じ。
しかし、今回は良かったけど、意外と足し算として成立させるのは難しいのかもしれないな。
いや、今回は、CDGFにおいて、三角形CDGと三角形CFG(順番は対応しておらず)は相似形で、角CGF + 角DFG == 角CDF + 角DCG == を仮に?1としてみる。あと、?1 + 相似形の底辺2角 == 180。
そうすると、元々CGD == FCGで、角DCGが?1 - 角CDFなので、って感じで行けないだろうか。無理だろうか。