数字つなぎというパズルがあります。ありますのは事実ですが、名称が一般的過ぎて特定できない恐れもありますな。JPC2013(http://jppuzzles.com/jpc2013/)やLMIのパズラーラウンド(http://logicmastersindia.com/2013/11P/)で出題されていたあれです。詳しいルールはそちらを参照してください。
で、ルールの構造的にはナンバーリンクと近しいところがありますので、現状存在するナンバーリンクのソルバーをちょっといじれば、数字つなぎのソルバーもできるんではないのか、というアイデアが出てきます。（ちなみに、このアイデア自体は某パズル作家さんが雑談で言っていたことで、ここに私のオリジナリティはありません）
ナンバーリンクのソルバーは現状いくつか公開されているようですが、私がいじれるという利点からsugarを利用する方法を考えてみたいと思います。私が知る限りsugarを利用したナンバーリンク解法は、a.sugar開発元の田村研のページ(http://bach.istc.kobe-u.ac.jp/sugar/puzzles/numberlink.html)、b.藤原博文さんの「プログラミング不要の「制約プログラミング手習い」」(http://karetta.jp/book-node/withoutprogramming/225938)にあります。ここでは、a.の手法をパクります。用語等できるだけ同一のものを使用する努力はします。
都合上ざっとその手法を以下で説明するつもりですが、用語の濫用に当たる記述を特に気にしませんので、もし活用する気があるなら、本家に当たる方が良いかと思います。
1. 各節点(マスのことです)に対して、１から表出数字までの値をとる変数x_i_jを用意します。この変数は、その節点を通る線がどの表出数字から延びてきたものかをあらわします。
2. タテヨコに隣接する節点に対し、0か1をとる変数(h_i_j,v_i_j,タテかヨコかを区別するために二つあるだけです)を用意し、これを辺と呼びます。辺が0なら、その節点どうしは直接線でつながっていません。1ならつながっています。
3. 各節点につながっている辺（最大で４、最少で２あります）に関して、表出数字の部分以外について、合計値が0か2であるという制約を加えます。3だと線が枝分かれしている状態、1だと線が途切れている状態を表します。表出数字の節点につながっている辺の合計値は1と制約します。
4. 辺が1である場合、その辺がつないでいる節点の数値は等しくなるよう制約を加えます。
実例を図で示します。赤数字で節点の数値を、青数字で辺の数値を表しています。（説明で色を使うのはあまりよろしくないという話もありますけどご勘弁ください）
図１
図２
さて、この手法を数字つなぎに応用することを考えます。
3. の制約を、以下のように変更します。
「表出数字の節点につながっている辺の合計値は1と制約します」
↓
「最小と最大の表出数字につながっている辺の合計値は1、それ以外の表出数字につながっている辺の合計値は2と制約します」
4. の制約に、以下の例外を追加します。
「ただし、最小以外の表出数字につながっている辺に関しては、この制約を以下のように変更します。3.で合計値が2であると制約されてるので、最大４つ存在するの辺のうち２つは1ですが、このうちひとつは同じ節点の数字を結んでおり、もうひとつは、表出数字よりひとつ少ない数字の接点を結んでいる」
イメージとしては、表出数字に隣接したマスに、ひとつ少ない表出数字から伸びてきた線が入ってきたら、それを捕捉する感じです。
これでできたできたーと思っていたのですが、よく考えたら以下のような別解が検出できないことに気付きました。
図３
図４
図５
たとえば、図３を作意解としてこのソルバーを動かせば、図４が出力されるので別解があるとわかりますが、図４を作意解としてこのソルバーを動かした場合、図３が出力されないので、別解チェッカーとしては使用できないことになります。
全マス通過の作意解ならば、この手法でも別解検出はできるはずですが、こんな状況なので証明したほうがいいよなーと思いつつ面倒なのでしてません。
ということで結論。
１．提案したちょい変の手法で、数字つなぎの全マス通過の作意解の別解の存在は検出できる！
２．たぶんできると(略)
３．できるんじゃ(略)
４．ま、ちょっと覚悟はして(略)
５．全マス通過でない作意解の場合、この手法では検出できない別解が存在する。
