ヒビルテ(2013-04-02)

2013-04-02 [長年日記]

λ. 「異様に難しいドラクエの謎解き」を整数線形計画問題として解く

「異様に難しいドラクエの謎解き」をモデル検査器で解くの続き。元の「人生を振り返る - 異様に難しいドラクエの謎解き」に「押す順番はどうでも良くて、四隅のボタンを押す回数の問題でしたね」とあって、この洞察を使えば整数線形計画問題として定式化して、もっとスマートに解けるなぁ、と思った。

整数線形計画問題による定式化

x1, x2, x3, x4 をそれぞれ左上、右上、右下、左下の石を押す回数とすると、最短の手順を求める問題は、以下の最適化問題として定式化できる。

Minimize
  x1 + x2 + x3 + x4
Subject To
  3 + x1 + x2 + x3 ≡ 0 mod 4  (左の像の条件)
  3 + x2 + x3 + x4 ≡ 0 mod 4  (上の像の条件)
      x3 + x4 + x1 ≡ 0 mod 4  (右の像の条件)
      x4 + x1 + x2 ≡ 0 mod 4  (下の像の条件)
  x1, x2, x3, x4 ≧ 0
  x1, x2, x3, x4 ∈ Z

追加的な変数を導入してmodを取り除けば、これは整数線形計画問題になる。その結果の問題をLPファイル形式にすると以下ようになる(baroque_tower.lp)。

Minimize
  x1 + x2 + x3 + x4
Subject To
  c1: x1 + x2 + x3 - 4 n1 = -3
  c2: x2 + x3 + x4 - 4 n2 = -3
  c3: x3 + x4 + x1 - 4 n3 = 0
  c4: x4 + x1 + x2 - 4 n4 = 0
Bounds
  0 <= x1
  0 <= x2
  0 <= x3
  0 <= x4
  0 <= n1
  0 <= n2
  0 <= n3
  0 <= n4
General
  x1 x2 x3 x4 n1 n2 n3 n4
End

MIPソルバで解いてみる

これをMIPソルバのlpsolveを使って解かせてみる。

> lp_solve.exe -rxli xli_CPLEX.dll baroque_tower.lp
set_XLI: Successfully loaded 'xli_CPLEX.dll'

Value of objective function: 6.00000000

Actual values of the variables:
x1                              1
x2                              2
x3                              2
x4                              1
n1                              2
n2                              2
n3                              1
n4                              1

ということで、(x1,x2,x3,x4)=(1,2,2,1)という最適解が得られ、これは左上を1回、右上と右下を2回ずつ、左下を一回という、前回得られたものと同じ解が得られる。

実は最初はGLPKでも解こうと思ったけれど、GLPKだと、有界でない整数変数のせいで無限にブランチして止まらないっぽい。各変数に適当な上界を加えれば解ける。あと、自分が以前に書いたオモチャのMIPソルバでも楽勝で解けた。

最適解の一意性

最適解の一意性については、MIPソルバを使うよりも、論理結合子を自由に使えるSMTソルバの方が便利なので、SMTソルバのZ3で確認してみることにする。

以下の内容(baroque_tower.smt2)をZ3に与える（オンラインでも Z3 online at RiSE4Fun で試せる）ことで、6手の他の解が存在しないことを確認できる。詳しくは以下のコメント中にて。

; baroque_tower.smt2
(set-option :produce-models true)
(set-logic QF_LIA)

; 変数の宣言
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)

; 前述の制約条件の追加
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))
(assert (>= x4 0))
(assert (= (mod (+ 3 x1 x2 x3) 4) 0))
(assert (= (mod (+ 3 x2 x3 x4) 4) 0))
(assert (= (mod (+ x3 x4 x1) 4) 0))
(assert (= (mod (+ x4 x1 x2) 4) 0))

;; まずは適当に解を求めてみる
(check-sat)
; sat と出力され、解が存在することが分かるので、解を表示させる
(get-value (x1 x2 x3 x4))
; ((x1 1)
;  (x2 4946)
;  (x3 4990)
;  (x4 9749))

;; 既に最適解での目的関数値が6と分かっているので、その条件を加えて再度解いてみる  
(assert (= (+ x1 x2 x3 x4) 6))
(check-sat)
; 今度もsatと出力され、解が存在することが分かるので、 解を表示させる
(get-value (x1 x2 x3 x4))
; ((x1 1)
;  (x2 2)
;  (x3 2)
;  (x4 1))

;; 更に、今見つかった最適解を除外する制約を加えて、再度解いてみる
(assert (not (and (= x1 1) (= x2 2) (= x3 2) (= x4 1))))
(check-sat)
; 今度はunsatと出力され、従って今除外された以外の解がないことが分かる