FIT2018（第 17 回情報科学技術フォーラム）A-002
充足可能性問題への変換を用いた重み付き仮説推論の高速化
An Efficient Algorithm for Weighted Abductive Reasoning by Converting into SATProblem
佐々木 耀一 †前原 貴憲 ‡赤崎 拓未 ‡
山本 風人 †
Yoichi Sasaki Takanori Maehara Takumi Akazaki Kazeto Yamamoto
1. はじめに
仮説推論とは，与えられた観測に対し，最良の説明を求める推論である．仮説推論は，観測情報に対する事前知識に基づいた理解や思考を自然な形でモデル化できることから，プラン認識や談話解析など人工知能の分野の様々な研究において，古くから研究がなされてきた[5, 10, 1]．近年においても，知識獲得技術の成熟により大規模知識を用いた仮説推論を実問題へ適用する土壌が整いつつあることや，計算機性能の向上や効率的な推論アルゴリズムが提案されたことで，大規模知識を用いた推論が計算量の面でも実現可能になってきたことなどにより，再び注目を浴びつつある [15, 11, 4]．
しかしながら，仮説推論における計算効率の問題は，未だ完全には解決されていないのが現状である．背景知識や観測の規模が大きくなるほど仮説推論の計算コストは組み合わせ的に増大していくため，より大規模な背景知識を用いた推論を行うためには，更なる推論の高速化が必要とされる．
上記の理由から，本研究の目的は，仮説推論の一種である重み付き仮説推論のさらなる高速化を行うことにある．
本研究の貢献として以下の 2 点が挙げられる．

• 重 み 付 き 仮 説 推 論 を SAT 問 題 の 一 つ で あ る
Weighted Partial MaxSAT 問題に帰着するアルゴリズムを提案．
• 計算機実験より提案アルゴリズムの有用性の確認．
提案手法は，ILP への定式化に基づく仮説推論に関する既存手法 [7, 8, 6] における ILP への変換手続きを基に，SAT 問題への変換を行なう．これは，近年の高速な SAT ソルバの開発や，SAT 変換後の制約論理式の特性から，高速化が期待される手法である．
また，実験結果より，提案手法は推論の探索空間が大きい場合には既存手法と比べて約 50 倍の高速化が行われたことを確認した．

2. 背景
2.1. 仮説推論
仮説推論とは，与えられた観測に対して最も良い説明を求める推論である．より一般的には以下のように定義される．
定義 1. 仮説推論では，入力として，背景知識 B ，観測 O が与えられたときに，集合 Shyp = {H|H ∪ B |=O, H ∪ B 6|=⊥} の中で，最良の仮説 Hopt ∈ Shyp を出力する．
† NEC セキュリティ研究所‡ 理化学研究所 革新知能統合研究センター

定政 邦彦 †Kunihiko Sadamasa

本論文では，上の条件を満たす集合 Shyp を候補仮説集合，H ∈ Shyp を候補仮説と呼び，最良の仮説 Hoptを解仮説と呼ぶ．候補仮説集合から解仮説を選択する
際の評価指標はどの仮説推論を用いるかによって異なるが，本研究では仮説推論の代表的な一つである重み付き仮説推論 [5] を用いる．
重み付き仮説推論では，背景知識 B はホーン節の一階述語論理式の集合で与えられる．また，前件の各リテラル Pi には，正の実数の重み w(pi ) が割り当てられw(p )w(p )w(p )ている．つまり，(p1 1 ∧ p2 2 . . . pn n ⇒ q) ∈ Bのように表すことができる．観測 O，候補仮説 H ，解仮説 Hopt はリテラルの連言の形をした論理式で表される．また論理式中の全ての論理変数は存在限量されていて，さらに全ての各リテラルは正の実数のコストを持つ．直観的な解釈としては，リテラルのコストが大きければそのリテラルはより不確かであることに対応する．
候補仮説集合 Shyp は，与えられた観測 O に対し，背景知識 B が含むホーン節のルールを後ろ向きに適用していくことにより生成される．この操作を後ろ向き推論と呼ぶ．例えば，任意の候補仮説を H 0 としたときに，X ⊂ H 0 に対して，背景知識 B が含む P ⇒ Xを後ろ向きに適用した場合，H 0 中の X の代わりに Pを加えた新たな候補仮説 H 00 を生成する．
さらに，任意の候補仮説 H 0 に含まれる同じ述語を持つ 2 つのリテラル l(x1 , . . . , xn ) と l(y1 , . . . , yn ) に対し，引数の等価関係 x1 = y1 , . . . , xn = yn を与えると同時に，重みがより大きいコストをもつリテラルを H 0から消去する単一化と呼ばれる操作を行うことにより，新しい候補仮説 H 00 を生成する．
また，解仮説 Hopt を候補仮説集合 Shyp の中から選択する際に用いる指標として，重み付き仮説推論ではある候補仮説 Hi に対するコスト c(Hi ) = Σh∈Hi c(h)は，最もコストが最小な候補仮説を解仮説とする．ただし c(h) はリテラル h に割り振られるコストを表す．
候補仮説集合 Shyp を生成した後に，全ての候補仮説
H ∈ Shyp に対しナイーブにコストを計算することで，解仮説を求めることができる一方で，計算コストが問題となる．
2.2. 関連研究
一階述語論理に対する仮説推論の高速化として，Markov Logic Networks[13] や Bayesian Logic
Programs[12] などの演繹推論モデルの上で実現する方法が提案されている [2, 14, 12] ．これらの手法は，機械学習の分野で培われた高速な最適化アルゴリズムを流用することにより推論速度を向上することを目指したものの，大規模データへの適用には難しいことが知られている [2]．

69
第 1 分冊Copyright © 2018 by
The Institute of Electronics, Information and Communication Engineers andInformation Processing Society of Japan All rights reserved.

FIT2018（第 17 回情報科学技術フォーラム）さらなる高速化手法として，Inoue ら [7, 6] が提案した整数線形計画法 (Integer Linear Programming, ILP)に基づく仮説推論 (ILP-formulated Abduction) が挙げられる．これは，仮説推論において最良の仮説を導出する計算処理を，ILP 問題における最適解を求める処理として定式化することで，外部の高速な ILP ソルバを利用することができ，効率的な仮説導出を可能にした．
より具体的な変換処理としては，まず始めに，候補仮説集合 Shyp を生成した後に，Shyp に含まれる全てのリテラルに対して，0-1 の ILP 変数を導入する．その後，解仮説を求める際に候補仮説となる条件を，ILP変数を用いた不等式制約として記述し，各リテラルが持つコストを，ILP 問題の目的関数内の ILP 変数の係数に対応させることで，ILP 問題への変換を実現する．
さらに Inoue らは，ILP-formulated Abduction において生成される ILP 制約の大半が変数の等価関係について成り立つ推移律に関する制約であることに着目し，それらの制約に対して Cutting Plane Inference と呼ばれる，最適化を繰り返しながら徐々に制約を追加していく手法を適用することにより，ILP-formulatedAbduction の推論効率を大きく改善する手法を提案している [8]．
また，Yamamoto ら [17] は，ILP-formulated Abduction の計算負荷が候補仮説の数に強く依存していることに着目し，背景知識に含まれる述語間の関連度を事前に推定しておき，関連度を用いて候補仮説の探索を行なうことによって，解の候補として冗長な候補仮説を除外し，推論を効率化する手法を提案している．

2.3.Weighted Partial MaxSAT
本小節では，提案アルゴリズムに用いる Weighted
Partial MaxSAT を説明する．
始めに，MaxSAT（最大充足割当問題）とは，連言標準形 (Conjunctive Normal Form, CNF) で書かれた論理式内の論理変数に対して，満たす節 (clause) の数が最も多くなるような真偽値（T rue, F alse）割り当てを求める問題である．ここで CNF とはリテラル xi,j にVW対し，xi,j の形式をした論理式のことである．例えば，(A ∨ B) ∧ (¬B ∨ C ∨ ¬D) ∧ (D ∨ ¬E) のような論理式は CNF である．次に，Weighted MaxSAT とは，CNF で書かれた論理式内の節に重みが与えられている場合に，論理式内の変数に対して，満たす節の重みの和が最も大きくなるような真理値割り当てを求める問題である．また提案アルゴリズムで用いる，WeightedPartial MaxSAT とは，前述の Weighted MaxSATに対し，必ず満たさなければいけない節 (hard) と満たさなくても構わない節 (soft) を考えた最適化問題である．より厳密には以下のように定義される．

3.Weighted Partial MaxSAT に基づく仮説推論
本節では，2.2 節で述べた Inoue ら [7] の ILP 問題への変換を用いたアルゴリズムに対し，2.3 節の Weighted
Partial MaxSAT への変換を用いたアルゴリズムを提案する．まず始めに，候補仮説集合 Shyp を生成した後に，Shyp に含まれる全てのリテラルに対して，論理変数 (True-False) を導入する．次に，解仮説を求める際に候補仮説となる条件を，論理変数を用いた論理式を導出し，hard な節として記述する．また，各リテラルが持つコストを，Weighted Partial MaxSAT の soft な節の重みに対応させる．変換により与えられた，hard節と soft 節で表される Weighted Partial MaxSAT に対して SAT ソルバを用いて最適解を求めることで，解仮説を導く．3.1 節で候補仮説としての条件を満たすた
めの hard な論理式の構築方法を具体的に与え，3.2 節で soft な論理式の構築方法を与える．
3.1.hard 節
候補仮説集合内に含まれる各リテラルに対して，以下の条件で真偽値が割り当てられる論理変数を導入する．以降では p, q を候補仮説集合内の任意のリテラルとする．

• hp : リテラル p を候補仮説に含む場合は，T rue．
• rp : リテラル p がコストを払わない場合は，T rue．
• up,q : リテラル p がリテラル q と単一化される場合
は，T rue．
Inoue ら [7] の ILP 変換アルゴリズム内で述べられている候補仮説となる条件に対し以下のように論理式制約を与える．まず始めに命題論理の範囲に関する制約を与える．
• 制約 1: 各 p ∈ 観測 O に対し 制約論理式：hp
この制約は，”観測に含まれるリテラルは常に含まれるか，候補仮説に説明されている”ことを表す．

• 制約 2: 各Wp ∈ 仮説 P に対し
W 制約論理式：・¬rp ∨ ( e∈expl(p) he ) ∨ ( q∈sml(p) up,q )WW・( a∈and(p) ha ) ∨ ( a∈and(p) ¬ha )ここで，expl(p) = {e|e ∈ P, e ∨ B |= p}，sml(p) ={q|q ∈ P, c(q) < c(p)} とする．ここで，and(p) は p を説明しうるリテラルで，and でつながっているリテラ
ル a ∈ P を表す．
制約 2 は，順に”仮説に含まれるリテラルがコストを払わないときは，そのリテラルがほかのリテラルに説
定義 2. Weighted Partial MaxSAT とは CNF の論理式
Φ ={(C1 , w1 ), . . . , (Cm , wm ),(Cm+1 , ∞), . . . , (Cm+m , ∞)}明されているときか，単一化するときである．” ”説明する可能性があるリテラルが and でつながっている場が与えられたときに，偽となる節の重みの和が最小と合は全て候補仮説に含むか全て含まないかである．”こなるような真理値割り当てを求める問題である．ただし，Φ の各要素は節 C と節に対する重み w を表し， とを表す．
ii

最初の m 個の節は soft，それに続く m0 個の節は hardである．

• 制約 3: 各 p, q ∈ 仮説 P に対し(¬up,q ∨ hp ) ∧ (¬up,q ∨ hq )70
第 1 分冊

制約論理式：

Copyright © 2018 by
The Institute of Electronics, Information and Communication Engineers andInformation Processing Society of Japan All rights reserved.

FIT2018（第 17 回情報科学技術フォーラム）この制約は”単一化されるときは，単一化されるリテラルはすべて仮説されている”ことを表す．
次に一階述語論理の範囲に関する制約を与える．変数の集合を V ，定数の集合を C で与える．新しい論理変数として，リテラルの引数の変数 x ∈ V と，リテラルの引数の定数または変数 y ∈ (V ∨ C) について

sx,y =T rue
F alse

表 1: 候補仮説集合内のリテラルの数
データ 推論の深さ リテラルの数
事例 1

事例 2

(x に y が代入されるとき)(それ以外)

3
510
35101490
16022170
3973
546113501を与える．

• 制約 4: リテラル p と q を単一化する際に必要な変数代入の組集合 usub(p, q) に対し 制約論理式：
Vup,q ⇒ {x,y}∈usub(p,q)
この制約は”単一化されるリテラルの引数は全て等しい”ことを表す．

• 制約 5:|U | |U | _^sx,ui=0 j=0j

¬sx,uj(i = j)(i 6= j)

制約 5 は，”一つの変数に複数の定数が同時に割り当てられることはない”ことを表している．

• 制約 6:・¬sx,y ∨ ¬sy,z ∨ sz,x・¬sz,x ∨ ¬sx,y ∨ sy,z・¬sy,z ∨ ¬sz,x ∨ sx,y
これらは三変数間の推移律を表している．
上記の制約 1 から制約 6 を CNF 形式の論理式 Φhardに変換し，Weighted Partial MaxSAT の入力の hard
節として与える．
3.2.soft 節
本小節では，候補仮説のコストの最小化と Weighted
Partial MaxSAT の soft 節での表現の対応付けを与える．2.1 節で述べたように候補仮説集合 Shyp に含まれる候補仮説 Hi に対し，コスト c(Hi ) = Σh∈Hi c(h) が最も小さい候補仮説を解仮説として求める．
これは，3.1 節で定義した各リテラル p が持つ論
理変数 hp , rp に対し，soft な制約論理式 Φsof t =Wp∈Shyp (¬rp ∧ hp , c(p)) を Weighted Partial MaxSATの入力として与えることと等価である．

4. 計算機実験
本節では，3 節で提案した手法の有効性を評価するために実施した計算機実験の結果について報告する．
4.1. データ
今回の実験で使用する，背景知識 B と観測 O のデータは人工的に作成した．事例 1 と事例 2 の二つを用意し，それぞれのサイズは以下の通りである．

• 事例 1 背景知識 B のルール数：215，述語数：390，観測 O のリテラル数：2078• 事例 2 背景知識 B のルール数：215，述語数：349， 観測 O のリテラル数：2202
候補仮説集合内に含まれるリテラルの数は表 1 に示す通りである．なお推論の深さとは，候補仮説を生成する際の，観測から個々のリテラルを仮説するのに必要な後ろ向き推論の回数の最大数である．
4.2. 実験方法
上記の事例 1 と事例 2 に対して重み付き仮説推論を適用する場合において，既存手法である ILP-formulatedabduction[7](gurobi) と，提案手法 (openwbo) の計算時間を比較した．この時，推論全体に要した時間に加えて，i)gene hypo: 与えられた背景知識と観測から候補仮説集合を求めるのに要する時間，ii)conv: ILP 問
題または SAT 問題に変換する時間，iii)sol:ソルバが最適解を求めるのに要する時間，の三つの内訳に関しても調査した．
ILP-formulated abduction に は Gurobi Optimizer § と呼ばれる商用の ILP ソルバを用いた．また，提案手法には Open-WBO ¶ [9] と呼ばれるフリーなSAT ソルバを用いた．実験では，推論の深さを変化させ，候補仮説集合の大きさに関する計算時間を調べた．
4.3. 結果
事例 1 に対する実験結果を図 1 に示す．推論全体の計算時間に関して，提案手法は既存手法と比べ約 1.2 倍高速であった．また，ILP 問題,SAT 問題それぞれへの変換にかかる時間はほぼ同じであるのに対して，ソルバが最適解を求めるのに要する時間 sol のみでの比較を行うと，約 8 倍高速であった．
事例 2 に対する実験結果を図 2 に示す．推論全体の計算時間に関して，提案手法は既存手法と比べ約 7 倍から 60 倍の高速化が行われた．また，ソルバが最適解を求めるのに要する時間 sol のみでの比較を行うと，約200 倍から 400 倍高速であった．
また，これらの実験結果より，事例 1 よりも事例 2の方が，提案手法によって推論効率が大きく改善されていることが観察される．これは，事例 2 のほうが，より探索空間が大きいためであると考えられる．よって，探索空間が大きくなるほど，既存手法と比べ速度上昇が大きくなり，有用性が高くなると期待できる．

§ http://www.gurobi.com/¶ http://sat.inesc-id.pt/open-wbo/

71
第 1 分冊Copyright © 2018 by
The Institute of Electronics, Information and Communication Engineers andInformation Processing Society of Japan All rights reserved.

FIT2018（第 17 回情報科学技術フォーラム）5. まとめ
本稿では，SAT 問題の一つである，Weighted Partial
MaxSAT への変換を用いて重み付き仮説推論の高速化を行った．実験結果からは，商用の ILP ソルバとして一般的な Gurobi を用いた ILP-formulated abductionと比較を行い，提案手法は最大 50 倍の高速化が行われていることを確認した．

54.5
4

Inference time [sec]

3.5

6. 考察

32.5

2
1.5

1
0.5

0
gurobi openwbo

gurobi openwbo

gurobi openwbo

depth：3

depth：5

depth：10

gene_hypoconvsol

図 1: 事例 1 に対する実験結果.

本稿での SAT 変換を用いた提案手法の高速化に関して考察を与える．
一般的に，制約式内の変数の数を n とすると，ILP問題，SAT 問題共に最適解を求めるのに O(2n ) 時間かかる．しかし，Williams ら [16] によりホーン節に近い論理式を入力とする SAT 問題は高速に解くことができることが知られている．変数の部分集合 X が Hornbackdoor であるとは，X の真偽値を決めた際にできる論理式がホーン節になることを表す．Horn-backdoorの論理変数の数を |backdoor| とすると，backdoor の論理変数への真偽値割り当てを全通り試すと残りはホーン節となり，多項式時間で解くことができる [3] ので，O(2|backdoor| ·poly(n)) 時間となり，FPT(Fixed Parameter Tractable) アルゴリズムとなる．
一方，本問題で作られる制約式内には，O(n3 ) という膨大な推移律の制約式が生成されることが示されている [8]．また推移律に基づく制約式はホーン節の論理式を用いて等価に表現できる．
よって，本問題の扱う制約としてホーン節に関する制約式が多いことから，全体の論理変数に対し |backdoor|が少なく，重み付き仮説推論の高速化が行われたと考察できる．

2000

謝辞
1800

本研究を行うにあたり，討論頂いた NEC セキュリティ研究所の岡嶋穣氏，実験に協力いただいた NEC ソ
リューションイノベータ株式会社の福井美和氏に感謝する．

1600

Inference time [sec]

1400

1200

参考文献
1000

[1] Debra Burhans And, Debra T. Burhans, and Stuart C. Shapiro. Abduction and question answering. In Proceedings of the IJCAI-01 Workshop
on Abductive Reasoning. AAAI, 2001.

800

600
400
2000
gurobi openwbo

gurobi openwbo

gurobi openwbo

depth：3

depth：5

depth：10

gene_hypoconvsol

図 2: 事例 2 に対する実験結果.

[2] James Blythe, Jerry R. Hobbs, Pedro Domingos,
Rohit J. Kate, and Raymond J. Mooney. Implementing weighted abduction in markov logic.
In Proceedings of the Ninth International Conference on Computational Semantics, IWCS 2011,
January 12-14, 2011, Oxford, UK, 2011.
[3] William F Dowling and Jean H Gallier. Lineartime algorithms for testing the satisfiability of
propositional horn formulae. The Journal ofLogic Programming, 1(3):267–284, 1984.

72
第 1 分冊Copyright © 2018 by
The Institute of Electronics, Information and Communication Engineers andInformation Processing Society of Japan All rights reserved.

FIT2018（第 17 回情報科学技術フォーラム）[4] Andrew S. Gordon. Commonsense interpretationof triangle behavior. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence,
AAAI’16, pages 3719–3725. AAAI Press, 2016.
[5] Jerry R. Hobbs, Mark E. Stickel, Douglas E. Appelt, and Paul A. Martin. Interpretation as abduction. Artif. Intell., 63(1-2):69–142, 1993.
[6] Naoya Inoue and Andrew S. Gordon. A scalable
weighted Max-SAT implementation of propositional Etcetera Abduction. In Proceedings ofthe 30th International Conference of the Florida
AI Society (FLAIRS-30), Marco Island, Florida,May 2017. AAAI Press.
[7] Naoya Inoue and Kentaro Inui. Ilp-based reasoning for weighted abduction. In Plan, Activity, and Intent Recognition, Papers from the2011 AAAI Workshop, San Francisco, California, USA, August 07, 2011, 2011.
[8] Naoya Inoue and Kentaro Inui. Large-scale costbased abduction in full-fledged first-order predicate logic with cutting plane inference. In Logics
in Artificial Intelligence - 13th European Conference, JELIA 2012, Toulouse, France, September
26-28, 2012. Proceedings, pages 281–293, 2012.

[14] Parag Singla and Raymond J. Mooney. Abductive markov logic for plan recognition. In Proceedings of the Twenty-Fifth AAAI Conferenceon Artificial Intelligence, AAAI 2011, San Francisco, California, USA, August 7-11, 2011, 2011.
[15] Jun Sugiura, Naoya Inoue, and Kentaro Inui.
Recognizing implicit discourse relations throughabductive reasoning with large-scale lexical
knowledge. In Proceedings of the 1st Workshop on Natural Language Processing and Automated Reasoning (NLPAR), number 1044 in
CEUR Workshop Proceedings, pages 76–87, ACorunna, Spain, 2013.
[16] Ryan Williams, Carla P Gomes, and Bart Selman. Backdoors to typical case complexity. In IJCAI, volume 3, pages 1173–1178. Citeseer, 2003.
[17] Kazeto Yamamoto, Naoya Inoue, Kentaro Inui,
Yuki Arase, and Jun’ichi Tsujii. Boosting the efficiency of first-order abductive reasoning using
pre-estimated relatedness between predicates.
International Journal of Machine Learning andComputing, 5(2):114–120, 2015.

[9] Ruben Martins, Vasco Manquinho, and InêsLynce. Open-wbo: A modular maxsat solver.
In Carsten Sinz and Uwe Egly, editors, Theoryand Applications of Satisfiability Testing – SAT
2014, pages 438–445, Cham, 2014. Springer International Publishing.
[10] Hwee Tou Ng and Raymond J. Mooney. Abductive plan recognition and diagnosis: A comprehensive empirical evaluation. In Proceedingsof the Third International Conference on Principles of Knowledge Representation and Reasoning,pages 499–508, Cambridge, MA, October 1992.
[11] Ekaterina Ovchinnikova, Andrew S. Gordon, andJerry R. Hobbs. Abduction for Discourse Interpretation: A Probabilistic Framework. In Proceedings of the Joint Symposium on Semantic
Processing, pages 42–50, November 2013.
[12] Sindhu Raghavan and Raymond J. Mooney.
Bayesian abductive logic programs. In Statistical
Relational Artificial Intelligence, Papers from the2010 AAAI Workshop, Atlanta, Georgia, USA,
July 12, 2010, 2010.
[13] Matthew Richardson and Pedro M. Domingos.
Markov logic networks. Machine Learning, 62(12):107–136, 2006.

73
第 1 分冊Copyright © 2018 by
The Institute of Electronics, Information and Communication Engineers andInformation Processing Society of Japan All rights reserved.