量子ウォークと古典ウォークを組み合わせた充足可能性問題の解法

横峯 大輔 (0851128)


論理式の乗法標準形を与えられた時に,その論理式に充足可能な真理値割り当てが存在するか否かを判定する問題は充足可能性問題(Satisfiability Problem, SAT)と呼ばれる. SATを解くための手法(SAT-solver)には様々なものが提案されており,その一つに量子力学に基づいたアルゴリズムである量子ウォークを用いた探索アルゴリズムがある. 量子ウォーク探索アルゴリズムはステップが経過するに従い解及び解周辺の観測確率が上昇するアルゴリズムであり,探索空間が大きい際には古典アルゴリズムと比べて効率的に解に近づくことができる. しかし,解の観測確率が十分な確率に上がるまで観測を行ってはいけないため,後半に無駄な動きができる. 一方,ランダムウォークを元にしたアルゴリズム(古典ウォーク)を用いたSAT-solverでは解に近づくことが困難であるが,解に近い初期値を与えることで比較的少ないステップ数で 解を見つけることが可能である. また,古典アルゴリズムであるため解を見つけた時点で終了となり無駄が無い.

そこで本研究では,この量子ウォーク及び古典ウォークのそれぞれのアルゴリズムが持つ特徴を活かしたハイブリッドアルゴリズムを提案した. 提案手法は以下のように動作する.

  1. 量子ウォークを一定回数行うことで解に近い値が観測されるようにする
  2. 量子ウォークの結果を観測し,観測結果を初期値として古典ウォークを行う
本提案手法を用いることで,従来手法よりも少ないステップ数で解の探索が可能であることがわかった.

本発表では,提案手法のアルゴリズムについて解説した後,提案手法をシミュレーションした結果を従来手法と比較することで評価を行う.