QSATから削減を選択した場合、タスクは数式から始まります。
プレーヤー1が勝利戦略を持っている場合、この式の否定がトートロジーになるように、ゲームのインスタンスを作成する必要があります。プレーヤー2の役割は、主に全称記号のブール変数の評価を修正することです。プレーヤー1は、存在記号のブール変数に関して同様の役割を果たします。
トートロジーの場合、プレーヤー1がゼロサムのみを強制できるように、テーブルにデータを入力する際にある程度の工夫を示す必要があります。また、必要なテーブル行の数が、数式内の数量詞の出現数でのみ線形であることを確認してください。
[SPOILER1が開始します]宿題モードで話し合うことを忘れないでください。ここで、ほとんどすべての詳細をヒントに追加しますが、詳細を理解すると、ソリューションに3つの技術的な欠陥が見つかると思います。できるだけ多くの人を見つけて、コメントでできるだけ多くの人に独自の修正を提案してください。
まず、ゲーム理論の用語でQSATを見てください。一般性を失うことなく、数量化されたブール文（自由変数のない式）がすべての数量詞を前にして書かれていると仮定します。最初にいくつかの存在記号、次にいくつかのユニバーサル、次に別の存在ブロックなど。最初のプレーヤーは、特定のブール値を最初のいくつかの存在記号に割り当てる（置換する）ことによって再生を開始します（最初のブロック全体に、置換後の式が左端の全称記号で始まる場合にのみ停止します。次に、プレーヤー2は全称記号の最初のブロックを処理します。同様に数量化;次に、プレーヤー1は、元々存在記号の2番目のブロックであったものに進みます。以下同様です。すべての変数が指定された後、式が「true」と評価された場合、プレーヤー1が勝ちます。
このQSATゲームは、数式のコーディングを想定している場合にも数値でプレイできるため、各数式には構文に基づいて一意の番号が付けられます（数式から数値を効率的に決定し、数値から数式を効率的に決定できるようにします）。数式を交換する代わりに、プレイヤーは番号（数式コード）を交換します。
ここで、このQSATのようなゲームをボードゲームに変換したいとします。各行は、1人のプレーヤーの動きを表します（同じタイプの数量詞の1つのブロックを表します）。行の各場所は、前の行の任意の位置からのそのプレーヤーの可能な移動を表します。より具体的には、移動によって生じる数値の違い：移動後の数式のコードから移動前の数式のコードを引いたものです。このように、現在の合計は、ゲームの特定のフェーズにあるため、常に数式と等しくなります。
特別な例外として、数式のコードをさらに減算して、最後の行のすべての場所を変更しますtrue。このように、完了したボードゲームの合計は、プレーヤー1が勝った場合は0になり、そうでない場合はゼロ以外になります。それはあなたのボードゲームへの定量化された公式のtautologicityの望ましい減少です。【ネタバレ1終了】