基本情報

所属

• 情報科学研究院　情報理工学部門　知識ソフトウェア科学分野

職名

• 准教授

学位

• 博士（情報学）（2010年03月 京都大学）

ホームページURL

https://kaken.nii.ac.jp/d/r/20584056.ja.html

J-Global ID

• 201501014888315418

研究キーワード

• アルゴリズム設計論   計算量理論   

研究分野

• 情報通信 / 情報学基礎論

担当教育組織

•  学士課程　工学部
•  修士課程　情報科学院
•  博士課程　情報科学院

職歴

• 2020年11月 - 現在 北海道大学 大学院情報科学研究院 准教授
• 2017年04月 - 2020年10月 成蹊大学 理工学部 准教授
• 2015年04月 - 2017年03月 成蹊大学 理工学部 専任講師
• 2013年09月 - 2015年03月 成蹊大学 理工学部 助教
• 2012年10月 - 2013年09月 電気通信大学 大学院情報理工学研究科 非常勤研究員
• 2010年04月 - 2012年09月 京都大学 大学院情報学研究科 特定研究員

所属学協会

• 電子情報通信学会   

研究活動情報

論文

• Theoretical Aspects of Generating Instances with Unique Solutions: Pre-assignment Models for Unique Vertex Cover.

  Takashi Horiyama, Yasuaki Kobayashi, Hirotaka Ono 0001, Kazuhisa Seto, Ryu Suzuki

  AAAI 20726 - 20734 2024年
• Finding top-k longest palindromes in substrings

  Kazuki Mitani, Takuya Mieno, Kazuhisa Seto, Takashi Horiyama

  Theoretical Computer Science 114183 - 114183 2023年09月 [査読有り]
  
• Theoretical Aspects of Generating Instances with Unique Solutions: Pre-assignment Models for Unique Vertex Cover.

  Takashi Horiyama, Yasuaki Kobayashi, Hirotaka Ono 0001, Kazuhisa Seto, Ryu Suzuki

  CoRR abs/2312.10599 2023年
• Optimal LZ-End Parsing Is Hard.

  Hideo Bannai, Mitsuru Funakoshi, Kazuhiro Kurita, Yuto Nakashima, Kazuhisa Seto, Takeaki Uno

  34th Annual Symposium on Combinatorial Pattern Matching, CPM 2023, June 26-28, Marne-la-Vallée, France 3 - 11 2023年 [査読有り]
  
• A Satisfiability Algorithm for Deterministic Width-2 Branching Programs

  MAKITA Tomu, NAGAO Atsuki, OKADA Tatsuki, SETO Kazuhisa, TERUYAMA Junichi

  IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E105.A 9 1298 - 1308 2022年09月01日 [査読有り]
   

  A branching program is a well-studied model of computation and a representation for Boolean functions. It is a directed acyclic graph with a unique root node, some accepting nodes, and some rejecting nodes. Except for the accepting and rejecting nodes, each node has a label with a variable and each outgoing edge of the node has a label with a 0/1 assignment of the variable. The satisfiability problem for branching programs is, given a branching program with n variables and m nodes, to determine if there exists some assignment that activates a consistent path from the root to an accepting node. The width of a branching program is the maximum number of nodes at any level. The satisfiability problem for width-2 branching programs is known to be NP-complete. In this paper, we present a satisfiability algorithm for width-2 branching programs with n variables and cn nodes, and show that its running time is poly(n)·2^(1-µ(c))n, where µ(c)=1/2^{O(c log c)}. Our algorithm consists of two phases. First, we transform a given width-2 branching program to a set of some structured formulas that consist of AND and Exclusive-OR gates. Then, we check the satisfiability of these formulas by a greedy restriction method depending on the frequency of the occurrence of variables.
• Satisfiability Algorithm for Syntactic Read-k-times Branching Programs.

  Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

  Theory Comput. Syst. 64 8 1392 - 1407 2020年 [査読有り]
  
• A Moderately Exponential Time Algorithm for k-IBDD Satisfiability.

  Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

  Algorithmica 80 10 2725 - 2741 2018年 [査読有り][通常論文]
  
• Satisfiability Algorithm for Syntactic Read-$k$-times Branching Programs.

  Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

  28th International Symposium on Algorithms and Computation, ISAAC 2017, December 9-12, 2017, Phuket, Thailand 58 - 10 2017年 [査読有り][通常論文]
  
• Improved exact algorithms for mildly sparse instances of Max SAT.

  Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, Junichi Teruyama

  Theor. Comput. Sci. 697 58 - 68 2017年 [査読有り][通常論文]
   

  We present improved exponential time exact algorithms for Max SAT. Our algorithms run in time of the form 0 (2((1-mu(c))n)) for instances with n variables and m = cn clauses. In this setting, there are three incomparable currently best algorithms: a deterministic exponential space algorithm with mu(c) = 1/o(clog c) due to Dantsin and Wolpert (2006) [9], a randomized l3c) polynomial space algorithm with mu(c) =1/o(clog(3) c) and a deterministic polynomial space algorithm with it mu(c) = 1/(c(2) log(2) c) due to Sakai, Seto and Tamaki (2015) [30]. Our first result is a deterministic polynomial space algorithm with mu(c) = 1/o(clog c) that achieves the previous best time complexity without exponential space or randomization. Furthermore, this algorithm can handle instances with exponentially large weights and hard constraints. The previous algorithms and our deterministic polynomial space algorithm run super-polynomially faster than 2(n) only if m = O(n(2)). Our second results are deterministic exponential space algorithms for Max SAT with mu(c) =1/o((c log c)(2/3)) and for Max 3-SAT with mu(c) = 1/o(c(1/2)) that run super-polynomially faster than 2n when m = o(n(5/2)/log(5/2) n) and m = o(n(3)/ log(2) n) respectively. Our third result is a randomized exponential space algorithm for Max SAT with mu(c) = 1/o(c(1/2) log(3/2) c) that run super-polynomially faster than 2n when m = o(n(3)/ log(5) n). (C) 2017 Elsevier B.V. All rights reserved.
• Bounded Depth Circuits with Weighted Symmetric Gates: Satisfiability, Lower Bounds and Compression.

  Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, Junichi Teruyama

  J. Comput. Syst. Sci. 105 82 - 16 2016年 [査読有り][通常論文]
  
• An Exact Algorithm for Oblivious Read-Twice Branching Program Satisfiability.

  Kazuhisa Seto, Junichi Teruyama

  IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 99-A 6 1019 - 1024 2016年 [査読有り][通常論文]
  
• An introduction to lower bounds on resolution proof systems (Special issue: Reviews and lectures : exploring the limits of computation II)

  Seto Kazuhisa

  Interdisciplinary Information Sciences 21 4 307 - 328 東北大学 2015年12月 [査読有り]
   

  Proof complexity, a measure to estimate the sizes of proofs in propositional logics, is studied as one of the fundamental approaches to the \mathcal{P} versus \mathcal{NP} problem, and has some practical applications such as automated theorem proving. It is a very hard task to prove lower bounds on strong proof systems such as Frege systems, for which no non-trivial lower bound is known yet. On the other hand, we have some rich success stories on weaker proof systems such as resolution proof systems. In this paper, we focus on resolution proof systems and review some of the existing techniques for proving lower bounds.
• Improved Exact Algorithms for Mildly Sparse Instances of Max SAT.

  Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, Junichi Teruyama

  10th International Symposium on Parameterized and Exact Computation, IPEC 2015, September 16-18, 2015, Patras, Greece 43 90 - 101 2015年 [査読有り][通常論文]
  
• Efficient Algorithms for Sorting k-Sets in Bins.

  Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

  IEICE Trans. Inf. Syst. 98-D 10 1736 - 1743 2015年 [査読有り][通常論文]
  
• A Moderately Exponential Time Algorithm for k-IBDD Satisfiability.

  Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

  Algorithms and Data Structures - 14th International Symposium, WADS 2015, Victoria, BC, Canada, August 5-7, 2015. Proceedings 9214 554 - 565 2015年 [査読有り][通常論文]
  
• Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction.

  Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki

  Theory Comput. Syst. 57 2 426 - 443 2015年 [査読有り][通常論文]
  
• Efficient Algorithms for Sorting k-Sets in Bins.

  Atsuki Nagao, Kazuhisa Seto, Junichi Teruyama

  ALGORITHMS AND COMPUTATION, WALCOM 2014 8344 225 - 236 2014年 [査読有り][通常論文]
   

  We give efficient algorithms for Sorting k-Sets in Bins. The Sorting k-Sets in Bins problem can be described as follows: We are given numbered n bins with k balls in each bin. Balls in the i-th bin are numbered n - i + 1. We can only swap balls between adjacent bins. How many swaps are needed to move all balls to the same numbered bins. For this problem, we design an efficient greedy algorithm with k+1/4n(2) + O(kn) swaps. As k and n increase, this approaches the lower bound of inverted right perpendicular((kn)(2))/(2k-1)inverted left perpendicular. In addition, we design a more efficient recursive algorithm using 15/16n(2) + O(n) swaps for the k = 3 case.
• Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction.

  Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki

  THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2014 8561 32 - 47 2014年 [査読有り][通常論文]
   

  We present a moderately exponential time polynomial space algorithm for sparse instances of Max SAT. Our algorithms run in time of the form O(2((1-mu(c))n)) for instances with n variables and cn clauses. Our deterministic and randomized algorithm achieve mu(c) = Omega(1/c(2) log(2) c) and mu(c) = Omega(1/c log(3) c) respectively. Previously, an exponential space deterministic algorithm with mu(c) = Omega(1/c log c) was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space deterministic algorithm with mu(c) = Omega(1/2(O(c))) was shown by Kulikov and Kutzkov [CSR 2007]. Our algorithms have three new features. They can handle instances with (1) weights and (2) hard constraints, and also (3) they can solve counting versions of Max SAT. Our deterministic algorithm is based on the combination of two techniques, width reduction of Schuler and greedy restriction of Santhanam. Our randomized algorithm uses random restriction instead of greedy restriction.
• A satisfiability algorithm and average-case hardness for formulas over the full binary basis.

  Kazuhisa Seto, Suguru Tamaki

  Comput. Complex. 22 2 245 - 274 2013年 [査読有り][通常論文]
  
• A Satisfiability Algorithm and Average-Case Hardness for Formulas over the Full Binary Basis

  Kazuhisa Seto, Suguru Tamaki

  The 27th IEEE Conference on Computational Complexity (CCC) 2012年06月 [査読有り][通常論文]
  
• Improved Randomized Algorithms for 3-SAT.

  Kazuo Iwama, Kazuhisa Seto, Tadashi Takai, Suguru Tamaki

  Algorithms and Computation - 21st International Symposium, ISAAC 2010, Jeju Island, Korea, December 15-17, 2010, Proceedings, Part I 6506 73 - 84 2010年 [査読有り][通常論文]
  
• The complexity of the Hajós calculus for planar graphs.

  Kazuo Iwama, Kazuhisa Seto, Suguru Tamaki

  Theor. Comput. Sci. 411 7-9 1182 - 1191 2010年 [査読有り][通常論文]
  
• The Planar Hajós Calculus for Bounded Degree Graphs.

  Kazuo Iwama, Kazuhisa Seto, Suguru Tamaki

  IEICE Transactions 93-A 6 1000 - 1007 2010年 [査読有り][通常論文]
  

講演・口頭発表等

• 多数決関数の計算複雑さと未解決問題について  [通常講演]

  脊戸 和寿

  電子情報通信学会コンピュテーション研究会 2022年12月 口頭発表（一般）
• A Moderately Exponential Time Satisfiability Algorithm for Linear-Sized Deterministic Width-2 Branching Programs  [通常講演]

  Tomu Makita, Atsuki Nagao, Tatsuki Okada, Kazuhisa Seto, Junichi Teruyama

  電子情報通信学会コンピュテーション研究会 2022年10月 口頭発表（一般）

その他活動・業績

• Optimal LZ-End Parsing is Hard.

  Hideo Bannai, Mitsuru Funakoshi, Kazuhiro Kurita, Yuto Nakashima, Kazuhisa Seto, Takeaki Uno CoRR abs/2302.02586 2023年
• Internal Longest Palindrome Queries in Optimal Time.

  Kazuki Mitani, Takuya Mieno, Kazuhisa Seto, Takashi Horiyama CoRR abs/2210.02000 2022年
• 理工学部初年次学生に対するオンデマンド型online講義による情報関連講義の教育効果—Effectiveness of an On-demand Online Course in Information Science for First-year Science and Engineering Students

  井内 勝哉, 西尾 悠, 脊戸 和寿, 小川 隆申 リメディアル教育研究 / リメディアル教育研究編集委員会 16 (25) 161 -167 2022年 

  本稿では，理工学部初年次生に対する情報教育において，オンデマンド型online講義をデザインした。講義毎の課題および講義期間終了後の授業アンケートを解析した結果，オンデマンド型online講義では課題達成能力，理解度，満足度の点で対面講義より評価が高かった。オンデマンド型online講義の特徴である反復学習により，理解度の向上が予想された。初年次生の知識の習得幅が大きい情報教育では，オンデマンド型online講義で知識を習得し，その後，対面講義や実習などによる知識の定着が効果的と想定された。
• コンピュテーション研究会 近況報告

  脊戸 和寿 情報・システムソサイエティ誌 23 (3) 8 -9 2018年11月01日 [査読無し]
  
• Sorting k-Sets in Bins問題に対する貪欲アルゴリズムの上界の改良 (コンピュテーション)

  清水 堅斗, 三觜 辰也, 脊戸 和寿 電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116 (503) 29 -32 2017年03月07日 [査読無し][通常論文]
  
• SYM-AND2段回路の充足可能性問題に対する厳密アルゴリズム

  脊戸 和寿, 玉置 卓, 照山 順一 電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116 (262) 29 -34 2016年10月21日 [査読無し][通常論文]
  
• 線形サイズk‐IBDD充足可能性問題に対する厳密アルゴリズム

  脊戸和寿, 照山順一, 照山順一, 長尾篤樹, 長尾篤樹 情報処理学会研究報告(Web) 2015 (AL-152) VOL.2015-AL-152,NO.1 (WEB ONLY) 2015年02月24日 [査読無し][通常論文]
  
• 線形サイズk-IBDD充足可能性問題に対する厳密アルゴリズム

  脊戸 和寿, 照山 順一, 長尾 篤樹 研究報告アルゴリズム（AL） 2015 (1) 1 -7 2015年02月24日 [査読無し][通常論文]
   

  k-IBDD は，k 段のレイヤーを持つ分岐プログラムであり，各レイヤーが OBDD (順序付き二分決定図) となっている．本稿では，k-IBDD 充足可能性問題 （以下，k-IBDD SAT） を考える．k-IBDD SAT とは，与えられた k-IBDD が 1 を出力するような変数割当が存在するかどうかを判定する問題である．本問題に対して，n 変数，poly(n) ノードの k-IBDD SAT を高々 poly(n)・2n-n1/2k-1 時間で解く多項式領域アルゴリズムが知られている．ここで，poly(n) は n の多項式を表す．本稿では，n 変数，cn ノードの k-IBDD SAT を高々 poly(n)・2(1-μ(c))n 時間で解く指数領域アルゴリズムを与える．ここで，μ(c)=Ω(1/(log c)2k-1-1) である．我々のアルゴリズムは既存のアルゴリズムを拡張することで線形サイズの k-IBDD に対して 2n 時間より指数的な高速化を達成している．
• 最大充足可能性問題の疎な例題に対する厳密アルゴリズム

  脊戸和寿 成けい大学理工学研究報告 51 (2) 19 -21 2014年12月01日 [査読無し][通常論文]
   

  type:Article We present a moderately exponential time polynomial space algorithm for sparse instances of Max SAT. For instances with n variables and cn clauses, our algorithm runs in time O(2^<(1-μ(c))n)>, where μ(c) = O(1/c^2log^2 c). Previously, an exponential space algorithm with μ(c) = O(1/clog c) was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space algorithm with μ(c) = O(1/2^) was shown by Kulikov and Kutzkov [CSR 2007]. Our algorithm is based on the combination of two techniques, width reduction of Schuler and greedy restriction of Santhanam. identifier:http://repository.seikei.ac.jp/dspace/handle/10928/606
• k‐IBDD充足可能性問題に対する厳密アルゴリズム

  脊戸和寿, 照山順一, 長尾篤樹 情報処理学会研究報告(Web) 2014 (AL-149) VOL.2014-AL-149,NO.9 (WEB ONLY) -6 2014年09月05日 [査読無し][通常論文]
   

  k-IBDD は，k 段のレイヤーを持つ分岐プログラムであり，各レイヤーが OBDD (順序付き二分決定図) となっている．本稿では，k-IBDD 充足可能性問題 （以下，k-IBDD SAT） を考える．k-IBDD SAT とは，入力として k-IBDD が与えられ，シンク 1 に到達する変数への割当が存在するかどうかを判定する問題である．本稿では，n 変数，poly(n) ノードの 2-IBDD SAT を高々 poly(n)・2n-√n 時間で解く多項式領域アルゴリズムを与える．poly(n) は n の多項式を表す．さらに，このアルゴリズムを拡張することにより，n 変数，poly(n) ノードの k-IBDD SAT を高々，poly(n)・2n-n1/2k-1 時間で解く多項式領域アルゴリズムを与える．
• k-IBDD充足可能性問題に対する厳密アルゴリズム

  脊戸和寿, 照山順一, 長尾篤樹 情報処理学会研究報告. AL, アルゴリズム研究会報告 2014 (9) 1 -6 2014年09月05日 [査読無し][通常論文]
   

  k-IBDD は,k 段のレイヤーを持つ分岐プログラムであり,各レイヤーが OBDD (順序付き二分決定図) となっている.本稿では,k-IBDD 充足可能性問題 (以下,k-IBDD SAT) を考える.k-IBDD SAT とは,入力として k-IBDD が与えられ,シンク 1 に到達する変数への割当が存在するかどうかを判定する問題である.本稿では,n 変数,poly(n) ノードの 2-IBDD SAT を高々 poly(n)・2n-√n 時間で解く多項式領域アルゴリズムを与える.poly(n) は n の多項式を表す.さらに,このアルゴリズムを拡張することにより,n 変数,poly(n) ノードの k-IBDD SAT を高々,poly(n)・2n-n1/2k-1 時間で解く多項式領域アルゴリズムを与える.
• 最大充足可能性問題の疎な例題に対する厳密アルゴリズム

  酒井隆行, 脊戸和寿, 玉置卓 電子情報通信学会大会講演論文集(CD-ROM) 2014 (1) ROMBUNNO.DS-1-5 -9"-"S-10" 2014年03月04日 [査読無し][通常論文]
  
• DS-1-5 最大充足可能性問題の疎な例題に対する厳密アルゴリズム(DS-1.COMP-ELC学生シンポジウム,シンポジウムセッション)

  酒井 隆行, 脊戸 和寿, 玉置 卓 電子情報通信学会総合大会講演論文集 2014 (1) "S -9"-"S-10" 2014年03月04日 [査読無し][通常論文]
  
• 計算複雑さへの招待(5) : 回路から迫るP vs. NP

  脊戸 和寿 電子情報通信学会技術研究報告. COMP, コンピュテーション 113 (371) 57 -57 2013年12月13日 [査読無し][通常論文]
  
• k集合整列問題に対する効率のよいアルゴリズム

  脊戸 和寿, 照山 順一, 長尾 篤樹 電子情報通信学会技術研究報告. COMP, コンピュテーション 113 (371) 81 -85 2013年12月13日 [査読無し][通常論文]
   

  本稿ではk集合整列問題に対して効率のよいアルゴリズムを与える.k集合整列問題とは以下のような問題である:n個のビンにk個のボールが入っており,i番目のビンにあるボールすべてに番号n-i+1がついている.隣り合うビンに存在する任意の2つのボールの交換のみを許した時,すべてのボールとビンの番号を一致させるためには何回の交換が必要だろうか.我々はこの問題に対して,高々(k+1)/4n^2+O(n)回の交換で本問題を解く貪欲アルゴリズムを与える.この値はn,kが大きくなるにつれて下界値と近くなる.また,k=3の場合に対してさらに効率のよいアルゴリズムを与える.このアルゴリズムは再帰的アルゴリズムであり,高々(15)/(16)n^2+O(n)回の交換で本問題を解くことができる.
• DS-1-4 Enumerating Non-3-colorable Planar Graphs by the Hajos Calculus

  Iwama Kazuo, Seto Kazuhisa, Tamaki Suguru 電子情報通信学会総合大会講演論文集 2010 (1) "S -7"-"S-8" 2010年03月02日

共同研究・競争的資金等の研究課題

• 超スマート社会時代のアルゴリズム工学 - パラメータ化近似均衡計算

  日本学術振興会：科学研究費助成事業 基盤研究(A)

  研究期間 : 2022年04月 -2027年03月 

  代表者 : 小野 廣隆, 柳浦 睦憲, 大舘 陽太, 脊戸 和寿, 土中 哲秀
• 列挙や数え上げなどを統一的に扱うための基盤技術

  日本学術振興会：科学研究費助成事業 基盤研究(B)

  研究期間 : 2022年04月 -2026年03月 

  代表者 : 堀山 貴史, 伝住 周平, 和佐 州洋, 栗田 和宏, 脊戸 和寿, 中畑 裕
• 定数段数回路における計算限界導出技法の研究

  日本学術振興会：科学研究費助成事業 基盤研究(C)

  研究期間 : 2021年04月 -2024年03月 

  代表者 : 脊戸 和寿

   

  本研究の目標は、MOD6素子（素子に入力される1の数が6の倍数のときに0を出力する素子）とAND素子、OR素子、NOT素子を用いた定数段数回路において多数決関数の非自明な下界を得ることである。 そのため、まず、AND素子、OR素子、NOT素子のみを使用した段数が定数の論理回路における多数決関数の素子数の下界、および分岐プログラムにおける多数決関数のサイズの下界の既存研究と証明技法の調査と整理を行った。その結果、2000年前後と状況はあまり変わっておらず、未だに上界に一致する下界が得られていないことを確認し、現在の知見と技法だけでは証明が難しい点を理解することができた。そのため、3段回路および幅2分岐プログラムに限定し、上界と一致する下界証明とそれを達成する手法の構築を試みたが、達成することはできなかった。 次に、MOD2素子（素子に入力される1の数が奇数のときに1を出力する素子）とAND素子、OR素子、NOT素子を用いた定数段数回路において近年証明された多数決関数の下界と上界の証明技法の理解と探究を行った。MOD2素子が多数決関数を計算するために利用できることは理解したが、現状の技法だけでは上界をさらに下げることは困難であることを理解した。この技法の拡張や多数決関数とパリティ関数（MOD2関数）との関係性のさらなる探求が今後の課題であると考えられる。 これらの研究の過程で、線形サイズの幅2分岐プログラムの充足可能性問題に対して、全探索アルゴリズムよりも指数的に高速なアルゴリズムを設計することができた。
• 強指数時間仮説に基づく計算限界の理解と探究

  日本学術振興会：科学研究費助成事業 学術変革領域研究(A)

  研究期間 : 2021年09月 -2023年03月 

  代表者 : 脊戸 和寿

   

  本研究の目標は強指数時間仮説の知見を深め、将来的に仮説の否定につなげるための研究を遂行することである。そのため、2021年度は既存研究の調査を行い、強指数時間仮説下における計算限界の結果をまとめることを目標とした。既存研究の調査は概ね終了したが、全体を手軽に参照できる形でまとめることはできていない。調査の過程で、強指数時間仮説よりも強い仮説（Super Strong Exponential Time Hypothesis：SSETH）について調査を進めることがあり、この仮説を否定することが直近の目標になることを確認した。 SSETH とは節内の変数の数が高々、k 個に制限された和積標準形論理式の充足可能性問題において、既存の最速アルゴリズムの計算時間より真に高速なアルゴリズムは存在しないという仮説である。これは強指数時間仮説よりもかなり強い仮説であり、これをまず否定するために新たなアルゴリズム設計を行うことが重要であると考え、SSETH に関する研究を実施したが、既存アルゴリズムの計算時間の改良には至らなかった。しかし、既存の最速アルゴリズムが苦手なインスタンス集合に対しては、別のアプローチで高速に解けることがわかった。 また、充足可能性判定アルゴリズムの設計技法の理解のために、幅2分岐プログラムの充足可能性判定アルゴリズムの設計を試みた。その結果、幅２分岐プログラムのノード数が入力変数の個数の線形個であれば、全探索よりも指数的に高速なアルゴリズムを設計することができた。さらなる高速化の手法への検討も既に行なっており、別の充足可能性判定問題を解く必要があることを確認している。
• 強指数時間仮説の反証にむけた研究

  日本学術振興会：科学研究費助成事業 基盤研究(C)

  研究期間 : 2018年04月 -2021年03月 

  代表者 : 脊戸 和寿, 長尾 篤樹

   

  本研究では強指数時間仮説の反証に向けた基礎研究を行うことを目的としている． 節の長さが無制限である和積標準形の充足可能性問題には，全探索より指数的に高速なアルゴリズムが存在しないという仮説である強指数時間仮説が知られている．この仮説下では，一部の多項式時間アルゴリズムや指数時間がアルゴリズムが，現在知られている計算時間から改良が不可能であることが示されている． 本研究では，論理関数がどのような構造を持てば全探索よりも指数的に高速なアルゴリズムを構築できるかを明らかにし，仮説の反証の障壁を見出すことを目標としている．特に既存研究で行われてきた論理回路の充足可能性問題ではなく，分岐プログラムの充足可能性問題を中心に研究を行っている． 節の長さが無制限である和積標準形は幅2分岐プログラムで表現することが可能であり，分岐プログラムはグラフの形式で表現できるため，何らかの構造を見出すことが可能ではないかと考えている． 本年度は，既存のk回読み分岐プログラムの充足可能性判定アルゴリズムについて，k=3の場合にはさらに高速なアルゴリズムが存在することを示し，国際論文誌に投稿した．また，前年度に構築した線形サイズの幅2分岐プログラムの充足可能性判定アルゴリズムを改良し，同じ計算時間で充足解の個数を計算可能なアルゴリズムを構築した．これらのアルゴリズムは全探索よりも指数的に高速なアルゴリズムである．また，幅3分岐プログラムの特殊ケースである幅3置換分岐プログラムにおける充足可能性問題のアルゴリズム構築に取り組み始めた．
• 回路計算量の下界証明におけるアルゴリズム的手法の研究

  日本学術振興会：科学研究費助成事業 若手研究(B)

  研究期間 : 2014年04月 -2017年03月 

  代表者 : 脊戸 和寿

   

  理論計算機科学分野における最大の未解決問題であるP vs. NP問題の解決に向け，充足可能性問題のアルゴリズム設計による回路計算量の下界証明の研究を行った．本研究では閾値素子を一定数含む定数段数論理回路の充足可能性問題に対して，全探索よりも真に高速なアルゴリズムを設計することに成功した．また付随する結果として，最大充足可能性問題の新たなアルゴリズムが得られた．
• 情報理論・符号理論からの計算限界研究

  日本学術振興会：科学研究費助成事業 新学術領域研究(研究領域提案型)

  研究期間 : 2012年06月 -2017年03月 

  代表者 : 河原林 健一, 脊戸 和寿, 玉置 卓, 伊藤 大雄, 吉田 悠一

   

  情報理論・符号理論など離散数学における最先端の解析手法を使いこなし発展させることで, 計算限界解明の研究を進展させた. 具体的には(1) 劣線形時間計算における定数時間検査可能性の特徴付けや論理回路クラスの分離等, 種々のP対NP問題の類似の解決,(2) 3彩色問題に対する多項式時間近似アルゴリズムの世界記録更新等, グラフや制約充足問題に関する基本的な計算問題の計算複雑性の精微な解析,(3) (1)(2) の成果に基づいた, 劣線形時間計算やグラフアルゴリズムの機械学習や大規模データ処理等の分野への応用, が挙げられる.
• データの巨大化から生じる不完全情報への対処に主眼をおいた近似計算

  日本学術振興会：科学研究費助成事業 基盤研究(A)

  研究期間 : 2013年04月 -2016年03月 

  代表者 : 岩間 一雄, エイビス デイビッド, 宮崎 修一, 玉置 卓, 伊藤 大雄, 堀山 貴史, 吉田 悠一, 岡本 和也, 脊戸 和寿, 川原 純, 上野 賢哉

   

  不完全情報をいかに扱うかが現代アルゴリズムの大きな課題になっている． 本研究では「データの巨大化から生じる不完全情報に対処するための近似計算における，できるだけ一般性の高いアルゴリズム設計理論の体系化」を目的として研究を行った． 結果として，グラフ問題，アルゴリズム的ゲーム理論，乱化に関する基礎理論の様々な問題において，情報の不完全性を克服できるアルゴリズムの設計と解析に成功した．
• 証明の複雑さにおけるグラフ理論的手法の構築

  日本学術振興会：科学研究費助成事業 研究活動スタート支援

  研究期間 : 2010年 -2011年 

  代表者 : 脊戸 和寿

   

  理論計算機科学分野における大きな未解決問題の1つに, NP対coNP問題があげられる.この問題に対する重要なアプローチ法に証明の複雑さの研究がある.本研究では,既存の論理式に対する証明系に焦点をあてた研究ではなく,グラフに対するグラフ計算論法を用いた研究を行い,証明系とグラフ計算論法の計算能力における関係を得ることに成功した.また,対象としたグラフ計算論法をシミュレートする列挙アルゴリズムを実装し実際に実験を行った.

教育活動情報

主要な担当授業