[2E1-J-1] 基礎・理論: 量子と探索

[2E1-J-1-03] SATソルバーを利用した施設配置のメカニズムデザイン

〇岡田 和夏¹、和田 勇歩¹、東藤 大樹¹、横尾 真¹ (1. 九州大学)

キーワード：SATソルバー、メカニズムデザイン、施設配置問題、架空名義操作不可能性、パレート効率性

我々は，充足可能性問題を解くソフトウェアであるSATソルバーを用いた計算機科学的アプローチで，多次元離散空間上の単一施設配置問題の解析を試みる．エージェントの選好は，自身の所在地から施設の配置位置までの距離が小さい程，効用が高いとする単峰的選好と，自身の所在地から施設の配置位置までの距離が大きい程，効用が高いと考える単溝的選好の2種類とする．本論文では，まず，グラフとエージェントの選好から，自動でCNF形式のSATインスタンスを生成するアルゴリズムの提案を行い，パレート効率性および架空名義操作不可能性に関する施設配置問題のSAT符号化を行った．次に，PicoSATを用いて実際に多次元離散空間上の施設配置問題を解き，パレート効率性および架空名義操作不可能性を同時に満たすメカニズムの存在性が，理論的結果と一致することを確認した．最後に，SATソルバーによって，サイズ2×3の格子空間において単溝的選好の場合，パレート効率性，架空名義操作不可能性，および全射性を同時に満たすメカニズムが存在しないことを示した．