Concise QBF Encodings for Games on a Grid (extended version)

要約

タイトル：グリッド上のゲームのための簡潔なQBFエンコーディング（拡張版）

要約：

– QBFを使った2人用ゲームのエンコードは正確かつ効率的な方法を持つことが難しく、エラーが発生することがある。
– Tic-Tac-Toe、Connect-4、Domineering、Pursuer-Evader、Breakthroughなど、グリッドボード上でプレイされるゲームのための簡潔な仕様と一貫性のあるエンコーディングを可能にするために、計画ドメインでのPDDLの成功に着想を得て、Board-game Domain Definition Language (BDDL)を紹介する。
– BDDLをQBFに効率的に変換して、有界深度の勝利戦略の存在をエンコードする。リフトされたエンコードは、ボードの位置を象徴的に扱い、シンボリックなボード位置に対して条件、影響、勝利構成の簡潔な定義を可能にする。
– エンコードのサイズは入力モデルと考慮される深さに線形に増加する。私たちは、いくつかの既知のゲームのインスタンスの勝利戦略のクリティカルセットを計算するために、QBFソルバを使用してこのような汎用的なアプローチの実現可能性を示す。
– いくつかのゲームについては、私たちの作業が最初のQBFエンコードを提供する。
– SATベースの計画の場合と異なり、QBFベースの勝利戦略の検証は難しいため、QBF証明書と対話型ゲームプレイを使用して勝利戦略の検証方法を示す。

要約(オリジナル)

Encoding 2-player games in QBF correctly and efficiently is challenging and error-prone. To enable concise specifications and uniform encodings of games played on grid boards, like Tic-Tac-Toe, Connect-4, Domineering, Pursuer-Evader and Breakthrough, we introduce Board-game Domain Definition Language (BDDL), inspired by the success of PDDL in the planning domain. We provide an efficient translation from BDDL into QBF, encoding the existence of a winning strategy of bounded depth. Our lifted encoding treats board positions symbolically and allows concise definitions of conditions, effects and winning configurations, relative to symbolic board positions. The size of the encoding grows linearly in the input model and the considered depth. To show the feasibility of such a generic approach, we use QBF solvers to compute the critical depths of winning strategies for instances of several known games. For several games, our work provides the first QBF encoding. Unlike plan validation in SAT-based planning, validating QBF-based winning strategies is difficult. We show how to validate winning strategies using QBF certificates and interactive game play.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI