2021 Fiscal Year Research-status Report
On Exact Algorithms for Branching Program Satisfiability Problems by Approaches for Proving Lower Bounds
| Project/Area Number |
18K18003
|
|---|
| Research Institution | University of Hyogo |
|---|
Principal Investigator |
照山 順一 兵庫県立大学, 情報科学研究科, 助教 (40709862)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | 分岐プログラム / 充足可能性問題 / 論理回路 / 計算複雑性 |
|---|
| Outline of Annual Research Achievements |
分岐プログラムの充足可能性問題とは，与えられた分岐プログラムが値１を出力するような変数入力（0/1割当）が存在するかどうかを判定する問題である．与えられる分岐プログラムに制限がない場合，総当たり探索よりも高速なアルゴリズムは知られていない．本研究では，未解決問題である計算量クラスNEXPとNC1の分離を導くため，幅限定分岐プログラムに焦点をあて総当たり探索よりも高速なアルゴリズムの開発を目標としている．
特に，研究当初より幅２分岐プログラムを対象として高速な充足アルゴリズム（SATアルゴリズム）開発の研究を進めており，本年度は，線形サイズの幅２分岐プログラムに対する非自明な決定性SATアルゴリズムの開発に成功した．我々のアルゴリズムは幅２の分岐プログラムの下界証明手法を基盤としており，研究計画に挙げていた下界証明法をSATアルゴリズム開発に適用できる新しい事例を与えることに成功した．我々のアルゴリズムは大きく２つのステップに分かれている．第１に単調分岐プログラムへの分割，第２に下界証明手法であるANDとXORからなる論理式への変換である．特に，第２のステップで得られる論理式の構造に注目し，総当たり探索よりも効率的に充足可能性問題を解くアルゴリズムを設計している．本結果は学術論文誌に投稿し，採録が決定している．
さらに，乱数の使用を認めることにより，サイズが２乗に十分近い場合まで非自明な計算時間を達成する乱択SATアルゴリズムの開発にも成功している．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
提案したアルゴリズムに誤りがあったため修正が必要となったが，その誤りを修正し，線形サイズの幅２分岐プログラムに対する非自明なSATアルゴリズムの開発に成功した．本結果は論文誌に投稿し，採録が決定している．
|
| Strategy for Future Research Activity |
前年度までの成果では，扱うことのできる幅２分岐プログラムのサイズは線形サイズに留まっている．今後は，より大きなサイズの分岐プログラムにも対応できるか検討を行う．
|
| Causes of Carryover |
理由：コロナ禍により共同研究者との議論のための国内出張や国際会議等参加のための海外出張が不可能となり，国内旅費・海外旅費の執行に変更が生じた．
使用計画：コロナ情勢によるが，本研究をさらに加速させるために共同研究者との対面による議論頻度を増やす．また，最新の研究成果調査のため，国内学会及び国際会議への参加を積極的に行う．
|
