論文の概要: Two-Colour Zig-Zag Numberlink on Rectangles: A Forbidden-Pattern Characterization, a Constructive Polynomial-Time Algorithm, and a Lean Verification

• arxiv url: http://arxiv.org/abs/2610.37691v1
• Date: Mon, 19 Oct 2026 22:59:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-02 06:06:26.166292
• Title: Two-Colour Zig-Zag Numberlink on Rectangles: A Forbidden-Pattern Characterization, a Constructive Polynomial-Time Algorithm, and a Lean Verification
• Title（参考訳）: 矩形上の二色ジグザグ数リンク:禁断パタン特性,構成多項式時間アルゴリズム,リーン検証
• Abstract要約: 格子内の任意の端点を持つ矩形上の2組の問題を解く。 矩形の両辺が少なくとも11であるとき、インスタンスは、禁じられたパターンの有限カタログのエントリが存在しない場合に限り解決可能である。 アルゴリズム,カタログ,証明構造,形式化における妥協,Python,JavaScript,Cの実装について述べる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: In Zig-Zag Numberlink, pairs of endpoints in a grid must be joined by vertex-disjoint paths that together visit every cell. The problem is NP-complete when the number of pairs is un- bounded (Adcock et al.). For a single pair it is the Hamiltonian path problem in rectangular grid graphs, solved by Itai, Papadimitriou and Szwarcfiter. Two pairs on a rectangle form the paired 2-disjoint path cover problem. We settle the case of two pairs on rectangles with the endpoints anywhere in the grid. If both sides of the rectangle are at least 11, an instance is solvable if and only if no entry of a finite catalogue of forbidden patterns occurs. The catalogue consists of a parity condition, an alternation condition on the border, a handful of local corner and edge patterns, 65 listed corner configurations, and a rule that propagates forced routes out of the corners before testing alternation. If a side is at most 10, a frontier dynamic programming algorithm decides the instance in time linear in the long side. The characterization is construc- tive. Solutions are built by deleting empty lines, splitting the rectangle by straight cuts, and splicing the pieces back together, in time O((R+C) RC). Both directions of the characterization and the correctness of the dynamic programming algorithm are verified in Lean 4. The finite case analyses, which are window certificates for the corner configurations and a check of all irreducible instances with sides 11-22, are carried out by the Lean compiler via native decide. We describe the algorithm, the catalogue, the proof structure, the compromises made in the formalization, and implementations in Python, JavaScript and C that produce identical output.
• Abstract（参考訳）: Zig-Zag Numberlinkでは、グリッド内のエンドポイントのペアは、すべてのセルを一緒に訪問する頂点非結合パスで結合されなければならない。 問題は、ペアの数が非有界であるときにNP完全である(Adcock et al )。 単一のペアに対して、それは正方形格子グラフのハミルトン経路問題であり、イタイ、パパディミトルー、シュヴァルツフィルガーによって解かれた。 矩形上の2対のペアは、ペア化された2-解離経路被覆問題を形成する。 格子上の任意の端点を持つ矩形上の2対の場合を解決する。 矩形の両辺が少なくとも11であるとき、インスタンスは、禁じられたパターンの有限カタログのエントリが存在しない場合に限り解決可能である。 カタログは、パリティ条件、国境での交替条件、一握りのローカルコーナーとエッジパターン、65のコーナー構成、および変更をテストする前にコーナーから強制経路を伝搬するルールで構成されている。 辺が少なくとも10である場合、フロンティア動的プログラミングアルゴリズムは、長い辺の時間のインスタンスを線形に決定する。 特徴は屈曲性である。 解は空の線を削除し、矩形を直線カットで分割し、時間 O((R+C) RC で部品をスプリシングすることで作られる。 動的プログラミングアルゴリズムの特徴付けの方向性と正確性は、Lean 4で検証される。 コーナー設定のためのウィンドウ証明書である有限ケース解析と、サイド11-22を持つすべての既約インスタンスのチェックは、ネイティブ決定を通じてリーンコンパイラによって実行される。 本稿では,アルゴリズム,カタログ,証明構造,形式化における妥協,同一出力を生成するPython,JavaScript,Cの実装について述べる。

関連論文リスト

• Draw2Think: Harnessing Geometry Reasoning through Constraint Engine Interaction [59.47026381165585]
  視覚言語モデルは精度を上げて幾何学的問題を解くが、その中間状態は潜伏し、検証できないままである。 我々は,GeoGebra制約エンジンとのエージェント相互作用に潜時空間推論から幾何推論を再キャストするフレームワークDraw2Thinkを提案する。
  論文  参考訳（メタデータ） (2026-05-20T05:46:14Z)
• GeoPAS: Geometric Probing for Algorithm Selection in Continuous Black-Box Optimisation [2.2060294178354307]
  GeoPASは、位置、向き、対数スケールでサンプリングされた複数の粗い2次元スライスによって問題インスタンスを表す。 共有妥当性を考慮した畳み込みエンコーダは、各スライスを埋め込みにマッピングし、スライススケールおよび振幅統計に基づいて条件付けする。 GeoPASは、離脱確率、グループランダム、離脱確率の評価の下で、単一最適解法よりも改善する。
  論文  参考訳（メタデータ） (2026-04-10T08:24:37Z)
• Structural Analysis of Directional qLDPC Codes [5.685589351789461]
  Gehér--Byfield--Ruban citeGeher2025Directional は量子低密度パリティチェック (qLDPC) 符号のハードウェア駆動型ファミリである。 これらの符号は、正方形またはヘックスグリッド接続上で固定エンフダイレクトワード(ルート)を実行するアンシラキュービットによって測定される安定化器によって定義される。
  論文  参考訳（メタデータ） (2026-02-22T05:59:57Z)
• AdaContour: Adaptive Contour Descriptor with Hierarchical Representation [52.381359663689004]
  既存の角度ベースの輪郭記述子は、星以外の形状の損失表現に悩まされる。 AdaConは、他のディスクリプタよりも正確に形を表現できる。
  論文  参考訳（メタデータ） (2024-04-12T07:30:24Z)
• CornerFormer: Boosting Corner Representation for Fine-Grained Structured Reconstruction [20.04081992616026]
  構造復元のための改良されたコーナー表現法を提案する。 隣接する角や小さな縁など、きめ細かい構造を再構築する方がよい。 コーナーでは+1.9%@F-1、エッジでは+3.0%@F-1である。
  論文  参考訳（メタデータ） (2023-04-14T11:51:26Z)
• Hybrid Trilinear and Bilinear Programming for Aligning Partially Overlapping Point Sets [85.71360365315128]
  多くの応用において、部分重なり合う点集合が対応するRPMアルゴリズムに不変であるようなアルゴリズムが必要である。 まず、目的が立方体有界関数であることを示し、次に、三線型および双線型単相変換の凸エンベロープを用いて、その下界を導出する。 次に、変換変数上の分岐のみを効率よく実行するブランチ・アンド・バウンド(BnB)アルゴリズムを開発する。
  論文  参考訳（メタデータ） (2021-01-19T04:24:23Z)
• Optimal network online change point localisation [73.93301212629231]
  オンラインネットワーク変化点検出の問題点について検討する。 この設定では、独立したベルヌーイネットワークの集合が順次収集され、基礎となる変化点が生じる。 目的は、虚偽のアラームの数または確率の制約に応じて、それが存在する場合、変更点をできるだけ早く検出することです。
  論文  参考訳（メタデータ） (2021-01-14T07:24:39Z)
• On Path Integration of Grid Cells: Group Representation and Isotropic Scaling [135.0473739504851]
  格子セルによる経路積分の一般的な表現モデルの理論的解析を行う。 我々は、歯列脳の格子細胞の同様の性質を共有する六角形格子パターンを学習する。 学習したモデルは、正確な長距離経路積分を行うことができる。
  論文  参考訳（メタデータ） (2020-06-18T03:44:35Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。