世界一美しい覆面算を制約ソルバーで解く

「世界一美しい覆面算はこれだ（と思う）」というWebページを見つけたので，制約ソルバーのCreamとSugarで解いてみた．

リンク

• 世界一美しい覆面算はこれだ（と思う）
• Cream
• Sugar
• パズルをSugar制約ソルバーで解く
• プログラム不要の「制約プログラミング手習い」

Creamのプログラム

JavaのクラスライブラリであるCreamを用いたプログラムは，以下のようになる．

import jp.ac.kobe_u.cs.cream.DefaultSolver;
import jp.ac.kobe_u.cs.cream.IntVariable;
import jp.ac.kobe_u.cs.cream.Network;
import jp.ac.kobe_u.cs.cream.NotEquals;
import jp.ac.kobe_u.cs.cream.Solution;
import jp.ac.kobe_u.cs.cream.Solver;

public class CryptArithm1 {

    private static IntVariable n(IntVariable x, IntVariable y) {
        return x.multiply(10).add(y);
    }
    
    public static void main(String[] args) {
        Network net = new Network();
        IntVariable a = new IntVariable(net, 1, 9, "a");
        IntVariable b = new IntVariable(net, 1, 9, "b");
        IntVariable c = new IntVariable(net, 1, 9, "c");
        IntVariable d = new IntVariable(net, 1, 9, "d");
        IntVariable e = new IntVariable(net, 1, 9, "e");
        IntVariable f = new IntVariable(net, 1, 9, "f");
        IntVariable g = new IntVariable(net, 1, 9, "g");
        IntVariable h = new IntVariable(net, 1, 9, "h");
        IntVariable i = new IntVariable(net, 1, 9, "i");
        new NotEquals(net, new IntVariable[] {a,b,c,d,e,f,g,h,i} );
        // AB * C = FG
        n(a,b).multiply(c).equals(n(f,g));
        // DE - FG = HI
        n(d,e).subtract(n(f,g)).equals(n(h,i));
        Solver solver = new DefaultSolver(net);
        for (solver.start(); solver.waitNext(); solver.resume()) {
            Solution solution = solver.getSolution();
            System.out.println(solution);
        }
        solver.stop();
    }
}

実行結果

a=1,b=7,c=4,d=9,e=3,f=6,g=8,h=2,i=5,v1=10,v2=10,v3=17,v4=90,v5=10,v6=93,v7=60,v8=10,v9=68,v10=20,v11=10,v12=25,v13=68,v14=25

実行結果は以下のようになったので元の問題の答え(唯一解)は以下の通りだとわかる．

       4
  17 )--
      93
      68
     ---
      25

Sugarの制約モデル

Sugarの制約モデル言語で記述したモデルは，以下のようになる．

(int a 1 9)
(int b 1 9)
(int c 1 9)
(int d 1 9)
(int e 1 9)
(int f 1 9)
(int g 1 9)
(int h 1 9)
(int i 1 9)
(alldifferent a b c d e f g h i)
(int ab 0 99)
(int de 0 99)
(int fg 0 99)
(int hi 0 99)
(= ab (+ (* 10 a) b))
(= de (+ (* 10 d) e))
(= fg (+ (* 10 f) g))
(= hi (+ (* 10 h) i))
(= (* ab c) fg)
(= (- de fg) hi)

実行結果

s SATISFIABLE
a a	1
a b	7
a c	4
a d	9
a e	3
a f	6
a g	8
a h	2
a i	5
a ab	17
a de	93
a fg	68
a hi	25
a