高速な和積形命題論理式の含意関係判定法

質問

２つの和積形命題論理式が与えられています。
この２つの式に含意関係が成り立つか判定したいのです。
この問題はco-NP完全問題でまともにやるととても時間がかかります。そこで次のような条件を満たすアルゴリズムを考えてください。

１．アルゴリズムが含意関係がなりたつと答えたときは必ず含意関係が成り立つ。

２．アルゴリズムが含意関係が成り立たないと答えたときは含意関係が成り立ってても成り立たなくてもよい。

３．入力の多項式時間で停止する。

この条件だけだと常に含意関係が成り立たないと
答えるアルゴリズムでもOKになってしまいますが
もちろん本当に含意関係が成り立つときはなるたけ含意関係が成り立つと答えてほしいわけです。

私が考えたのは和積形の論理式ｆ、ｇがあたえられたとしてfのすべての和項に対してgにそれを含意する和項があったらgはｆを含意するというものです。
これよりもよい方法を考えてください。
よろしくお願いします。

回答No.2

bender

和積形のＳＡＴはＮＰ完全問題なので、ご指摘にあるように指数時間かかってしまうのですが、任意の i　において、g_i''　に含まれる命題記号の数がある自然数　k　より小さくなる場合のみ（十分に記号の数が少ないとき）、2のk乗の真偽値の組み合わせすべてを g_i'' 代入して、充足可能性を確認する、というつもりで「可能な場合のみ、充足可能を強引に調べる」と書きました。不明瞭な記述で失礼しました。

l_j　(0<=j<=m) に偽を代入する部分など、問題文中最後にある解法とほぼ同じ考えであるとは思ったのですが、可能な場合さらにリテラルに真値を代入することで和項が消えるので、以上のように強引にＳＡＴの解を求めることのできる場合も比較的多くなるかと考えました。式をさらに　decomposition　することなども有効かと考えたのですが、実をいうと、投稿が全くなかったので、とりあえず関心を持って問題を読んでいます、という意味をこめて投稿してみました。

専門の方にとっては、ある程度標準的な解法がある問題かもしれないと思ったのですが、ユニークな解法である程度平易なものが投稿されるかもしれないと思い楽しみにしていました。

私には他にあまりいい考えが浮かびそうにないのですが、よい解法が寄せられるとされるといいですね。

お礼

もう回答が来そうにないので締め切らせてもらいます。

回答No.1

bender

質問の回答に関心をよせていたのですが、投稿がないようなので、質問の確認の意味もこめて投稿させていただきます。

質問としては、和積形論理式 f、g が与えられたとき、論理式g=>fがトートロジーであるかを判定する発見的アルゴリズム（のうち条件１，２，３を満たすもの）を求める、ということでよいのでしょうか？

このとき、f　をn個の和項 f_1,f_2,...,f_n　の積であるとすると（f=f_1^f_2^...^f_n）、g=>f　がトートロジーとなるのは、g=>f_1, g=>f_2, ..., g=>f_n　の各式がトートロジーであることが必要十分条件になります。したがって、この問題は、「和積形命題論理式 g が任意の和項 f_i を含意するか」を判定するアルゴリズムを n回利用することで解くことができます。

そこで任意の式　g=>f_i に注目すると、g=>f_i　がトートロジーでなく偽になり得るとすると、それは　f_i　が偽、かつ　g　が真のときのみです。f_i　がm個のリテラル　l_1, l_2, ..., l_m　の和であるとすると（f_i=l_1vl_2v...vl_m）、f_i　が偽になるのは、l_1, l_2, ..., l_m　がすべて偽であるときだけなので、g　内のこれらリテラルに偽を代入した時に得られる和積形論理式 g_i'　が充足可能であるとき、またそのときのみ、g=>f_i　が偽になり得る、つまりトートロジーでない、といえることがわかります。

これらのことから、はじめに与えられた問題は、和積形論理式が充足可能であるか判定する問題（ＳＡＴ）を解くアルゴリズムを用いることで解くことができる、とわかります。

ＳＡＴのためのアルゴリズムについてはすでに深い研究がされてきたと思うのですが、私が思いつく単純なものとしては、g_i'　のリテラル l　のうち、~l　が g_i'　内に無いものに真を代入して得られるより単純な式 g_i''（g_i''=>g_i'　を満たす）に関して、それが可能な場合のみ、充足可能を強引に調べるというものです。

質問された方が書かれているアルゴリズムとあまりかわらないのですが、以上のような回答でもよいのでしょうか？　また、誤りがある場合、どなたか指摘してくださると幸いです。

お礼

回答ありがとうございます。
もう回答がつかないものとあきらめかけていました。
うれしいです。

SATに帰着されるということですが、SATを解こうとすると指数時間かかってしまいそうです。
充足可能を強引に調べるとありますが、具体的にはどのように調べるのでしょうか。