• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2021 年度 実施状況報告書

下界証明アプローチによる分岐プログラム充足アルゴリズムの研究

研究課題

研究課題/領域番号 18K18003
研究機関兵庫県立大学

研究代表者

照山 順一  兵庫県立大学, 情報科学研究科, 助教 (40709862)

研究期間 (年度) 2018-04-01 – 2023-03-31
キーワード分岐プログラム / 充足可能性問題 / 論理回路 / 計算複雑性
研究実績の概要

分岐プログラムの充足可能性問題とは,与えられた分岐プログラムが値1を出力するような変数入力(0/1割当)が存在するかどうかを判定する問題である.与えられる分岐プログラムに制限がない場合,総当たり探索よりも高速なアルゴリズムは知られていない.本研究では,未解決問題である計算量クラスNEXPとNC1の分離を導くため,幅限定分岐プログラムに焦点をあて総当たり探索よりも高速なアルゴリズムの開発を目標としている.
特に,研究当初より幅2分岐プログラムを対象として高速な充足アルゴリズム(SATアルゴリズム)開発の研究を進めており,本年度は,線形サイズの幅2分岐プログラムに対する非自明な決定性SATアルゴリズムの開発に成功した.我々のアルゴリズムは幅2の分岐プログラムの下界証明手法を基盤としており,研究計画に挙げていた下界証明法をSATアルゴリズム開発に適用できる新しい事例を与えることに成功した.我々のアルゴリズムは大きく2つのステップに分かれている.第1に単調分岐プログラムへの分割,第2に下界証明手法であるANDとXORからなる論理式への変換である.特に,第2のステップで得られる論理式の構造に注目し,総当たり探索よりも効率的に充足可能性問題を解くアルゴリズムを設計している.本結果は学術論文誌に投稿し,採録が決定している.
さらに,乱数の使用を認めることにより,サイズが2乗に十分近い場合まで非自明な計算時間を達成する乱択SATアルゴリズムの開発にも成功している.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

提案したアルゴリズムに誤りがあったため修正が必要となったが,その誤りを修正し,線形サイズの幅2分岐プログラムに対する非自明なSATアルゴリズムの開発に成功した.本結果は論文誌に投稿し,採録が決定している.

今後の研究の推進方策

前年度までの成果では,扱うことのできる幅2分岐プログラムのサイズは線形サイズに留まっている.今後は,より大きなサイズの分岐プログラムにも対応できるか検討を行う.

次年度使用額が生じた理由

理由:コロナ禍により共同研究者との議論のための国内出張や国際会議等参加のための海外出張が不可能となり,国内旅費・海外旅費の執行に変更が生じた.
使用計画:コロナ情勢によるが,本研究をさらに加速させるために共同研究者との対面による議論頻度を増やす.また,最新の研究成果調査のため,国内学会及び国際会議への参加を積極的に行う.

  • 研究成果

    (1件)

すべて 2022

すべて 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件)

  • [雑誌論文] A Satisfiability Algorithm for Deterministic Width-2 Branching Programs2022

    • 著者名/発表者名
      Tomu MAKITA, Atsuki NAGAO, Tatsuki OKADA, Kazuhisa SETO, Junichi TERUYAMA
    • 雑誌名

      IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

      巻: E105.A ページ: 1298~1308

    • DOI

      10.1587/transfun.2021EAP1120

    • 査読あり / オープンアクセス

URL: 

公開日: 2022-12-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi