成 膜 大 学 理 工 学 研 究 報 告
J,Fac,Sci,Tech.,Sei/keiUniv.
Vol.49No.2(2012)pp.51-54
充 足可 能 性 問 題 の アル ゴ リズ ム
山 本
真 基1
Algorithms
for the satisfiability
problem
Masaki
Yamamoto'
ABSTRACT
: The satisfiability problem (SAT problem for short) is a computational problem, such as the
traveling salesman problem. It is a fundamental problem in theoretical computer science. We present the
background of the SAT problem as well as typical algorithms for solving the problem. The main purpose
of this paper is to introduce one of my research work.
Keywords
: algorithm,
satisfiability
problem,
NP-hard
1.充
足 可 能 性 問 題 と は?
充 足 可 能 性 問 題(satisfiabilityproblem,以 下,SAT
問 題 と 略 す)と は,理 論 計 算 機 科 学 で 最 も 基 本 的 で 重 要
なNP完 全 問 題 の 一 つ で あ る 。 グ ラ フ 理 論 に お け る 巡 回
セ ー ル ス マ ン 問 題,頂 点 彩 色 問 題,独 立 頂 点 集 合 問 題,
オ ペ レ ー シ ョ ン ズ ・ リサ ー チ に お け る 整 数 計 画 問 題 ゲ
ー ム ・パ ズ ル に お け る 数 独 ,テ ト リス な ど,実 社 会 で 遭
遇 す る 多 く の(決 定)問 題 がNP完 全 問 題 で あ る 。 そ の
中 で も,SAT問 題 は,そ のNP完 全 性 が 示 さ れ た 最 初
の 問 題 で あ る 。 以 下 の 意 味 で,SAT問 題 はNP完 全 問
題 の 根 本 で あ る 。
す べ て のNP完
全 問題 のNP完
全 性 は,(い
くつ か の 例 外 を除 い て)SAT問
題 か らの
有 限 回 の 多 項 式 時 間 還 元 を経 て 示 され た 。
題 か らの 多 項式 時 間 還元 を示 す こ とが で き るは ず だ が,
証 明 が よ り複 雑 に な る こ とで し ょ う。)
SAT問
題 は,以 下 の よ うな 問題 で あ る。
・入 力:和 積 標 準 形(conjunctivenormalforrn:CNF)論
理 式 ψ
・質 問:ψ は 充 足 可 能 か?
こ こ で,「CNF論 理 式 ψ が 充 足 可 能 で あ る 」 と は,「 ψ
を1(tme)に させ る よ うな ψ の 変 数 へ の0/1割 り 当 て
が 存 在 す る 一 こ と を 指 す 。 例 え ば,論 理 変 数 荷,ろ,る,
x4,x5上 の 以 下 の よ う なCNF論 理 式,
ψ=Xl(Xl>T2)(Xl>X2>M3)(X2>X3>N,)
(x3>x4>M5)(Xl>x2>x3>x4>x5).
例 え ば,教 科 書[1]で
は,ハ
ミル トン 閉 路 問題 は 頂 点 被
覆 問題 か らの 多 項 式 時 間 還 元 に よ り,更 に,頂 点 被 覆 問
題 はSAT問
題 か らの 多 項 式 時 間 還 元 に よ りNP完
全 性
が 示 され て い る。 更 に,ハ ミル トン閉 路 問 題 か らの 多 項
式 時 間還 元 が 示 され るNP完
全 問題 も数 多 く存 在 す る。
(も ち ろん,SAT問
題 か らの 直 接 の 還 元,更 に は,S
AT問
題 のNP完
全 性 が 示 され た よ うに,任 意 のNP問
が 入 力 と し て 与 え られ た とす る 。 こ こ で,死 は 濯 の 否
定 を 表 す 。 ま た,ψ を 構 成 す る 一 つ 一 つ の(卍 〉,_)
を 節 と 呼 ぶ 。(上 の ψ の 表 記 に お い て,節 と節 と の 間 の
AND記 号 く は 省 略 され て い る 。)こ の 場 合,上 の ψ は
充 足 可 能 で あ る 。 な ぜ な ら,変 数 荷,あ,あ,曲,萌 へ
の 割 り 当 て を,(Xl,X2,κ3,X4,X5)=(1,1,1,1,1)と し た 場
合,ψ の そ れ ぞ れ の 節 は1と な り,そ れ ゆ え ψ が1と
な る か ら で あ る 。 一 方,
1情 報 科 学 科 准 教 授(y㎜ ㎜oto@st
.seikei.ac.jp)
一51一
成 践 大 学 理 工 学 研 究 報 告
Vol,49No.2(2012.12)
q=a,(Xl>72)(Xl>X2>M3)(X2>X3>M,)
(x3>x4>75)(Xl>x2>x3>x4>x5),
/(-SAT問 題 に つ い て,以 下 の 基 本 的 な 事 実 が 知 ら れ て い
る 。
の 場 合,こ の ψ は 充 足 不 可 能 で あ る 。(な ぜ な ら,ど の
よ うな 割 り 当 て に 対 し て も ψ が1に な らな い の で 。)
任 意 の 整 数1(≧3に 対 し て,/(-SAr問 題
はNP完 全 で あ る 。
2.SAT問
題 を 解 くア ル ゴ リズ ム
で は,こ の よ うな 根 本 的 な 問題 を ど うや っ て(ど の よ
うな ア ル ゴ リズ ム で)解 い た ら よい で し ょ うか?SAT
問 題 はNP完
全 問題 で あ るか ら,多 項 式 時 間 で 解 く こ と
は か な り難 しい こ とで し ょ う。 現 実 的 で はな い が,指 数
時 間 か け て も よい とす る と,以 下 の よ うな 全 探 索 ア ル ゴ
リズ ム がSAT問
題 を解 く こ と分 か る。
bruteforce(f)
{
fbreacht∈{0,1}〈n
if(fが 割 り 当 てtに よ り 充 足 す る),
thenoutputYES
outputNO
}
こ こ で,〃 をCNF論 理 式fの 変 数 の 個 数 と す る 。 こ
の ア ル ゴ リズ ム の(最 悪)計 算 時 間 は0(lqレ2n)と な
る 。(以 降 で は,指 数 時 間 に お け る 多 項 式 要 素 は 省 略 し て
表 記 す る 。 例 え ば,0(IqI・2n)は 〃(2n)と 表 記 さ れ
る 。)で は,SAT問 題 を,例 え ば,〃(1.gggggn)時
間 で 解 く こ と は で き な で い だ ろ うか?残 念 な が ら,今(2
012年8月)の と こ ろ,そ の よ うな ア ル ゴ リズ ム は 見
つ か っ て い な い 。
そ の よ うな 一 般 のSAT問 題 で は な く,以 下 の よ うな
SAT問 題 の 特 殊 な 問 題,!(-SAT問 題,な ら ば そ れ が 可
能 で あ る 。
よ っ て,SAT問 題 と 同 様,/(≧3で あ れ ば,1(-SAT問
題 を 多 項 式 時 間 で 解 く こ と は か な り難 し い こ と で し ょ う。
(一 方,2-SAr問 題 は 多 項 式 時 間 計 算 可 能 で あ る こ と が
示 さ れ て い る 。)し か し,々 が 定 数 で あ れ ば,少 し 工 夫
す る こ と に よ り,/(-SAr問 題 を 〃((2-E)n)時 間 で 解
く こ と が で き る(E>0は/(に 依 存 し た 正 の 定 数)。
s㎞ple
_ksat(f)
{
if(fが 充 足 し て い る),thenoutputYES
if(fが 充 足 し て い な い),thenret㎜
}
fの 任 意 の 節Cを 選 ぶ
tk)reacha∈{0,1}〈k
if(Cがaで 充 足 す る),
thensimple
_ksat(fIa)
こ こ で,flaと は,fに 割 り 当 てaを 適 用 し て 得 ら れ る
論 理 式 の こ と で あ る 。 簡 単 な 漸 化 式 を 解 く こ と に よ り,
こ の ア ル ゴ リ ズ ム の 計 算 時 間 が 〃((2k-1)n/k)と な る こ
と が 分 か る 。(1(=3の 場 合 は,〃(Lgl3n)と な る 。)
上 の ア ル ゴ リ ズ ム を 少 し 改 良 す る こ と に よ り,よ り 高
速 の ア ル ゴ リ ズ ム が 得 ら れ る 。
s㎞ple
_ksat2(f)
{
if(fが 充 足 し て い る),thenoutputYES
if(fが 充 足 し て い な い),thenret㎜
・ 入 力;1( -CNF論 理 式 ψ
・ 質 問:ψ は 充 足 可 能 か?
こ こ で,!(-CNF論 理 式 と は,節 の 大 き さ が 高 々!(で
あ るCNF論 理 式 の こ と で あ る 。 例 え ば,以 下 の ψ は
3-CNF論 理 式 で あ る,
}
ψ の 任 意 の 節Cを 選 ぶ
//ア ル ゴ リ ズ ム の 記 述 を 簡 略 化 さ せ る た め,
//Cが す べ て 正 の リ テ ラ ル か ら 成 る と す る
fori:0<=i<=ICI-l
a=10〈i
simple _ksat2(fIa)
q=κ1(Xl>af2)(Xl>κ2>llf3)(X2>X3>af4)(X3>κ4>lil5).
上 のfbr文 で は,例 え ば,任 意 に 選 ん だ 節CがC=(Xl
一52一
成 践 大 学 理 工 学 研 究 報 告
Vol,49No.2(2012.12)
>x2>x3)の 場 合,d=1,10,100に よ る3つ の 再 帰
呼 び 出 しsimple _ksat2(fIa)が 実 行 さ れ る 。簡 単 な 漸 化
式 を 解 く こ と に よ り,こ の ア ル ゴ リ ズ ム の 計 算 時 間 が 〃
(cn)(cは 方 程 式 ■k-■k-1-… 一 ■2-■-1=0
を 満 た す 唯 一 の 正 の 実 数 解)と な る こ と が 分 か る 。(沌=
3の 場 合 は,〃(1.841n)と な る 。)
以 上 の 二 つ は,分 枝 限 定 法 と 呼 ば れ る ア ル ゴ リズ ム で
あ る.こ れ 以 外 に も,以 下 の よ うな 局 所 探 索 法 と 呼 ば れ
る ア ル ゴ リズ ム も あ る.
local _search(f)
{
a∈{0,1}〈nを ラ ン ダ ム に 選 ぶ
}
repeatNtimesdo{
if(fがaで 充 足),outputYES
aで 充 足 し て い な い 節Cを 任 意 に 選 ぶ
Cの 変 数xを ラ ン ダ ム に 選 ぶ
aに お け るxの 割 り当 て を 反 転 す る
}
outputNO
こ こ で,Nは 繰 り返 し 回 数 を 表 す パ ラ メ ー タ で あ る 。 入
力fが!(-CNF論 理 式 で あ れ ば,Nを(2(1(-1)/lt)nに 設
定 す る こ と に よ り,高 い 確 率(1-1/n》O.999)でf
の 充 足 可 能 性 を 判 定 で き る こ と が 証 明 さ れ て い る[2]。
以 上 よ り,1(-SAr問 題 は,明 ら か な 計 算 時 間 〃(2n)
よ り も 高 速 に 解 け る こ と が 分 か っ た 。で は,!(-SAT問 題
は ど の く ら い 高 速 に 解 く こ と が で き る の だ ろ うか?現 在
(2012年8月)の と こ ろ,最 速 の(決 定 性)ア ル ゴ
リズ ム の 計 算 時 間 は,〃((2(1(-1)/!t)n)と な っ て い
る[3]。(こ の 式 に1(=3を 代 入 す る と,3-SAr問 題 は 〃
(L3334〃)で 解 け る こ と に な る 。)特 に,3-SAT問 題 に
対 し て は さ ら な る 高 速 化 が 図 ら れ,最 速 は0(L3303〃)
と な っ て い る[4]。(更 に,「 乱 択 」 ア ル ゴ リズ ム を 使 う こ
と に よ り,さ ら な る 高 速 化 が 図 ら れ て い る 。 例 え ば,
3-SAT問 題 を 解 く 最 速 の 乱 択 ア ル ゴ リ ズ ム の 計 算 時 間
は,〃(L308n)と な っ て い る[5]。)
3.な
ぜ,SAT問
題 を 解 く(指 数 時 間)ア
ル ゴ リ
ズ ム を 研 究 す る の か?
理 論 計 算 機 科 学 の 分 野 に,「Pv.S.NPと い う大 き
な 未 解 決 問 題 が あ る 。問 題 ク ラ スPがNPに 真 に 包 含 さ
れ て い る か ど うか を 問 う問 題 で あ る。(詳 し く は,教 科 書
[7]な ど を 参 照 。)現 在(2012年8月),多 く の 研 究
者 がP≠NPと 予 想 し て い る 。 つ ま り,SAT問 題 や
/(-SAT問 題 が 多 項 式 時 間 で は 解 け な い と予 想 さ れ て い
る 。 ア ル ゴ リ ズ ム と い うの は,通 常,と り わ け 実 社 会 で
の 応 用 を 考 え た 場 合 は,多 項 式 時 間 計 算 可 能 な 問 題 に 対
し て そ の 存 在 意 義 が 認 め られ る。 で は,な ぜ,多 項 式 時
間 で は 解 け そ うに も な いSAT問 題 を 解 く(指 数 時 間)
ア ル ゴ リ ズ ム を 研 究 す る の で し ょ うか?
先 のP≠NPと い うの は あ く ま で 予 想 で あ っ て 証 明
さ れ た 事 実 で は な い が,仮 に,真 実 がP≠NPで あ っ
た とす る。 こ こ で,将 来,3-SAr問 題 を 解 く 〃(L2999〃)
時 間(決 定 性)ア ル ゴ リ ズ ム が 開 発 さ れ た と す る。(こ の
ア ル ゴ リ ズ ム をAと す る 。)更 に,将 来,コ ン ピ ュ ー一一タ
の 性 能 が 向 上 し て,指 数 時 間 か か る ア ル ゴ リ ズ ム も,あ
る 程 度 の 大 き な 長 さ の 入 力 を 扱 え る よ うに な っ た と す る 。
例 え ば,〃=1000に 対 して,〃(1.2gggn)時 間 ア ル ゴ
リ ズ ムAの 実 行 が(最 新 の ス ー一一パ ー コ ン ピ ュ ー一一タ を 使
っ て)1日 以 内 で 終 了 し た と す る 。 一 方 で,仮 に,現 在
(2012年8月)の3-SAr問 題 を 解 く最 速 の ア ル ゴ
リ ズ ム,〃(1.3303n)時 間(決 定 性)ア ル ゴ リズ ム,の
開 発 以 降 こ の 研 究 が 停 滞 し て,こ れ が 最 速 の ま ま で あ っ
た とす る。(こ の ア ル ゴ リ ズ ム をBと す る。)こ の 場 合,
L3303/L2999・:LO234よ り,ア ル ゴ リ ズ ムBの
実 行 に は,(最 新 の ス ー パ ー コ ン ピ ュ ー タ を 使 っ て も)
LO2341000日,お よ そ 三 千 年 も の 年 月 を 要 す る こ と に な
る 。(異 な る 二 つ の 指 数 関 数 の 比 も ま た 指 数 関 数 と な る!)
コ ン ピ ュ ー タ の 性 能 が 向 上 す れ ば す る ほ ど扱 え る 〃 の
範 囲 が 大 き く な り,そ れ ゆ え,二 つ の ア ル ゴ リ ズ ム の 計
算 時 間(を 表 す 指 数 の 底)が100分 の1で も 異 な れ ば,
そ の 比,す な わ ち 二 つ の ア ル ゴ リ ズ ム の 優 劣 が 顕 著 に 表
れ る。 これ が 指 数 時 間 ア ル ゴ リ ズ ム の 研 究 が 滞 っ て は な
ら な い 大 き な 理 由 で あ る 。
蛇足
先 の 未 解 決 問 題 「Pv.S.NP」 に つ い て お も し ろ い
調 査 が あ る 。2002年,WilliamGasarchが 理 論 計 算
機 科 学 者 を 対 象 に,あ る 投 票 を 行 っ た[6]。(2011年
7月 に も,彼 は 新 た な 投 票 を 募 る と し て,第2回 目 の 調
査 を 始 め た 。)そ の(2002年 の)投 票 結 果 で 注 目 す べ
き こ と は,予 想 の 明 言 を 控 え た 研 究 者 が 少 な く な か っ た
こ と で あ る 。(単 純 に,そ の 調 査 自 体 に 興 味 が な か っ た だ
け か も しれ な い が 。)更 に,BelaBollobas(ラ ン ダ ム グ
一53一
成 蹟 大 学 理 工 学 研 究 報 告
Vol.49No.2(2012.12)
ラ フ)やPaulVitanyi(コ ル モ ゴ ロ フ 計 算 量)と い っ た
そ の 分 野 の 権 威 が,大 胆 に もP=NPと 予 想 し た こ と
も 興 味 深 い 。(ど の 程 度 本 気 な の か は 分 か ら な い が 。)こ
の こ とか ら言 え る こ と は,P=NPで あ る と い う可 能
性 が 限 りな く ゼ ロ に 近 い と い う こ と で も な い こ と で あ る 。
lc-SAT問 題 を 解 く 指 数 時 間 ア ル ゴ リ ズ ム の 高 速 化 の 延
長 に,劣 指 数 時 間 ア ル ゴ リズ ム,そ し て 多 項 式 時 間 ア ル
ゴ リズ ム と,大 方 の 予 想 に 反 す るP=NPと い う可 能
性 を 追 求 す る こ と は,そ れ ほ ど 大 そ れ た こ と で も な い の
か も し れ な い 。
参考文献
[1]ComputersandIntractability:AGuidetotheTheory
ofNP-Completeness,M.RGareyandD.S.Jo㎞son,
WHFreeman&Co(Sd),1979.
[2]U.Sch6ning,AProbabilisticAlgorithmfbrk-SArand
ConstrailtSatisfactionProblems,FOCSl999.
[3]R.Moser,andD.Scheder,A血llderandomizationof
Sch6n血g「sl(-SATalgorithm,STOC2011.
[4]K.Makino,S.Tamaki,andM.Y㎜ ㎜oto,
DerandomizingHSSWalgorit㎞fbr3-SAr,
COCOON2011.
[5]THertli,3-SArFasterandSimpler-UniqueSAr
Bo㎜dsfbrPPSZHoldinGeneral,FOCS2011.
[6]W,Gasarch,TheP=?NPPoll,SIGACTNews
ComplexityTheoryColumn36,2002.
[7]S.AroraandB.Barak,ComputationalComplexity:A
modenlapproach,CambridgeUniversityPress,2009.
一54一
