(57)【要約】【課題】和積形論理式の充足可能性を非常に高速に判定する方法および装置を提供する。【解決手段】入力された和積形論理式を線形不等式に変換する。この線形不等式は凸多面体を作る。凸多面体上での最小値の計算をすべての２リテラル線形式に対して行なう。凸多面体が空ならば充足不能を出力する。空でない場合は、追加できる２リテラル線形式が存在するかどうか調べる。追加できる２リテラル線形式が残っていれば、その最小値を切り上げた整数を最小値とする線形不等式を作成し、これを線形不等式の集合に追加する。追加すべき２リテラル線形式が存在しない場合には、最小値が０を超え最大値が１未満の変数が存在するかどうか調べ、そのような変数が存在すれば、充足不能を出力する。そうでなければ、各変数の最大値と最小値を出力する。【選択図】  図１
2004355038.tif 000002
【特許請求の範囲】
【請求項１】
和積形論理式を充足する変数の割り当てが存在するかどうかを判定する充足可能性判定方法であって、変数の範囲を［０，１］区間に拡張し、和積形論理式の各節に対応する線形不等式を作成し、その線形不等式が作る凸多面体で和積形論理式の充足可能性を判定する際に、凸多面体の領域の中で充足可能性判定には関係のない領域を切除し凸多面体を小さくすることで和積形論理式の充足不能性を判定することを特徴とする論理式充足可能性判定方法。
【請求項２】
凸多面体の領域の中で充足可能性判定には関係のない領域を切除する際に、線形式もしくは非線形式の凸多面体上での最小値もしくは最大値を用いて計算される値に基づいて、凸多面体の領域を切除することを特徴とする請求項１に記載の論理式充足可能性判定方法。
【請求項３】
凸多面体の領域の中で充足可能性判定に関係のない領域を切除する際に、線形式の凸多面体上での最小値もしくは最大値が非整数である場合にはその非整数を用いて計算した値で線形不等式の追加の是非を決め、その非整数に基づいて計算された値を最小値とした線形不等式を追加することで、凸多面体を切除し小さくすることを特徴とする請求項２に記載の論理式充足可能性判定方法。
【請求項４】
凸多面体の領域の中で充足可能性判定には関係のない領域を切除する際に、和積形論理式における変数が０か１のいずれかであるということに基づいて線形式の非整数最小値を切り上げた整数を最小値にした線形不等式を追加することで、凸多面体を切除し小さくすることを特徴とする請求項２または請求項３に記載の論理式充足可能性判定方法。
【請求項５】
凸多面体の領域の中で充足可能性判定には関係のない領域を切除する際に２リテラル線形式の最小値を用いることを特徴とする請求項２、請求項３または請求項４に記載の論理式充足可能性判定方法。
【請求項６】
ある変数の最小値が０を超えていてかつその変数の最大値が１未満であることで、充足可能性判定を行うことを特徴とする請求項１乃至請求項５のいずれか一つに記載の論理式充足可能性判定方法。
【請求項７】
充足解を求めるときに、上記の充足可能性判定方法を繰り返し用いて充足解を求めることを特徴とする請求項１乃至請求項６のいずれか一つに記載の論理式充足可能性判定方法。
【請求項８】
入力された和積形論理式を充足する変数の割り当てが存在するか否かを判する和積形論理式の充足可能性判定装置において、入力された論理式を、その変数の範囲を０〜１の区間に拡張し、和積形論理式の各節に対応する複数の線形不等式に変換する不等式変換部と，前記不等式変換部によって得られた複数の線形不等式によって形成される凸多面体上における最小値若しくは最大値を計算する最小（大）値計算部と、前記計算された最小値若しくは最大値に基づいて追加できる線形不等式の有無を判定する不等式追加判定部と、追加すべき線形不等式が存在しないと判断した場合に最小値が０を超えかつ最大値が１未満の変数の有無を検索する変数検索部と、追加すべき線形不等式が存在すると判断した場合に、前記最大値または最小値の値に基づいて新たな線形不等式を作成し、前記最小値計算部に出力する不等式追加部と、前記変数検索部において最小値が０を超えかつ最大値が１未満の変数がある場合には充足不能と判定し、最小値が０を超えないかまたは最大値が１未満でない変数がある場合には充足可能と判定する充足可能性判定部と、を備えていることを特徴とする和積形論理式の充足可能性判定装置。
【請求項９】
前記充足可能性判定部において充足可能と判定した場合に、充足可能とされた充足解の範囲を出力する充足解出力部と、この充足解出力部において具体的な一つの充足解が発見されない場合に、和積形論理式０か１を代入して新しい和積形論理式を計算し、この新しい和積形論理式を前記線形不等式変換部に出力する和積形論理式計算部を備えていることを特徴とする請求項８に記載の和積形論理式の充足可能性判定装置。
【請求項１０】
前記充足可能性判定部において充足可能と判定した場合に、充足可能とされた充足解の範囲を出力する充足解出力部と、この充足解出力部において具体的な一つの充足解が発見されない場合に、線形不等式に０か１を代入して新しい線形不等式を計算し、この新しい線形不等式を前記最小（大）値計算部に出力する線形不等式計算部を備えていることを特徴とする請求項８に記載の和積形論理式の充足可能性判定装置。
【請求項１１】
前記充足可能性変換部が、前記最小（大）値計算部において、凸多面体を構成する線形不等式の領域が空の場合に充足不能と判定するものであることを特徴とする請求項８、請求項９または請求項１０に記載の和積形論理式の充足可能性判定装置。
【請求項１２】
前記不等式追加部が、前記最小（大）値計算部によって得られた最小値あるいは最大値が非整数である場合に、その非整数を切り上げ若しくは切り下げて得られた整数を最小値あるいは最大値とする線形不等式を作成するものであることを特徴とする請求項８、請求項９、請求項１０または請求項１１に記載の和積形論理式の充足可能性判定装置。
【請求項１３】
前記線形不等式が、２リテラル線形不等式であることを特徴とする請求項８、請求項９、請求項１０、請求項１１または請求項１２に記載の和積形論理式の充足可能性判定装置。
【請求項１４】
前記最小（大）値計算部の出力側に、凸多面体が空かどうか調べるための凸多面体存在判定部が接続され、この凸多面体存在判定部は、凸多面体が空の場合には、その旨を前記充足可能性判定部に出力し、前記充足可能性判定部が和積形論理式が充足不能であると判定するものであることを特徴とする請求項８、請求項９、請求項１０、請求項１１、請求項１２または請求項１３に記載の和積形論理式の充足可能性判定装置。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は和積形論理式の充足可能性判定方法及びこれを実行する装置に関するものである。
【０００２】
【従来の技術】
（１）産業上の利用可能性
論理式の充足可能性問題は、次の分野で登場する。
１．ＶＬＳＩ等の論理回路の論理合成、論理検証、試験パターンの自動生成
２．人工知能の自動推論
３．スケジューリング
【０００３】
これら以外にも多くの問題が論理式の充足可能性問題として定式化される。たとえば、代表的な問題は、以下のとおりである。
・ハミルトン閉路判定問題
・彩色判定問題
・ナップザック問題
・最小被覆判定問題
・巡回セールスマン判定問題
ナップザック問題、巡回セールスマン問題等は、暗号に利用されているので、論理式の充足可能性問題は、暗号にも登場することになる。
【０００４】
（２）和積形論理式の充足可能性問題とは
和積形論理式の充足可能性問題について説明する。変数ｘｉは真か偽のいずれかをとる。真を１、偽を０で表わす。変数の否定ｘｉ′（′は否定を表すものとする）は変数ｘｉの値が０の時１となり、１の時０となる。（真の時に１、偽の時に−１というのも可能であり、その他の数値化の方法もあるが、これらは、容易に相互に変換可能であるので、その差は本質的ではない。）
【０００５】
変数ｘｉおよびその否定ｘｉ′をリテラルと呼ぶ。リテラルｌｊ（ｊ＝０，…，ｍ）の論理和ｌ０∨ｌ１∨，…，∨ｌｍを節という。論理和により、節はリテラルが１つでも１である場合には１となり、そうでない場合は０となる。
【０００６】
和積形論理式とは、節をＣｋ（ｋ＝０，…，ｎ）とすると、節の論理積である。すなわち、Ｃ０∧Ｃ１∧，…，∧Ｃｎである。論理積により、論理式はすべての節が１であるときに１となり、それ以外の時は０となる。
【０００７】
充足可能性問題は、与えられ和積形論理式を１とする変数への０か１かの割り当てが存在するかどうかを調べる問題であり、和積形論理式を１とする変数への割り当てを充足解と呼ぶ。充足解が存在する時は充足可能であり、充足解が存在しないときは、充足不能である。
【０００８】
例えば、変数が（ｘ，ｙ，ｚ，ｗ）で、節がＣ１＝ｘ∨ｙ∨ｚ，Ｃ２＝ｘ∨ｙ’∨ｚ，Ｃ３＝ｘ’∨ｗ′の場合、変数への１か０の割り当てが、（ｘ，ｙ，ｚ，ｗ）＝（１，１，１，０）の時に３個の節がすべて１になるため、和積形論理式Ｃ１∧Ｃ２∧Ｃ３は、充足可能であり、（１，１，１、０）が充足解の１つとなる。
【０００９】
また、たとえば、変数が（ｘ，ｙ，ｚ）で、節がＣ１＝ｘ∨ｙ∨ｚ，Ｃ２＝ｘ∨ｙ’∨ｚ，Ｃ３＝ｘ’∨ｚ′、Ｃ４＝ｙ’の場合、和積形論理式Ｃ１∧Ｃ２∧Ｃ３∧Ｃ４は、変数への１か０の割り当てをどのようにしても、１にならないため、この和積形論理式は充足不能である。
【００１０】
（３）和積形論理式の充足可能性判定問題の特徴
和積形論理式の充足可能性判定問題では、変数への０か１の割り当ての数は、変数の組み合わせの数であり、それは、変数の数をｎとすると、２ｎとなり、変数の数の増加とともに指数関数的に増大して行く。いわゆる組み合わせ的爆発の問題である。したがって、変数の割り当てすべてを調べて、和積形論理式が充足可能か充足不能かを判定するのは、変数の数が大きいときには、非常に時間がかかる方法であり、場合によっては、現実的な時間では処理が終わらないということもありえる。そこで、これまで、解の探索を工夫する等の手法が提案されてきた。しかしながら、計算量が変数の数の指数オーダーのままである。
【００１１】
これらの問題点を解決するために、下記の特許文献に示すような従来技術も提案されているが、これらの従来技術に比較してもより高速に解を得ることのできる充足可能性判定問題の処理装置や方法出現が望まれていた。
【００１２】
【特許文献１】
特開平９−２９３０８７号公報
【特許文献２】
特開平７−２４４６５４号公報
【特許文献３】
特開平１１−１８４８４０号公報
【特許文献４】
特開平１０−９１６１２号公報
【００１３】
【発明が解決しようとする課題】
上述したように、従来、和積形論理式の変数への０か１の割り当てを計算機を用いて行う方法では時間がかかりすぎる。
【００１４】
本発明は、このような状況を考慮してなされたものであって、その目的とするところは、和積形論理式の充足可能性判定問題を非常に高速（変数の数の多項式オーダー）に解析できる和積形論理式の充足可能性判定方法および装置を提供することにある。
【００１５】
【課題を解決するための手段】
和積形論理式の充足可能性判定問題が組み合わせ的爆発を起こすことの根本的原因は、変数が０と１いう離散的な値しか取らないことにある。そこで、請求項１の発明は、各変数の値を０か１から［０，１］の区間に拡張し、各節を、線形不等式に対応させることによって、和積形論理式に対応する凸多面体を作り、一つの図形を処理するという基本的方法を採用することで、組合わせ的爆発を根源的に回避することを特徴とし、変数を０と１から［０，１］に拡張することによって発生した充足可能性判定には関係のない領域を凸多面体から切除することにより、凸多面体を小さくすることで和積形論理式の充足不能性を判定することを特徴とする。
【００１６】
請求項２の発明は、請求項１の発明を実現する方法に関するものであり、凸多面体の領域の中での充足可能性判定には関係のない領域を同定する際に、凸多面体上での線形式もしくは非線形式の最小値（もしくは最大値）を計算し、その値の数的性質（たとえば、整数でない、偶数でない）もしくはその最小値（もしくは最大値）を用いて計算された値に基づいて、凸多面体の中の充足可能性とは関係のない領域を同定することを特徴とする。
【００１７】
請求項３の発明は、請求項２の発明を具体的に実現する方法に関するものであり、凸多面体の領域の中で充足可能性判定には関係のない領域を切除する際に、ある線形式の凸多面体上での最小値（もしくは最大値）が非整数である場合にはその非整数にもとづいて求めた値を最小値とした線形不等式を追加することで、凸多面体を切除し、小さくすることを特徴とする。
【００１８】
請求項４の発明は、請求項２およびに請求項３をより具体的に実現する方法に関するものであり、凸多面体の領域の中で充足可能性判定には関係のない領域を切除する線形不等式の最小値を、和積形論理式における変数が０か１のいずれかであるという性質に基づいて、非整数を切り上げた整数にすることで、凸多面体を効率的に切除し、小さくすることを特徴とする。
【００１９】
請求項５の発明は、請求項２、請求項３または請求項４の発明中で用いるところの凸多面体の領域の中での最小値を計算する線形式にかかわる発明で、その線形式を２リテラルの節に対応する線形式（２リテラル線形式）を用いることで計算量を減少させることを特徴とする。
【００２０】
請求項６の発明は、充足不能を判定する際にかかわるものであって、領域を空にするまで計算せず、ある変数の最小値が０を超えていてかつその変数の最大値が１未満であることで、計算量を減ずることを特徴とする。
【００２１】
請求項７の発明は、和積形論理式が充足可能な場合で、請求項１乃至請求項６のいずれか一つに記載の発明を繰り返し用いることで、その充足解を求めることを特徴とする。
【００２２】
請求項８の発明は、前記請求項１の発明を装置の観点から把握したものであって、入力された和積形論理式を充足する変数の割り当てが存在するか否かを判する和積形論理式の充足可能性判定装置において、入力された論理式を、その変数の範囲を０〜１の区間に拡張し、和積形論理式の各節に対応する複数の線形不等式に変換する不等式変換部と，前記不等式変換部によって得られた複数の線形不等式によって形成される凸多面体上における最小値若しくは最大値を計算する最小（大）値計算部と、前記計算された最小値若しくは最大値に基づいて追加できる線形不等式の有無を判定する不等式追加判定部と、追加すべき線形不等式が存在しないと判断した場合に最小値が０を超えかつ最大値が１未満の変数の有無を検索する変数検索部と、追加すべき線形不等式が存在すると判断した場合に、前記最大値または最小値の値に基づいて新たな線形不等式を作成し、前記最小値計算部に出力する不等式追加部と、前記変数検索部において最小値が０を超えかつ最大値が１未満の変数がある場合には充足不能と判定し、最小値が０を超えないかまたは最大値が１未満でない変数がある場合には充足可能と判定する充足可能性判定部と、を備えていることを特徴とする。
【００２３】
請求項９の発明は、前記請求項８の発明において、前記充足可能性判定部において充足可能と判定した場合に、充足可能とされた充足解の範囲を出力する充足解出力部と、この充足解出力部において具体的な一つの充足解が発見されない場合に、和積形論理式０か１を代入して新しい和積形論理式を計算し、この新しい和積形論理式を前記線形不等式変換部に出力する和積形論理式計算部を備えていることを特徴とする。
【００２４】
請求項１０の発明は、前記請求項８の発明において、前記充足可能性判定部において充足可能と判定した場合に、充足可能とされた充足解の範囲を出力する充足解出力部と、この充足解出力部において具体的な一つの充足解が発見されない場合に、線形不等式に０か１を代入して新しい線形不等式を計算し、この新しい線形不等式を前記最小（大）値計算部に出力する線形不等式計算部を備えていることを特徴とする。
【００２５】
請求項１１の発明は、請求項８、請求項９または請求項１０に記載の発明において、前記充足可能性変換部が、前記最小（大）値計算部において、凸多面体を構成する線形不等式の領域が空の場合に充足不能と判定することを特徴とする。
【００２６】
請求項１２の発明は、請求項８、請求項９、請求項１０または請求項１１に記載の発明において、前記不等式追加部が、前記最小（大）値計算部によって得られた最小値あるいは最大値が非整数である場合に、その非整数を切り上げ若しくは切り下げて得られた整数を最小値あるいは最大値とする線形不等式を作成することを特徴とする。
【００２７】
請求項１３の発明は、請求項８、請求項９、請求項１０、請求項１１または請求項１２に記載の発明において、前記線形不等式が、２リテラル線形不等式であることを特徴とする。
【００２８】
請求項１４の発明は、請求項８、請求項９、請求項１０、請求項１１、請求項１２または請求項１３に記載の発明において、前記最小（大）値計算部の出力側に、凸多面体が空かどうか調べるための凸多面体存在判定部が接続され、この凸多面体存在判定部は、凸多面体が空の場合には、その旨を前記充足可能性判定部に出力し、前記充足可能性判定部が和積形論理式が充足不能であると判定するものであることを特徴とする。
【００２９】
【発明の実施の形態】
以下、本発明の実施の形態について、図面を参照して具体的に説明する。
【００３０】
（１）実施の形態の構成
本発明の論理式充足可能性判定方法を実現する装置は、一例として、図６の機能ブロック図に示すような構成を有している。すなわち、本装置は、判定対象となる和積形論理式を入力するキーボード、通信装置、外部記憶装置などの入力装置１と、判定結果を出力するディスプレイ、プリンタ、外部記憶装置通信装置などの出力装置２を備えたコンピュータ３上で実行されるプログラムによって、以下述べる各部位を機能させることにより実現される。
【００３１】
本装置は、前記入力装置１から入力された論理式を、その変数の範囲を０〜１の区間に拡張し、和積形論理式の各節に対応する複数の線形不等式に変換する不等式変換部１０を備えている。この不等式変換部１０は、本実施の形態では、入力された論理式を２リテラル線形式に変換するものである。
【００３２】
前記不等式変換部１０の出力側には、不等式変換部１０によって得られた複数の線形不等式によって形成される凸多面体上における最小値若しくは最大値を計算する最小（大）値計算部１１とを備えている。なお、この最小（大）値計算部１１は、最小値若しくは最大値のいずれか一方を計算するものであって、どちらを計算するかは、本発明の方法を実行する際のアルゴリズムにより予め決定されている。
【００３３】
前記最小（大）値計算部１１の出力側には、凸多面体が空かどうか調べるための凸多面体存在判定部１８が接続されている。この凸多面体存在判定部１８は、凸多面体が空の場合には、その旨を充足可能性判定部１５に出力し、この充足可能性判定部１５が和積形論理式が充足不能であると判定し、その判定結果を出力装置２に出力するものである。
【００３４】
前記凸多面体存在判定部１８は、凸多面体が空でないと判定した場合に、前記最小（大）値計算部１１によって計算された最小値若しくは最大値に基づいて追加できる線形不等式の有無を判定する不等式追加判定部１２に接続されている。この不等式追加判定部１２は、線形式の凸多面体上での最小値もしくは最大値が非整数である場合にはその非整数を用いて計算した値で線形不等式の追加の是非を決定するものである。
【００３５】
前記不等式追加判定部１２の出力側は、追加すべき線形不等式が存在しないと判断した場合に最小値が０を超えかつ最大値が１未満の変数の有無を検索する変数検索部１３と、追加すべき線形不等式が存在すると判断した場合に、前記最大値または最小値の値に基づいて新たな線形不等式を作成し、前記最小値計算部１１に出力する不等式追加部１４とに接続されている。
【００３６】
前記変数検索部１３は、前記変数検索部１３において、最小値が０を超えかつ最大値が１未満の変数がある場合には充足不能と判定し、最小値が０を超えないかまたは最大値が１未満でない変数がある場合には充足可能と判定する充足可能性判定部１５に接続されている。この充足可能性判定部１５は、その判定結果を前記コンピュータ３の出力装置２に出力するものである。
【００３７】
前記充足可能性判定部１５には、充足可能性判定部１５が充足可能と判定した場合に、充足可能とされた充足解の範囲を出力する充足解出力部１６と、この充足解が発見されなかった場合に、和積形論理式に０か１を代入して新しい和積形論理式を計算し、この新しい和積形論理式を前記線形不等式変換部に出力する和積形論理式計算部１７が接続されている。前記充足解出力部１６は、その判定結果及び得られた充足解を前記コンピュータ３の出力装置２に出力するものである。
【００３８】
（２）実施の形態の作用
前記のような構成を有する本発明の装置の基本的な作用を、図１のフローチャートに従って、以下に説明する。なお、図中Ｓは、ステップを示す。
【００３９】
まず、入力装置１より充足可能性の判定対象となる和積形論理式をコンピュータ３に入力する（ステップ１）。入力された和積形論理式は、不等式変換部１０において２リテラル線形式に変換される。すなわち、ステップ１で入力された和積形論理式の各節に対応する線形不等式の集合Ｃを、ステップ２で作る。たとえば、その節が、ｘ∨ｙ∨ｚならば、ｘ＋ｙ＋ｚ＞１である。ｘ∨ｙ’∨ｚならば、ｘ＋（１−ｙ）＋ｚ＞１である。
【００４０】
線形不等式および線形式では、ｘの否定は、１−ｘとして表現される。ｘ，ｙ，ｚの各変数の定義域は、［０，１］なので、１＞ｘ＞０，１＞ｙ＞０，１＞ｚ＞０の線形不等式を追加して凸多面体を作る。線形不等式の集合は、この例では、以下のようになる。
【００４１】
｛ｘ＋ｙ＋ｚ＞１，ｘ＋（１−ｙ）＋ｚ＞１，１＞ｘ＞０，１＞ｙ＞０，１＞ｚ＞０｝
【００４２】
前記のようにして不等式変換部１０によって２リテラル線形式に変換された後は、最小（大）値計算部１１において、変換されたすべての２リテラル線形式についてその最小値を計算する（ステップ３）。
【００４３】
その具体的な手法は、図３に示す通りである。まず、ステップ２１で線形不等式を入力する。そしてステップ２２で、全ての２リテラル線形式を生成する。変数がｘ，ｙ，ｚの場合には、２リテラル以下の節とそれに対応する２リテラル線形式は、以下のとおりである。
【００４４】
（ｘ’はｘの否定）
ｘ∨ｙ      ｘ＋ｙ
ｘ∨ｙ’    ｘ＋１−ｙ
ｘ’∨ｙ    １−ｘ＋ｙ
ｘ’∨ｙ’  １−ｘ＋１−ｙ
ｘ∨ｚ      ｘ＋ｚ
ｘ∨ｚ’    ｘ＋１−ｚ
ｘ’∨ｚ    １−ｘ＋ｚ
ｘ’∨ｚ’  １−ｘ＋１−ｚ
ｘ∨ｗ      ｘ＋ｗ
ｘ∨ｗ’    ｘ＋１−ｗ
ｘ’∨ｗ    １−ｘ＋ｗ
ｘ’∨ｗ’  １−ｘ＋１−ｗ
ｘ∨ｗ      ｙ＋ｚ
ｙ∨ｚ’    ｙ＋１−ｚ
ｙ’∨ｚ    １−ｙ＋ｚ
ｙ’∨ｚ’  １−ｙ＋１−ｚ
ｙ∨ｗ      ｙ＋ｗ
ｙ∨ｗ’    ｙ＋１−ｗ
ｙ’∨ｗ    １−ｙ＋ｗ
ｙ’∨ｗ’  １−ｙ＋１−ｗ
ｚ∨ｗ      ｚ＋ｗ
ｚ∨ｗ’    ｚ＋１−ｗ
ｚ’∨ｗ    １−ｚ＋ｗ
ｚ’∨ｗ’  １−ｚ＋１−ｗ
【００４５】
以降では、簡単のため、２リテラル線形式の「２リテラル」を省略する。ステップ２３で、線形式の凸多面体上での最小値の計算を線形計画法を用いて、行う。線形計画法は、シンプレックス法（単体法）でも、内点法でも、楕円体法等、どのようなものでもよい。ステップ２４で、計算された最小値を出力する。
【００４６】
次に、前記凸多面体存在判定部１８において、凸多面体が空かどうか調べる（ステップ４）。空とは、線形不等式の共通領域がなく、凸多面体を作れないことである。たとえば、ｘ＞０．８，０．４＞ｘという二つの線形不等式の共通領域は存在しないので、凸多面体は形成されず、空になる。空であれば、その時点で、充足不能であることがわかるので、充足不能と判定してその結果を出力装置２に出力して、プログラムを終了する。なお、空であるかどうかは、線形計画法が判定する。
【００４７】
そうでない場合は、ステップ５に行く。ステップ５では、不等式追加判定部１２により、線形式の最小値が非整数のものはないかを調べる。もし非整数のものが無ければ、すなわち、すべての線形式の最小値が整数であれば、ステップ７に行く。
【００４８】
ステップ７では、変数検索部１３において、各変数の最小値と最大値を調べて、もし、ある一つの変数の最大値が１未満で最小値が０を超えている（たとえば、０．５＞ｘ＞０．５）ならば、充足可能性判定部１５により充足不能と判定して、その結果を出力装置２に終了する。そうでなければ、充足可能性判定部１５により充足可能と判定して、各変数の最大値と最小値を出力装置２に出力して終了する。
【００４９】
前記不等式追加判定部１２は、ステップ５で、線形式の最小値が非整数のものがあれば、この最小値にもとづいて不等式追加部１４により新たな線形不等式を作成し、これを再び最小（大）値計算部１１に出力する（ステップ６）。このステップ６の詳細は、図４に示す通りである。ステップ３１で線形不等式の集合を入力する。ステップ３２で２リテラル線形式の最小値を入力する。そして、ステップ３３で、その最小値が整数かどうかを判定する。整数であれば、ステップ３２に戻る。
【００５０】
整数でなければ、ステップ３４に行き、その非整数を切り上げた整数を最小値に持つ線形不等式を作り、凸多面体を作っている線形不等式の集合に加える。そして、ステップ３５で、線形不等式の集合を出力する。
【００５１】
｛ｘ＋ｙ＋ｚ＞１，ｘ＋１−ｙ＋ｚ＞１，１＞ｘ＞０，１＞ｙ＞０，１＞ｚ＞０｝
【００５２】
たとえば、上記の線形不等式が作る凸多面体では、ｘ＋ｚの最小値は０．５になる。０．５は非整数なので、０．５を切り上げて、整数１を得る。この整数１を最小値とする線形不等式ｘ＋ｚ＞１を凸多面体を作る線形不等式の集合に加える。線形不等式の集合は以下のようになる。新しい線形不等式が加わった分だけ、線形不等式が作る凸多面体は小さくなる。
【００５３】
｛ｘ＋ｚ＞１，ｘ＋ｙ＋ｚ＞１，ｘ＋１−ｙ＋ｚ＞１，１＞ｘ＞０，１＞ｙ＞０，１＞ｚ＞０｝
【００５４】
他に、最小値が非整数であるような線形式があれば、同様にして、その非整数を切り上げた整数にして、線形不等式を作り、上記の線形不等式の集合に加える。この辺の概念図を図５に示す。このように、非整数の最小値を切り上げた整数を最小値とする不等式をなぜ作れるかというと、それは、もともとの和積形論理式での変数の取りうる値が０か１だからである。充足可能な場合には、充足解が存在し、変数の値が０と１だから、その和は整数になる。たとえば、ｘ＋ｚの凸多面体上での最小値が０．５、すなわちｘ＋ｚ＞０．５でも、ｘ＋ｚは０，１、２のいずれかなので、ｘ＋ｚ＞０．５はｘ＋ｚ＞１に変更しても、充足可能性には影響を与えない。
【００５５】
上記では、ステップ５で、最小値が非整数である線形式があるかないかを調べ、ステップ６で、その非整数を切り上げた整数を最小値にもつ線形不等式を作ったが、これは、たとえば、次のように変形できる。このように、似たような手法はいくつか考えられる。
【００５６】
（１）  ステップ５で、最小値の２乗が非整数である線形式があるかないかを調べ、ステップ６で、その最小値を切り上げた整数より少し小さい値（非整数）を最小値にもつ線形不等式を作る。
（２）  ステップ５で最小値を２のｎ乗倍した値が２のｎ乗未満で０を超えていれば、ステップ６で、その最小値を切り上げた整数を最小値に持つ線形不等式を作る。
（３）  最小値が非整数である線形式があるかないかを調べ、ステップ６で、その非整数を切り上げた整数を最小値にもつ２次不等式を作る。
【００５７】
不等式追加部１４によるステップ６の処理後は、最小（大）値計算部１１によるステップ３に行き、再び、全２リテラル線形式の最小値を線形計画法（たとえば内点法）を用いて計算する。線形式の中には、線形不等式に現れるものがあり、その場合、線形式の最小値は、簡単な計算から１となることがわかる。たとえば、上記で、追加になったｘ＋ｚ＞１であるが、ｘ＋ｚの最小値が１になる。したがって、最小値の計算は、線形不等式の集合中に存在しない最小値が０の２リテラル線形式のみに対して行う。図３のステップ２３を参照。
【００５８】
ステップ３処理後は、ステップ４以降の処理を行う。後は、この繰り返しである。この繰り返しのループから脱するのは、領域が空か、追加すべき線形式が残っていないか、のいずれかである。
【００５９】
領域が空で、充足不能と判定して、繰り返しのループから脱するのはよいが、追加すべき（２リテラル）線形式がないという条件で、繰り返しのループから脱してよいかは、自明ではない。しかしながら、充足不能である場合には、追加すべき２リテラル線形式がないときは、凸多面体が空でなければ、どれか一つの変数の最小値が０を超えてかつ最大値が１未満であることが示せる。証明は、以下のとおりである。
【００６０】
どれか一つの変数の最小値が０を超え最大値が１未満になるということは、その変数の値が以下のようになるということである。
［ａ，ｂ］（０＜ａ，ｂ＜１）
【００６１】
したがって、「どれか一つの変数の最小値が０を超え最大値が１未満になる。」を否定すると「すべての変数で、その最小値が０を超えないかまたは最大値が１未満にならない。」となり、これは、各変数の値が以下のいずれかになることを意味する。
［０，１］［０，ａ］，［ｂ，１］（０＜ａ，ｂ＜１）
【００６２】
（Ａ）［０，ａ］の場合
ｘ１が
０＜ｘ１＜ａ
としよう。したがって、
ｘ１＝０
となるような点が凸多面体に存在する。その点は
（０，ｘ２，ｘ３，．．．，ｘｎ）
と記されるが、
ｘ２，ｘ３，．．．，ｘｎ
が、すべて０か１になることはない。たとえば、
（０，１，０，．．．，１）
のようになることはない。
【００６３】
なぜならば、この点は、充足可能な点であり、充足不能の仮定に反する。したがって、
ｘ２，ｘ３，．．．，ｘｎ
が、すべて０か１になることはないので、
ｘ２，ｘ３，．．．，ｘｎ
の中のどれか一つの変数の最小値は０を超え、最大値は１未満になる。すなわち、ある変数ｘｉ（２＜ｉ＜ｎ）は、
０＜ｘｉ＜１
である。
【００６４】
別の表現では
ｐ＜ｘｉ＜ｑ（０＜ｐ，ｑ＜１）
である。したがって、ｘ１が０になる点は
（０，１，０，．．，ｘｉ．，１）（ｐ＜ｘｉ＜ｑ（０＜ｐ＜ｑ＜１））のように表現される。
【００６５】
ここで、
ｘ１＋ｘｉ
の最小値を考える。
ｘ１とｘｉが同時に０になることはないので、
０＜ｘ１＋ｘｉ
であり、最小値は０以上になる。
【００６６】
また、
ｘ１＋ｘｉ
の最小値が１ということもありえない．なぜなら、
ｘ１＋ｘｉ
は
０＋ｐ＝ｐ
という値をとるからである。
【００６７】
したがって、
ｘ１＋ｘｉ＞ｃ（０＜ｃ＜１）
となる。このｃは整数ではない。
【００６８】
なお、必ずしも、ｃ＝ｐではない。それは、
ｘｉ＝０の時に、
ｄ＜ｘ１（０＜ｄ＜１）
となり、
ｃ＝ｍｉｎ（ｐ，ｄ）
になるからである。
【００６９】
（Ｂ）［０，１］の場合
つぎに、ｘ１が
０＜ｘ１＜１
としよう。このときも、
０＜ｘ１＜ａ
の場合と全く同じ議論が成立し、
ｘ１＋ｘｉ
の最小値は非整数になる。
【００７０】
（Ｃ）［ａ，１］の場合
次に、
ａ＜ｘ１＜１の場合を考えよう。
この場合には、ｘ１＝１となるような点が凸多面体にあると仮定し、（Ａ）で考えた
ｘ１＋ｘｉ
のかわりに
（１−ｘ１）＋ｘｉ
の最小値を考えれば（Ａ）と同様の議論で、
（１−ｘ１）＋ｘｉ＞ａ’（０＜ａ’＜１）
が言え、
（１−ｘ１）＋ｘｉ
の最小値は非整数になる。
【００７１】
以上のように、３個のどの場合でも、最小値が非整数になる２リテラル線形式が存在する。最小値が整数の２リテラル線形式しか、残っていないので、このような非整数を最小値とする２リテラル線形式が存在するのは矛盾である。この矛盾は、「ある変数の最小値が０を超え最大値が１未満である」の否定を仮定したことに起因する。したがって、「ある変数の最小値が０を超え最大値が１未満である。」ということになる。これで、「充足不能である場合には、上記の凸多面体切除アルゴリズムの終了後、凸多面体が空でなければ、どれか一つの変数の最小値が０を超えてかつ最大値が１未満である。」が、証明されたことになる。
【００７２】
また、ステップ６の線形不等式の追加は、充足可能性に影響を与えないので、充足可能な場合には、「ある変数の最小値が０を超え最大値が１未満である。」ということはない。
【００７３】
ステップ３で、２リテラル線形式のみの最小値を計算する理由は、上記のとおりである。しかしながら、１リテラル線形式、３リテラル線形式等の線形式も用いることも考えられる。
【００７４】
１リテラル線形式の場合、たとえば、ｘの最小値がａ（０＜ａ＜１）ならば、すなわち
ａ＜ｘ
ならば、ｘは、もとの和積論理式では０か１なので、
１＜ｘとなる。
この場合には、ステップ３一回あたりの計算量は増えるが、繰り返しの回数が少なくてすむ可能性がある。
【００７５】
ステップ３ではリテラル線形式で最小値を計算したが、線形式の最大値を計算することも可能である。最大値を計算することは、最小値を計算することと同じである。たとえば、上記の説明ではｘと１−ｘの最小値を計算したが、これは、１−ｘとｘの最大値を計算していることである。また、リテラル線形式ではなく、別の線形式、もしくは非線形式での評価も可能である。
【００７６】
ところで、充足不能の場合には、凸多面体切除アルゴリズムの停止後、線形不等式が作る凸多面体は空になる。証明は以下のとおりである。
【００７７】
充足不能の場合には、２リテラル線形式による凸多面体切除アルゴリズムの停止後、不等式の領域が空でなければ、どれか一つの変数は、最小値が０を超え最大値が１未満になる。その変数をｘとして、その最小値をａその最大値をｂとすれば、
ａ＜ｘ，ｘ＜ｂ（０＜ａ，ｂ＜１）
となる。
【００７８】
ａ＜ｘ
は、ｘは、もとの和積形論理式では０か１なので、
１＜ｘ
と変更できる。
ｘ＜ｂ
は、ｘは、もとの和積形論理式では０か１なので、
ｘ＜０
と変更できる。
【００７９】
二つの変更した不等式
１＜ｘ
ｘ＜０
を凸多面体に追加すれば、凸多面体は、空になる。これで、「充足不能の場合には、凸多面体切除アルゴリズムの停止後、線形不等式が作る凸多面体は空になる。」が証明されたことになる。
【００８０】
したがって、「ある変数の最小値が０を超え最大値が１未満である」ということで、充足不能の判定をせずに、「領域が空になる」で、充足不能の判定もできるが、計算量的には、空で判定する方が、空を導く処理分だけ多いので、「ある変数の最小値が０を超え最大値が１未満である」ということで、充足不能の判定をする方が効率的である。
【００８１】
本発明の計算量であるが、２リテラル線形式の数は、Ｏ（ｎ２）である。従って，本アルゴリズムのステップ３の処理を一回行う時の、最小値を求める計算の回数は、Ｏ（ｎ２）で抑えられる。また、ステップ３の繰り返しの数は、最悪でＯ（ｎ２）で抑えられる。したがって、ステップ３で行う最小値を求める計算の回数はＯ（ｎ４）で抑えられる。
【００８２】
ステップ３の最小値を求める計算は線形計画法で実施されるが、その線形計画法には内点法等の多項式時間アルゴリズムが存在するので、本発明の計算量は多項式時間になる。
【００８３】
ところで、論理式充足可能性判定問題に関する従来手法は以下のとおりである。
・離散的（定性的）な手法：探索、導出法、項書き換え、ＢＤＤ（二分決定グラフ）等
・連続的（定量的）な手法：整数計画法、線形計画法、非線形計画法、ニューラルネットワーク、Ｆｏｕｒｉｅｒ−Ｍｏｔｚｋｉｎの消去法等
【００８４】
さらに、これらを組み合わせた手法、並列化した手法とさまざまな手法が提案されている。本発明を、上記の従来手法の一つもしくは複数と、組み合わせることで、さらに高速化できる。ここでは、その一例として、本発明と導出法との組み合わせについて以下に簡単に述べる。
【００８５】
導出法は、二つの節から一つの節を生成する推論手法である。例えば、
ｘ∨ｙ∨ｚ，ｘ∨ｙ’∨ｚからｘ∨ｚ
を導出する。
この例のｙ（ｙ’）のように、各節に肯定と否定が入っている変数は消去することができる。これを線形不等式で表現すると、
ｘ＋ｙ＋ｚ＞１，ｘ＋（１−ｙ）＋ｚ＞１からｘ＋ｚ＞１
を導出する、と表現される。（線形不等式の場合も、導出と呼ぶ。）
【００８６】
本発明の手法で記述すると、以下のようになる。
ｘ＋ｙ＋ｚ＞１，ｘ＋（１−ｙ）＋ｚ＞１の制約下でｘ＋ｚの最小値を計算すると、０．５となる。０．５は非整数なので、これを切り上げて１とした線形不等式ｘ＋ｚ＞１を得る。この線形不等式は、導出法で得られた線形不等式と同じである。
【００８７】
この例のように、本発明における線形計画法によって計算された最小値を基にして得られた線形不等式は、導出によっても得られることがある。一回の導出の方が一回の線形計画法より、計算量は少ない。したがって、導出で得られる線形不等式は、線形計画法で最小値の計算をしなくてよく、その分だけ、本発明の計算量を減らすことができる。したがって、本発明を導出法と組み合わせることで、線形計画法の回数を減らすことが可能になり、高速化が可能になる。
【００８８】
また、導出では、２リテラル線形不等式以外の線形不等式が得られるが、この線形不等式を制約として追加することで、多面体をより小さくできるので、その分だけ早く多面体を空にできる。
【００８９】
組み合わせの方法にはいくつかの方法が考えられる。たとえば、以下の組み合わせ方法が考えられる。
（１）  論理式の節（に対応する線形不等式）に対して導出を或る回数行い、導出された線形不等式を制約に追加する。その導出された線形不等式中の２リテラル線形不等式の線形式を最小値計算の対象からはずす。
（２）  ある２リテラル線形式ｆの最小値を計算し、非整数であれば、ｆ＞１という線形不等式を制約に追加する。そうでなければ、次の２リテラル線形式の最小値を計算する。
（３）  追加された２リテラル線形不等式とすでに制約になっている線形不等式から導出される線形不等式を制約に追加する。
（４）  （２）  と（３）  を繰り返す。
ただし、上記の処理で、制約に追加する線形不等式は、線形不等式が作る多面体を真に小さくするような線形不等式だけとする。
【００９０】
ところで、上記の組み合わせでは、２リテラル線形式の最小値のみを計算しているが、最小値計算の対象を１リテラル線形式、３リテラル線形式等に拡張するような組み合わせも考えられる。また、上記の組み合わせでは、導出と最小値計算を切り替えながら行っているが、並列に、導出と最小値計算を行い、適当にお互いの情報を交換しながら進行するという組み合わせも考えられる。
【００９１】
本発明と他の手法との組み合わせ方法であるが、上述した方法と類似の方法の場合もあるし、類似していない方法の場合もある。本発明と他の手法との組み合わせにより、計算量を減らせるが、その要点は、上記からわかるように、以下のとおりである。
（１）  他の手法で得られた線形不等式を制約に追加することで、多面体をなるべく早く小さくする。
（２）  最小値計算を行う線形式の数をなるべく少なくする。
【００９２】
また、上述したように、並列化によって、高速化が可能である。さらに、計算量の減少の方法としては、なるべく早く多面体を空にするために、最小値の計算を行う線形式の順序をあらかじめ決めておくのではなく、或る段階でどの線形式の最小値を計算すればよいかを他の手法等を用いて動的に決定してゆくという方法も考えられる。
【００９３】
なお、途中で、なんらかの方法で或る変数の値が０か１かわかった場合には、その変数に０か１の値を代入して、論理式を簡略化して、それ以降の処理を行うことで、計算量を減少できる。
【００９４】
本発明の第２の実施形態を図２に示す。図２のステップ１０は、図１のステップ１からステップ７の処理を意味する。
【００９５】
充足可能な場合、一般的には、図２のステップ１０（図１のステップ７）の出力は、各変数の取りうる範囲なので、解を出力するわけではない。
【００９６】
たとえば、
（ｘ∨ｙ）（ｘ’∨ｙ’）
を図２のステップ１０（図１のステップ１）に入力すると、図２のステップ１０（図１のステップ７）の出力は、
ｘ＝０，１
ｙ＝０，１
となる。
【００９７】
しかしながら、充足解は、
（ｘ，ｙ）＝（１，０），（０，１）
であり、
（ｘ，ｙ）＝（０，０），（１，１）
は充足解にはならない。
【００９８】
このような状況は、図２のステップ１０（図１のステップ７）の出力からはわからない。しかしながら、充足解の範囲はわかる。ｘ＝０，１、ｙ＝０，１という出力は、ｘ＝０という充足解が存在するということを示している。そこで、本実施の形態においては、和積論理式計算部１７において、元の和積形論理式にｘ＝０を代入することで得られる和積形論理式を再び、図２のステップ１０（図１のステップ１）に入力することで、図２のステップ１０（図１のステップ７）よりｙ＝１の充足解を得る事ができる。
【００９９】
このようにして一つの充足解
（ｘ，ｙ）＝（０，１）
を得ることができる。
【０１００】
一般的に言えば、充足可能な場合には、図２のステップ１０の一つでも充足解が求まっているかどうかの判定を、充足解出力部１６において行う（ステップ１１）。充足可能解が一つでも求まっていれば、充足解出力部１６はこれを出力装置２に出力してプログラムを終了する。
【０１０１】
充足解出力部１６において、充足可能解が求まっていないことが判明した場合は、ステップ１２に行き、和積論理式計算部１７により、０か１かが決まっている変数は、その値を元の和積形論理式に代入し、０か１か決まっていないものは、一つの変数を選び、０か１かのいずれかを元の和積形論理式に代入する。このようにして得られた新しい和積形論理式を、ステップ１０に入力し、再び、ステップ１０の出力を得る。これを繰り返して、最終的に充足可能解を得る。
【０１０２】
この繰り返しの回数であるが、毎回一つずつしか、変数の代入が行えない場合も考えられるので、最悪の場合、繰り返しの数は変数の数ということになる。
【０１０３】
なお、前記の説明は、和積論理式計算部１７から論理式を出力し、これを不等式変換部１０に入力することで、論理式に変数の値を代入して、新しい論理式を計算して、それを、線形不等式に変換したものであるが、必ずしも論理式に変数の値を代入することに限定されるものではなく、線形不等式に変数の値を代入することも可能である。
【０１０４】
図７は、そのような場合の本装置の機能ブロック図であって、図６の和積論理式計算部１７の代わりに、線形不等式計算部１７ａが設けられ、この線形不等式計算部１７ａにおいて線形不等式に変数の値を代入することで新たな線形不等式が作成され、その新たな線形不等式が最小（大）値計算部１１に出力され、図６の実施形態と同様な繰り返しの処理がなされるように構成されている。
【０１０５】
以上述べたように、充足可能解を求めるに当たっては、論理式に変数を代入しても良いし、線形不等式に変数の値を代入しても良いが、線形不等式に変数の値を代入した場合には、論理式を線形不等式に変換する手間が省ける。
【０１０６】
【実施例】
以下に、前記のような本実施の形態に従って充足可能解の有無の判定及び得られた充足可能解を出力する場合の実施例を二つ示す。
（１）実施例１
最初の例は充足不能の例である。変数の数は４で、節の数は９である。
【０１０７】
（ｘ∨ｙ∨ｚ）（ｘ∨ｗ∨ｚ’）（ｘ∨ｙ’∨ｗ）（ｘ∨ｙ’∨ｗ’）（ｘ’∨ｚ∨ｗ）（ｘ’∨ｚ’∨ｗ）（ｙ∨ｚ∨ｗ’）（ｙ∨ｚ’∨ｗ’）（ｘ’∨ｙ’∨ｗ’）
【０１０８】
ステップ１の入力装置で入力された和積形論理式をステップ２で以下の線形不等式に変換する。
【０１０９】
ｘ＋ｙ＋ｚ  ＞１
ｘ＋１−ｚ＋ｗ＞１
ｘ＋１−ｙ＋ｗ＞１
ｘ＋１−ｙ＋１−ｗ＞１
１−ｘ＋ｚ＋ｗ＞１
１−ｘ＋１−ｚ＋ｗ＞１
ｙ＋ｚ＋１−ｗ＞１
ｙ＋１−ｚ＋１−ｗ＞１
１−ｘ＋１−ｙ＋１−ｗ＞１
【０１１０】
ステップ２では、変数の領域を示す以下の不等式も付加される。
０＜ｘ＜１，０＜ｙ＜１，０＜ｚ＜１，０＜ｗ＜１
【０１１１】
ステップ３で、すべての２リテラル式とその最小値を計算する。以下は、その線形式と最小値である。線形式の最小値は線形計画法（内点法等）で行う。
【０１１２】
ｘ＋ｙ          １／３
ｘ＋１−ｙ      １／２
１−ｘ＋ｙ      ０
１−ｘ＋１−ｙ  １／４
ｘ＋ｚ          １／４
ｘ＋１−ｚ      １／３
１−ｘ＋ｚ      １／３
１−ｘ＋１−ｚ  １／３
ｘ＋ｗ          １／３
ｘ＋１−ｗ      １／３
１−ｘ＋ｗ      １／２
１−ｘ＋１−ｗ  １／４
ｙ＋ｚ          １／３
ｙ＋１−ｚ      １／４
１−ｙ＋ｚ      ０
１−ｙ＋１−ｚ  ０
ｙ＋ｗ          ０
ｙ＋１−ｗ      １／２
１−ｙ＋ｗ      １／４
１−ｙ＋１−ｗ  １／２
ｚ＋ｗ          １／２
ｚ＋１−ｗ      １／４
１−ｚ＋ｗ      １／２
１−ｚ＋１−ｗ  １／４
【０１１３】
ステップ４で、上記の領域が空かどうか判定する。この場合、空でないので、ステップ５に進む。
ステップ５では、２リテラル線形式の最小値が非整数のものがあるかどうかを判定する。この場合、最小値が非整数のものがあるので、ステップ６に進む。
ステップ６では、非整数を切り上げた整数を最小値とする線形不等式を作り、線形不等式の集合に追加する。
【０１１４】
ｘ＋ｙ＋ｚ＞１
ｘ＋１−ｚ＋ｗ＞１
ｘ＋１−ｙ＋ｗ＞１
ｘ＋１−ｙ＋１−ｗ＞１
１−ｘ＋ｚ＋ｗ＞１
１−ｘ＋１−ｚ＋ｗ＞１
ｙ＋ｚ＋１−ｗ＞１
ｙ＋１−ｚ＋１−ｗ＞１
１−ｘ＋１−ｙ＋１−ｗ＞１
０＜ｘ＜１
０＜ｙ＜１
０＜ｚ＜１
０＜ｗ＜１
【０１１５】
（ここから下が、ステップ６で追加された線形不等式）
ｘ＋ｙ＞１
ｘ＋１−ｙ＞１
１−ｘ＋１−ｙ＞１
ｘ＋ｚ＞１
ｘ＋１−ｚ＞１
１−ｘ＋ｚ＞１
１−ｘ＋１−ｚ＞１
ｘ＋ｗ＞１
ｘ＋１−ｗ＞１
１−ｘ＋ｗ＞１
１−ｘ＋１−ｗ＞１
ｙ＋ｚ＞１
ｙ＋１−ｚ＞１
ｙ＋１−ｗ＞１
１−ｙ＋ｗ＞１
１−ｙ＋１−ｗ＞１
ｚ＋ｗ＞１
ｚ＋１−ｗ＞１
１−ｚ＋ｗ＞１
１−ｚ＋１−ｗ＞１
【０１１６】
ステップ３にもどり、すべての２リテラル式とその最小値を計算する。ただし、線形不等式中に存在する線形式の最小値は１であるので、それらの計算はしない。したがって、１回目のステップ３の計算で最小値が整数の線形式だけ、最小値の計算を行う。以下は、その線形式と最小値である。線形式の最小値は線形計画法（内点法等）で行う。
【０１１７】
１−ｘ＋ｙ  １
１−ｙ＋ｚ  １
１−ｙ＋１−ｚ  １
ｙ＋ｗ  １
【０１１８】
領域が空でないので、ステップ５に進み、最小値が非整数の式がないので、ステップ７に進む。ステップ７では、各変数の最小値と最大値を計算する。その結果が以下である。
【０１１９】
ｘ＝１／２
ｙ＝１／２
ｚ＝１／２
ｗ＝１／２
【０１２０】
すべての変数の値が１／２であり、「どれか一つの変数の最小値が０を超えてかつ最大値が１未満である。」を満たすので、充足不能を出力して、終了する。
【０１２１】
上記の例からわかるように、ある一つの変数で、その最小値が０を超えてかつ最大値が１未満であるということがわかれば、その時点で、充足不能と判定できるので、以降の計算は行わなくて良い。
【０１２２】
なお、ステップ３の最小値の計算であるが、２変数リテラル式だけではなく、１変数リテラル線形式の最小値の計算も行えば、追加すべき２変数リテラル線形式がなくならなくても、どれか一つの変数の最小値が０を超えてかつ最大値が１未満であるという状況が発生するかもしれない。
【０１２３】
たとえば、２回目のステップ３で、１変数リテラル線形式の最小値の計算からはじめるとする。最初の変数ｘが、最小値が０を超え、最大値が１未満になったとしよう。そうすると、もうそこで、充足不能ということがわかるので、他の１変数リテラル線形式の計算と２変数リテラル線形式の計算は、行う必要がない。
【０１２４】
このような場合には、最小値の計算は、２変数リテラル式だけではなく、１リテラル線形式に対しても行った方が効率的である。しかし、ステップ３一回あたりに最小値計算を行う線形式の数は増える。また、さらに、ステップ３で、最小値が非整数がわかった時点で、その非整数を切り上げた整数を最小とした線形不等式を線形不等式の集合に追加したほうが、効率的である。
【０１２５】
（２）実施例２
２番目の例は充足可能の例であり、充足解はｘ＝１，ｙ＝１，ｚ＝１，ｗ＝０，１である。変数の数は４で、節の数は１０である。
【０１２６】
（ｘ∨ｙ∨ｚ）（ｘ∨ｗ∨ｚ’）（ｘ∨ｙ’∨ｗ）（ｘ∨ｙ’∨ｗ’）（ｘ’∨ｙ∨ｗ）（ｘ’∨ｙ∨ｗ’）（ｘ∨ｚ∨ｗ）
（ｘ∨ｚ∨ｗ’）（ｘ’∨ｚ∨ｗ）（ｘ’∨ｚ∨ｗ’）
【０１２７】
この和積形論理式はｘ＝１，ｙ＝１，ｚ＝１，ｗ＝０，１で充足される。
ステップ１の入力装置で入力された和積形論理式をステップ２で以下の線形不等式に変換する。以下のようになる。
【０１２８】
ｘ＋ｙ＋ｚ＞１
ｘ＋ｙ＋１−ｚ＞１
ｘ＋１−ｙ＋ｗ１＞
ｘ＋１−ｙ＋１−ｗ＞１
１−ｘ＋ｙ＋ｗ＞１
１−ｘ＋ｙ＋１−ｗ＞１
ｘ＋ｚ＋ｗ＞１
ｘ＋ｚ＋１−ｗ＞１
１−ｘ＋ｚ＋ｗ＞１
１−ｘ＋ｚ＋１−ｗ＞１
【０１２９】
ステップ２では、変数の領域を示す以下の不等式も付加される。
０＜ｘ＜１，０＜ｙ＜１，０＜ｚ＜１，０＜ｗ＜１
【０１３０】
ステップ３で、すべての２リテラル式とその最小値を計算する。以下は、その線形式と最小値である。線形式の最小値は線形計画法（内点法等）で行う。
【０１３１】
ｘ＋ｙ          １
ｘ＋１−ｙ      １／２
１−ｘ＋ｙ      １／２
１−ｘ＋１−ｙ  ０
ｘ＋ｚ          １／２
ｘ＋１−ｚ      １／４
１−ｘ＋ｚ      １／２
１−ｘ＋１−ｚ  ０
ｘ＋ｗ          １／３
ｘ＋１−ｗ      １／３
１−ｘ＋ｗ      ０
１−ｘ＋１−ｗ  ０
ｙ＋ｚ          ２／３
ｙ＋１−ｚ      １／４
１−ｙ＋ｚ      １／２
１−ｙ＋１−ｚ  ０
ｙ＋ｗ          １／３
ｙ＋１−ｗ      １／３
１−ｙ＋ｗ      ０
１−ｙ＋１−ｗ  ０
ｚ＋ｗ          １／２
ｚ＋１−ｗ      １／２
１−ｚ＋ｗ      ０
１−ｚ＋１−ｗ  ０
【０１３２】
ステップ４で、上記の領域が空かどうか判定する。この場合、空でないので、ステップ５に進む。
ステップ５では、２リテラル線形式の最小値が非整数のものがあるかどうかを判定する。この場合、最小値が非整数のものがあるので、ステップ６に進む。
ステップ６では、非整数を切り上げた整数を最小値とする線形不等式を作り、線形不等式の集合に追加する。なお、このステップにおいては、最小値が１の線形式ｘ＋ｙもｘ＋ｙ＞１として追加することも可能である。
【０１３３】
ｘ＋ｙ＋ｚ＞１
ｘ＋ｙ＋１−ｚ＞１
ｘ＋１−ｙ＋ｗ１＞
ｘ＋１−ｙ＋１−ｗ＞１
１−ｘ＋ｙ＋ｗ＞１
１−ｘ＋ｙ＋１−ｗ＞１
ｘ＋ｚ＋ｗ＞１
ｘ＋ｚ＋１−ｗ＞１
１−ｘ＋ｚ＋ｗ＞１
１−ｘ＋ｚ＋１−ｗ＞１
０＜ｘ＜１
０＜ｙ＜１
０＜ｚ＜１
０＜ｗ＜１
【０１３４】
（ここから下がステップ６で追加された線形不等式）
ｘ＋１−ｙ＞１
１−ｘ＋ｙ＞１
ｘ＋ｚ＞１
ｘ＋１−ｚ＞１
１−ｘ＋ｚ＞１
ｘ＋ｗ＞１
ｘ＋１−ｗ＞１
ｙ＋ｚ＞１
ｙ＋１−ｚ＞１
１−ｙ＋ｚ＞１
ｙ＋ｗ＞１
ｙ＋１−ｗ＞１
ｚ＋ｗ＞１
ｚ＋１−ｗ＞１
【０１３５】
ステップ３にもどり、すべての２リテラル式とその最小値を計算する。ただし、線形不等式中に存在する線形式の最小値は１であるので、それらの計算はしない。したがって、１回目のステップ３の計算で最小値が０の線形式だけ、最小値の計算を行う。以下は、その線形式と最小値である。線形式の最小値は線形計画法（内点法等）で行う。
【０１３６】
１−ｘ＋１−ｙ  ０
１−ｘ＋１−ｚ  ０
１−ｘ＋ｗ      ０
１−ｘ＋１−ｗ  ０
１−ｙ＋１−ｚ  ０
１−ｙ＋ｗ      ０
１−ｙ＋１−ｗ  ０
１−ｚ＋ｗ      ０
１−ｚ＋１−ｗ  ０
【０１３７】
ステップ４に行く。領域は空ではないので、ステップ５に行く。
ステップ５では、２リテラル線形式の最小値が非整数のものがあるかどうかを判定する。この場合、最小値が非整数のものがないので、ステップ７に進む。
ステップ７では、各変数の最小値と最大値を調べる。
【０１３８】
１／２＜ｘ＜１
１／２＜ｙ＜１
１／２＜ｚ＜１
０＜ｗ＜１
【０１３９】
となり、０，１に限定すれば、
ｘ＝１
ｙ＝１
ｚ＝１
ｗ＝０，１
となり、これを出力して、終了する。
【０１４０】
この場合は、（ｘ，ｙ，ｚ，ｗ）が（１，１，１，０）と（１，１，１，１）の二つが充足解である。
また、この場合には、充足解がわかったので、ステップ１から７を繰り返すという請求項７の発明の処理は不要である。
【０１４１】
【発明の効果】
本発明により、従来の手法と比較すれば、非常に短時間で和積形論理式の充足性を判定できる。さらに、充足可能な場合には、従来の手法に比べれば、非常に短時間で充足解を求めることができる。
【図面の簡単な説明】
【図１】本発明の基本的実施形態の各ステップを説明するフローチャート
【図２】本発明の第２の実施形態の各ステップを説明するフローチャート
【図３】ステップ３の処理において、変換されたすべての２リテラル線形式についてその最小値を計算する手法を示すフローチャート。
【図４】ステップ６の処理において、２リテラル線形式の追加の手法を示すフローチャート。
【図５】ステップ６の処理による、線形不等式と２リテラル線形式の推移の概念図
【図６】本発明の論理式充足可能性判定装置の一実施形態を示す機能ブロック図。
【図７】本発明の論理式充足可能性判定装置の他の実施形態を示す機能ブロック図。
【符号の説明】
１…入力装置
２…出力装置
３…コンピュータ
１０…不等式変換部
１１…最小（大）値計算部
１２…不等式追加判定部
１３…変数検索部
１４…不等式追加部
１５…充足可能性判定部
１６…充足解出力部
１７…和積形論理式計算部
１７ａ…線形不等式計算部
１８…凸多面体存在判定部
【図１】
2004355038.tif 000003
【図２】
2004355038.tif 000004
【図３】
2004355038.tif 000005
【図４】
2004355038.tif 000006
【図５】
2004355038.tif 000007
【図６】
2004355038.tif 000008
【図７】
2004355038.tif 000009