Exocet

Exocetは、他のアルゴリズムとは"異なるタイプのLocked"です。Exocetのみで解ける局面もあり、魅力的なアルゴリズムです。
Exocetには、素朴なタイプから拡張タイプまで 様々な種類があり、Exocetはそれらの総称です。
ver.6.0では Target 型の Exocet を対象とします。 Object 型は将来のバージョンの課題です。

1.   JExocet (JE2)
2.   JExocet (JE1)
3.   SExocet (SE)
4.   SExocet Single
5.   SExocet SingleBase
6.   F/M Exocet (Franke/Mutant Exocet)


7.   Exocet ファミリー
8.   Exocet サンプル

 Junior Exocet (JE2)

JExocetは、Base、S領域、Target の関係 による Locked です。
Baseの2セルには、3以上の候補数字があります。2つならLockedSetなので、3つ以上とします。

JExocet Lockedは、つぎのような制約です。
  Exocet Locked : Baseの候補数字からどの2つの数字組を選んだとしても、それらは Target1 と Target2 で肯定となる。

実際には Baseには候補数字が2つ超あるので、"どの2つの数字組を選んでも矛盾しない。(どの2つの数字組が正しいと仮定しても矛盾は生じない。)" という状態です。

JExocet Lockedからは、次の論理が展開できます。これらは、以下の 除外 の項で詳述します。

1. Targetには、候補数字以外は入らない。
2. Base数字が 一方のTargetで 肯定 なら、他方のTargetでは 否定 である。
3. Cross-Cover-Line をもつベース数字は、対応する Target で 否定 である。

以下に示す "形の定義"と"候補数字の条件" を満たすとき、JExocet Locked は成立します。

 (1) JE2 形の定義

Junior Exocet(JE2) には、複数の役割のセルがあり、次の図のように配置されます。

• Baseセルは1ブロック内のminiラインに配置する。
• Escapeセルは、Baseセルと相補的な位置にある。
• Targetセルの配置には、対角形（Diagonal）と整列形（Aligned）の2タイプがある。
• Companionセルは、Targetセルの位置に連動して配置される。

* [Exocetの最初の理解のための補足]
  Exocet の仕組みの理解には、"方向" を区別するのが役立ちます。
  "Baseの並び"を基準として、これと並行の方向は "Parallel"です。交差する方向は "Cross" です。
  文脈から明らかなときは、これらはしばしば省略されます。

JExocetの形は、次の手順で導きます。これらは、JExocetの解法コードを作成する上でも参考になります。

1. ステップ 1 : 盤面上の一つのセル(Stemセル)と、方向(行、列)を選ぶ。これによって、mini-lineが決まる。
   mini-lineの2つのBaseセル(B1,B2)と、Band、2つのブロック(Block1,Block2)が決まる。 また、Stemセルと方向から、Cross-Line-0が決まる。

   *mini-line は、ブロック内の行または列の3セル。
   *Stemセルは形を導くためのもので、Exocetのロジックには関わりません。 また、Stemセルは、確定/未確定のいずれでも選べます。
   



2. ステップ 2 : ブロック1,2にあり Baseに連結しないセルは、それぞれ6セルある。各ブロックから、数字未確定の Target セルを選ぶ(T1,T2)。
   方向と Targetセル(T1,T2)から、Companionセル(C1,C2)、Cross-Line(CL1,CL2)、SLine(S1, S2) が定まります。 これらのセルは、確定/未確定のいずれの状態もあります。
   Companion には、Exocet 成立のうえで重要な役割があります。このことについては 後に 説明します。
   SLine(S0,S1,S2)は、Cross-LineのBand外の領域です。

Mirrorは、Exocet Locked の成立には関係しません。GNPXでは、Mirrorは扱いません。

 (2) JE2 候補数字の条件

JExocet の形の定義のもとで、次の条件(R1～R4) をテストします。
全てのBase数字が条件 R1～R4 を満たすとき、Exocet Locked になります。

JE2 候補数字の条件

 (3) JExocet の論理 ... Lockedの証明

R1～R4を満たすBase数字は、Locked です。
Base数字から 任意の2数字を選択 したとき、この2数字組について次の命題が成り立ちます。
    命題 : Baseで positive なら、Target1 と Target2 でも positive である。

JE2 Lockedの証明 (CL:Cross-Line)
1. L1. Baseセルで、ベース数字#ab は positive とする。Escapeでは #ab は negative となる。
2. L2. CL-0,CL-1,CL-2には、#abのインスタンスがそれぞれ 3つあり(数独のルール)、合わせて6個のインスタンスがある。
3. L3. R4より、Sセル(S0,S1,S2) には 2つの #a CoverLine、2つの#b CoverLine がある。
4. L4. "6-4=2"より、CL-1,CL-2の Band領域には #aと#b のインスタンスがある。
5. L5. #aと#b インスタンスは、Escape、Companionにはないので、それぞれ Target1 と Targe2にある。(どちらにどれかは確定しない)

 (4) Exocet Locked の理解

ここで、改めて Exocet Locked の状態を考えます。
Exocet Locked は、Baseの候補数字から どの2つの候補数字を選んだ としても、それらは Target で肯定となります。
対象とするPuzzleには解があり、かつ唯一解のPuzzleです。その解から翻れば いずれかの2つのBase候補数字(#a,#b)は確定数字(#A,#B)です。 Base候補数字は3つ以上あるので、残り"#x"に着目すると、候補数字#Xは Target で否定であり、Escapeで肯定です。
ただし、Puzzleを解く途中段階では、Base候補数字のどれが解であるかは分かっていません。
Exocet Lockedは、確定していない が それでも導けることがある 推論です。 同様のこと(推論)は、例えば LockedSet を思い浮かべると良いでしょう。

 除外

Exocet Locked が成立すると、Target の候補数字が 否定 に確定することがあります。
本HP および GNPX では、除外ルールは次のように用います。

1. 除外ルール は、Exocet の定義から導かれます。

     本HPでは、Bird 文書 の JE2のルール番号を流用します。
     JExocet Compendium   by:David P Bird
     http://forum.enjoysudoku.com/jexocet-compendium-t32370.html
   

2. 波及的(二次的)に、否定/肯定 が導かれる論理は対象としません。
   これは他の解析アルゴリズムと同じです。
   二次的な効果は、次のステップで解析されます。

 除外ルール

1. E3. Target内の 非ベース数字は 否定である。

   Exocet Locked なら、Targetには いづれかの ベース候補数字が入ります。したがって、非ベース数字が Target に入る余地はない。
   
   




2. E5. Cross Cover-Lineをもつベース数字は、対応する Target で 否定 である。

   これは、次のように導けます。
   1. (1) S1に #a の Cross-Cover-Line があるとします。
   2. (2) 命題:T1で Base候補数字#a は positive とする。
   3. (3) Baseの#aは positive。
   4. (4) S0には #a インスタンスがある。
   5. (5) S2には #a インスタンスはない。
   6. (6) T2には +#a がある。
   7. (7) T1#a と T2#a は矛盾する(他のBase数字がTargetに配置できない)。
           従って、(2)命題は偽であり、T1の #a は negativeである。
   
   
   
   
   

 除外-2

除外-2 は、2つのベース数字 による 除外 です。Bird の文書では, "Incomtible Base Pairs" の項です。
2つの Base にある 候補数字 は、自由な組み合わせで ベース数字の候補にはなりません。 例えば、Baseの 候補数字が(1,2,3)であれば、{(1,2),(1,3),(2,3),(2,1),(3,1)(3,2)}の組み合わせがあります。 また、2つのBaseの候補が異なる場合には、可能な組み合わせのパターンになります。

これらの組み合わせに対して、それぞれをテストします。Exocetの性質から、次のことを用います。

1. テスト対象の Base数字 は、それぞれTarget にある。
2. 2つのBase数字のインスタンスは、S0にある。インスタンスは確定済みのこともある。
3. 2つのBase Cellの 2つのCross-Blockには、候補状態の Base数字がある。

1. Case-1:2つのBase数字のS0におけるインスタンスが、同じセルになる。
              このパターンは数独解としてあり得ないので、この組み合わせパターンは除外できる。


2. Case-2:2つのBase数字のS0におけるインスタンスが、同じ Cross-Block にある。
              このパターンは、Cross-Block のBase数字を全て排除する。
              もう一つの Cross-Block には何も影響しません。
              したがって、この組み合わせは Baseと UR の関係になり、
              数独解の唯一性から、この組み合わせパターンは除外できる。


3. Case-3:2つのBase数字のS0におけるインスタンスが、異なる Cross-Block にある。
              このパターンは、それぞれの Cross-Block で それぞれの Base数字 を排除する。
              この場合は、Baseと UR にはなりません。
              したがって、この組み合わせパターンは解の可能性が残る。

 Junior Exocet_1 (JE1)

JE1は Targetが1つのタイプです。JE2での 一つのTarget(Object)がある位置に、確定数字（問題数字、または解析により確定した数字）があります。
JE1の要素は、Base、Base数字、1つのTarget、確定数字Object(Base数字以外の確定数字があるObject)です。 BaseのCrossLine、Targetと空白ObjectのSLineは、Junior Exocetの自然な形で定義します。

Sセル{S0,S1,S2}のカバーの仕方には、2つのタイプがあります。これは、JE1特有の条件です。

• S 基準 : 2つの CoverLine でカバーされる。
• Wildcard 基準 : 3つの CoverLine でカバーされる。

 JE1 の論理

JE1の Base数字 のカバーの仕方別に次の論理が成り立ちます。

1. (1) S基準を満たす Base数字

   S基準 Lockedの証明 (CL:Cross-Line)
   1. 1)Base数字 #aは、S領域に2つのCoverLineがある とします。
   2. 2)S領域を含むCrossLineには、合わせて3つの#aインスタンスが必要である。
   3. 3)従って、Targetに #a がある。(3-2=1)
   Target が Object タイプの場合には、Object の2セルにある。
   
   
   

2. (2) Wildcard基準を満たす Base数字

   JWildcard基準の証明 (CL:Cross-Line)
   1. 1)Base数字 #zは、S領域に2超のCoverLineがある とします。
   2. 2)S領域を含むCrossLineには、合わせて3つの#zインスタンス必要である。
   3. 3)従って、Targetに #z はない。(3-3=0)
   
   
   

 JE1 の除外

JE1 が成立すると、次の除外ができます。

1. Target の Wildcard(#z)は、negative に確定
2. Baseの Wildcard は positive に確定、Base のもう一つの数字は未定。
3. Escape にある Wildcard は negative に確定。
4. Sline-1にある Wildcard は positive に確定。これが１つなら、対応セルの Wildcard 以外の候補は除外できる。
5. BaseとTargetのWildcardが確定することで、これの影響圏の Wildcard 数字は negative になる。