もとの6けたの整数はいくつ？

※記法については『算数の問題文の記法のまとめ【随時更新】 - 算数の問題文の記法を考える』を読んでください。

【2000年度ジュニア算数オリンピックトライアル問題7問目】
　6けたの整数があり一の位の数字は9です。今、この「9」を一番上の位に移したら、もとの整数の4倍になりました。もとの6けたの整数はいくつですか。

【記法化】

Aは0から9の整数である;
Bは0から9の整数である;
Cは0から9の整数である;
Dは0から9の整数である;
Eは0から9の整数である;
(100000*A + 10000*B + 1000*C + 100*D + 10*E + 9) * 4 == 900000 + 10000*A + 1000*B + 100*C + 10*D + E;

print(100000*A + 10000*B + 1000*C + 100*D + 10*E + 9)

ちょっと普通の制約プログラミングで解けるか気になったのでCP-SAT ソルバー  |  OR-Tools  |  Google for Developersを参考にして試してみた。

from ortools.sat.python import cp_model

model = cp_model.CpModel()

num_vals = 10
A = model.new_int_var(0, num_vals - 1, "A")
B = model.new_int_var(0, num_vals - 1, "B")
C = model.new_int_var(0, num_vals - 1, "C")
D = model.new_int_var(0, num_vals - 1, "D")
E = model.new_int_var(0, num_vals - 1, "E")

model.add((100000*A + 10000*B + 1000*C + 100*D + 10*E + 9) * 4 == 900000 + 10000*A + 1000*B + 100*C + 10*D + E)

solver = cp_model.CpSolver()
status = solver.solve(model)

if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print(f"A = {solver.value(A)}")
    print(f"B = {solver.value(B)}")
    print(f"C = {solver.value(C)}")
    print(f"D = {solver.value(D)}")
    print(f"E = {solver.value(E)}")
else:
    print("No solution found.")

結果

A = 2
B = 3
C = 0
D = 7
E = 6

【工夫】
「ABCDE9 * 4 == 9ABCDE」なので、まず左辺の計算結果の下1ケタは6だと分かり、Eは6だと分かる。Eが分かれば下2ケタ目も求められるし、下2ケタ目が求められれば同じように下3ケタ目も求められる。そういうことが普通の制約プログラミングでできるか分からなかったのだけど、どうもできるらしいので工夫はいらないものと考える。