(57)【特許請求の範囲】
【請求項１】
所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定方法にあって、
状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式のすべての節の状態を判定する第１のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、この判定した節の状態においてnot-satisfiedの節が存在するか否かを判定し、not-satisfiedの節が存在する場合には、第６のステップに進む第２のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、第２のステップにおいてnot-satisfiedの節が存在する場合には現在の値の割り当てが解であり、determinedが０の変数の値はdon't careであり、状態判定部の総合判定部からの出力を入力とし、充足出力部より前記解を出力して、第６のステップに進む第３のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、第３のステップにおいて全ての節がsatisfiedでない場合には、unitの節が存在するか否かを判定し、unitの節が存在する場合には、それらの節がinconsistentであるか否かを判定し、inconsistentである場合には、第６のステップに進み、inconsistentでない場合には、コンシステント・ユニット部において前記総合判定部の出力を入力とし、それらの全ての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depthをcurrent_depthに設定し、第１のステップに戻る第４のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、第４のステップにおいてunitの節が存在しない場合にはブランチ部において前記総合判定部の出力を入力としbinaryの節に最も多く含まれる変数を選択し、その変数の値、determined、およびbranchをそれぞれ０、１、１に設定し、depthをcurrent_depth＋１に設定し、current_depthを１増加し、第１のステップに戻る第５のステップと、
バックトラック部において前記総合判定部の出力を入力とし、current_depthが０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対して、depth=current_depth、かつbranch=０の場合にはdeterminedおよびdepthを０に設定し、depth=current_depth、かつbranch=１の場合にはその変数の値を１に設定し、depthをcurrent_depth-1に設定し、かつbranchを０に設定し、更にcurrent_depthを１低減し、第１のステップに戻る第６のステップと、
を有することを特徴とする和積形論理式の充足判定方法。
【請求項２】
所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定方法であって、
状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式のすべての節の状態を判定する第１のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、この判定した節の状態においてnot-satisfied の節が存在するか否かを判定し、not-satisfied の節が存在する場合には、第６のステップに進む第２のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、第２のステップにおいてnot-satisfied の節が存在しない場合には、すべての節がsatisfied であるか否かを判定し、satisfied である場合には、現在の値の割り当てが解であり、determinedが０の変数の値はdon't careであり、状態判定部の総合判定部からの出力を入力とし、充足出力部より前記解を出力して、第６のステップに進む第３のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、第３のステップにおいてすべての節がsatisfied でない場合には、unitの節が存在するか否かを判定し、unitの節が存在する場合には、それらの節がinconsistentであるか否かを判定し、inconsistentである場合には、第６のステップに進み、inconsistentでない場合には、コンシステント・ユニット部において前記総合判定部の出力を入力とし、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、第１のステップに戻る第４のステップと、
状態判定部の総合判定部において前記第１ステップの出力を入力とし、第４のステップにおいてunitの節が存在しない場合には、ブランチ部において前記総合判定部の出力を入力としbinaryの節に最も多く含まれる変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、第１のステップに戻る第５のステップと、
バックトラック部において前記総合判定部の出力を入力とし、current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減し、第１のステップに戻る第６のステップとを有し、
前記第１乃至第６のステップにおける処理をすべてフィールドプログラマブルゲートアレイ（ＦＰＧＡ）で実現し、すべての処理を同時に並列して行うことを特徴とする和積形論理式の充足判定方法。
【請求項３】
所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定装置であって、
節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態を判別する状態判定手段と、
前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth の値を格納する変数格納手段と、
前記状態判定手段で判定された各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態からsatisfied ，not-satisfied ，unit，binary，trinary のいずれかにある各節の状態を判定して各節の状態を統合し、この結果、not-satisfied およびunitの節が存在せず、かつすべての節がsatisfied でない場合に、ブランチ出力を発生し、すべての節がsatisfied である場合に、充足出力を発生し、not-satisfied の節が存在せず、かつunitの節が存在し、それらがinconsistentでない場合に、コンシステント・ユニット出力を発生し、not-satisfied の節が１つでも存在するかまたはすべての節がsatisfied またはinconsistentなunitの節が存在する場合、バックトラック出力を発生する総合判定手段と、
前記総合判定手段からのコンシステント・ユニット出力に応答し、unitの節に含まれるdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定するコンシステント・ユニット手段と、
前記総合判定手段からのブランチ出力に応答し、binaryの節に最も多く含まれる変数を選択し、同数の場合は、より上位の変数を選択し、変数の値、determined、およびbranchをそれぞれ０，１、および１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加するブランチ手段と、
前記総合判定手段からのバックトラック出力に応答し、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１に低減するバックトラック手段と、
前記総合判定手段からの充足出力に応答し、前記和積形論理式が充足したことを出力する充足出力手段と
を有することを特徴とする和積形論理式の充足判定装置。
【請求項４】
所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定装置であって、
節毎のパートにおいて、変数格納手段の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態を判別する状態判定手段と、
前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth の値を格納する変数格納手段と、
前記状態判定手段で判定された各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態からsatisfied ，not-satisfied ，unit，binary，trinary のいずれかにある各節の状態を判定して各節の状態を統合し、この結果、not-satisfied およびunitの節が存在せず、かつすべての節がsatisfied でない場合に、ブランチ出力を発生し、すべての節がsatisfied である場合に、充足出力を発生し、not-satisfied の節が存在せず、かつunitの節が存在し、それらがinconsistentでない場合に、コンシステント・ユニット出力を発生し、not-satisfied の節が１つでも存在するかまたはすべての節がsatisfied またはinconsistentなunitの節が存在する場合、バックトラック出力を発生する総合判定手段と、
前記総合判定手段からのコンシステント・ユニット出力に応答し、unitの節に含まれるdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定するコンシステント・ユニット手段と、
前記総合判定手段からのブランチ出力に応答し、binaryの節に最も多く含まれる変数を選択し、同数の場合は、より上位の変数を選択し、変数の値、determined、およびbranchをそれぞれ０，１、および１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加するブランチ手段と、
前記総合判定手段からのバックトラック出力に応答し、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１に低減するバックトラック手段と、
前記総合判定手段からの充足出力に応答し、前記和積形論理式が充足したことを出力する充足出力手段とを有し、
前記各手段をフィールドプログラマブルゲートアレイ（ＦＰＧＡ）で実現し、各手段により各処理をすべて同時に並列して行うことを特徴とする和積形論理式の充足判定装置。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、所与の和積形式の２値論理式を充足する変数の値の割り当てが存在するかどうかを判定する問題を解析し、充足するときには充足解を出力する和積形論理式の充足判定方法および装置に関する。
【０００２】
【従来の技術】
まず、和積形論理式の充足可能性問題について説明する。２値変数ｘi は真か偽のいずれかをとる（それぞれを１と０で表わす）。変数の否定ｘi ′（否定はダッシュ「′」で表すものとする）は変数の値が０の時１、１の時０となる。変数およびその否定をリテラルと呼ぶ。リテラルｌk （ｋ＝０，…，ｍ）の和ｌ0 ＋ｌ1 ＋，…，ｌm は節と呼ばれる。演算、和（＋）により、節はリテラルが１つでも１である場合には１となり、そうでない場合は０となる。和積形論理式とは、節をＣn （ｎ＝０，…，ｐ）とすると、節の積（Ｃ0 ・Ｃ1 ・，…，・Ｃp ）である。演算、積（・）により、論理式はすべての節が１であるときに１となり、それ以外の時は０となる。充足可能性問題は与えられた論理式を真（すなわち１）とする変数への値の割り当てが存在するかどうかを調べる問題であり、１とする変数への割り当てを充足解と呼ぶ。
【０００３】
例えば、変数が（ｘ5 ，ｘ4 ，ｘ3 ，ｘ2 ，ｘ1 ）で、節がＣ1 ＝ｘ5 ＋ｘ4 ＋ｘ1 ，Ｃ2 ＝ｘ4 ＋ｘ3 ＋ｘ1 ′，Ｃ3 ＝ｘ5 ＋ｘ2 ＋ｘ1 ′の場合、変数への値の割り当てが、（ｘ5 ，ｘ4 ，ｘ3 ，ｘ2 ，ｘ1 ）＝（０，０，１，１，１）の時にすべての節が１になるため、この論理式は充足可能であり、（０，０，１，１，１）が充足解の１つである。
【０００４】
和積形論理式の充足判定問題は変数の数が増大するにつれて、変数への値の割り当ての数が指数関数的に増大していき、変数の数が大きい場合に解くことが困難な問題として知られている。この問題を解く最も単純な方法はすべての変数の組み合わせを調べ上げることであるが、変数の数が大きくなるとこの方法は時間がかかりすぎ、現実的ではなくなる。そこで、これまでに汎用計算機上で実行するための様々な方法（アルゴリズム）が考え出されていた。
【０００５】
また、本発明者らが提案した和積形論理式の充足判定問題解析方法および装置（特願平８−２４６２４４号）においては、変数の評価の順番が固定であったため、ソフトウェアを汎用計算機上で実行する場合のように変数の評価の順番を変更しながら評価を進めていく場合に比べ、削減可能な探索領域が少なかった。
【０００６】
【発明が解決しようとする課題】
上述したように、従来、和積形論理式の変数への値の割り当ておよび変数の評価などを計算機を用いて逐次的に行う方法では時間がかかる。また、特願平８−２４６２４４号で提案した方法および装置では変数の評価順が変更できないという欠点がある。
【０００７】
本発明は、上記に鑑みてなされたもので、その目的とするところは、和積形論理式の充足判定問題を高速に解析することができる和積形論理式の充足判定方法および装置を提供することにある。
【０００８】
【課題を解決するための手段】
上記目的を達成するため、請求項１記載の本発明は、所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定方法にあって、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式のすべての節の状態を判定する第１のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、この判定した節の状態においてnot-satisfiedの節が存在するか否かを判定し、not-satisfiedの節が存在する場合には、第６のステップに進む第２のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、第２のステップにおいてnot-satisfiedの節が存在する場合には現在の値の割り当てが解であり、determinedが０の変数の値はdon't careであり、状態判定部の総合判定部において出力を入力とし、充足出力部より前記解を出力して、第６のステップに進む第３のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、第３のステップにおいて全ての節がsatisfiedでない場合には、unitの節が存在するか否かを判定し、unitの節が存在する場合には、それらの節がinconsistentであるか否かを判定し、inconsistentである場合には、第６のステップに進み、inconsistentでない場合には、コンシステント・ユニット部において前記総合判定部の出力を入力とし、それらの全ての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depthをcurrent_depthに設定し、第１のステップに戻る第４のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、第４のステップにおいてunitの節が存在しない場合にはブランチ部において前記総合判定部の出力を入力としbinaryの節に最も多く含まれる変数を選択し、その変数の値、determined、およびbranchをそれぞれ０、１、１に設定し、depthをcurrent_depth＋１に設定し、current_depthを１増加し、第１のステップに戻る第５のステップと、バックトラック部において前記総合判定部の出力を入力とし、current_depthが０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対して、depth=current_depth、かつbranch=０の場合にはdeterminedおよびdepthを０に設定し、depth=current_depth、かつbranch=１の場合にはその変数の値を１に設定し、depthをcurrent_depth-1に設定し、かつbranchを０に設定し、更にcurrent_depthを１低減し、第１のステップに戻る第６のステップと、を有することを要旨とする。
【０００９】
請求項１記載の本発明にあっては、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、not-satisfied の節が存在するかの判定、すべての節がsatisfied であるかの判定、unitの節が存在するかの判定を行い、not-satisfied の節が存在せず、すべての節がsatisfied である場合には、現在の値の割り当てを解として出力し、すべての節がsatisfied でなく、unitの節が存在する場合には、inconsistentであるか否かを判定し、inconsistentでない場合には、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、unitの節が存在しない場合には、binaryの節に最も多く含まれる変数を選択し、同数の場合には、より上位の変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、前記処理でnot-satisfied の節が１つでも存在するかまたはすべての節がsatisfied であるかまたはそれらがinconsistentでない場合には、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減するという各処理を繰り返して行い、探索領域を削減することにより、和積形論理式が充足可能かどうか判定し、その充足解を求めることができる。
【００１０】
また、請求項２記載の本発明は、所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定方法であって、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式のすべての節の状態を判定する第１のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、この判定した節の状態においてnot-satisfied の節が存在するか否かを判定し、not-satisfied の節が存在する場合には、第６のステップに進む第２のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、第２のステップにおいてnot-satisfied の節が存在しない場合には、すべての節がsatisfied であるか否かを判定し、satisfied である場合には、現在の値の割り当てが解であり、determinedが０の変数の値はdon't careであり、状態判定部の総合判定部において出力を入力とし、充足出力部より前記解を出力して、第６のステップに進む第３のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、第３のステップにおいてすべての節がsatisfied でない場合には、unitの節が存在するか否かを判定し、unitの節が存在する場合には、それらの節がinconsistentであるか否かを判定し、inconsistentである場合には、第６のステップに進み、inconsistentでない場合には、コンシステント・ユニット部において前記総合判定部の出力を入力とし、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、第１のステップに戻る第４のステップと、状態判定部の総合判定部において前記第１ステップの出力を入力とし、第４のステップにおいてunitの節が存在しない場合には、ブランチ部において前記総合判定部の出力を入力としbinaryの節に最も多く含まれる変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、第１のステップに戻る第５のステップと、
バックトラック部において前記総合判定部の出力を入力とし、current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減し、第１のステップに戻る第６のステップとを有し、前記第１乃至第６のステップにおける処理をすべてフィールドプログラマブルゲートアレイ（ＦＰＧＡ）で実現し、すべての処理を同時に並列して行うことを要旨とする。
【００１１】
請求項２記載の本発明にあっては、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、not-satisfied の節が存在するかの判定、すべての節がsatisfied であるかの判定、unitの節が存在するかの判定を行い、not-satisfied の節が存在せず、すべての節がsatisfied である場合には、現在の値の割り当てを解として出力し、すべての節がsatisfied でなく、unitの節が存在する場合には、inconsistentであるか否かを判定し、inconsistentでない場合には、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、unitの節が存在しない場合には、binaryの節に最も多く含まれる変数を選択し、同数の場合には、より上位の変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、前記処理でnot-satisfied の節が１つでも存在するかまたはすべての節がsatisfied であるかまたはそれらがinconsistentでない場合には、 バックトラック部において前記総合判定部の出力を入力とし、current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減するという各処理をフィールドプログラマブルゲートアレイ（ＦＰＧＡ）で実現し、各処理を同時に並列して行い、探索領域を削減することにより、和積形論理式が充足可能かどうかを高速に判定し、その充足解を短時間で求めることができる。
【００１２】
更に、請求項３記載の本発明は、所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定装置であって、節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態を判別する状態判定手段と、前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth の値を格納する変数格納手段と、前記状態判定手段で判定された各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態からsatisfied ，not-satisfied ，unit，binary，trinary のいずれかにある各節の状態を判定して各節の状態を統合し、この結果、not-satisfied およびunitの節が存在せず、かつすべての節がsatisfied でない場合に、ブランチ出力を発生し、すべての節がsatisfied である場合に、充足出力を発生し、not-satisfied の節が存在せず、かつunitの節が存在し、それらがinconsistentでない場合に、コンシステント・ユニット出力を発生し、not-satisfied の節が１つでも存在するかまたはすべての節がsatisfied またはinconsistentなunitの節が存在する場合、バックトラック出力を発生する総合判定手段と、前記総合判定手段からのコンシステント・ユニット出力に応答し、unitの節に含まれるdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定するコンシステント・ユニット手段と、前記総合判定手段からのブランチ出力に応答し、binaryの節に最も多く含まれる変数を選択し、同数の場合は、より上位の変数を選択し、変数の値、determined、およびbranchをそれぞれ０，１、および１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加するブランチ手段と、前記総合判定手段からのバックトラック出力に応答し、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１に低減するバックトラック手段と、前記総合判定手段からの充足出力に応答し、前記和積形論理式が充足したことを出力する充足出力手段とを有することを要旨とする。
【００１３】
請求項３記載の本発明にあっては、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、not-satisfied の節が存在するかの判定、すべての節がsatisfied であるかの判定、unitの節が存在するかの判定を行い、not-satisfied の節が存在せず、すべての節がsatisfied である場合には、現在の値の割り当てを解として出力し、すべての節がsatisfied でなく、unitの節が存在する場合には、inconsistentであるか否かを判定し、inconsistentでない場合には、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、unitの節が存在しない場合には、binaryの節に最も多く含まれる変数を選択し、同数の場合には、より上位の変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、前記処理でnot-satisfied の節が１つでも存在するかまたはすべての節がsatisfied であるかまたはそれらがinconsistentでない場合には、バックトラック部において前記総合判定部の出力を入力とし、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減するという各処理を繰り返して行い、探索領域を削減することにより、和積形論理式が充足可能かどうか判定し、その充足解を求めることができる。
【００１４】
請求項４記載の本発明は、所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定装置であって、節毎のパートにおいて、変数格納手段の各変数毎の値、determined, branch, depthの変数の状態を入力とし、前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態を判別する状態判定手段と、前記和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth の値を格納する変数格納手段と、前記状態判定手段で判定された各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態からsatisfied ，not-satisfied ，unit，binary，trinary のいずれかにある各節の状態を判定して各節の状態を統合し、この結果、not-satisfied およびunitの節が存在せず、かつすべての節がsatisfied でない場合に、ブランチ出力を発生し、すべての節がsatisfied である場合に、充足出力を発生し、not-satisfied の節が存在せず、かつunitの節が存在し、それらがinconsistentでない場合に、コンシステント・ユニット出力を発生し、not-satisfied の節が１つでも存在するかまたはすべての節がsatisfied またはinconsistentなunitの節が存在する場合、バックトラック出力を発生する総合判定手段と、前記総合判定手段からのコンシステント・ユニット出力に応答し、unitの節に含まれるdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定するコンシステント・ユニット手段と、前記状態判定手段の前記総合判定手段からのブランチ出力に応答し、コンシステント・ユニット手段において前記総合判定手段の出力を入力とし、  binaryの節に最も多く含まれる変数を選択し、同数の場合は、より上位の変数を選択し、変数の値、determined、およびbranchをそれぞれ０，１、および１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加するブランチ手段と、前記総合判定手段からのバックトラック出力に応答し、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１に低減するバックトラック手段と、前記総合判定手段からの充足出力に応答し、前記和積形論理式が充足したことを出力する充足出力手段とを有し、前記各手段をフィールドプログラマブルゲートアレイ（ＦＰＧＡ）で実現し、各手段により各処理をすべて同時に並列して行うことを要旨とする。
【００１５】
請求項４記載の本発明にあっては、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、determined, branch, depthの変数の状態を入力とし、not-satisfied の節が存在するかの判定、すべての節がsatisfied であるかの判定、unitの節が存在するかの判定を行い、not-satisfied の節が存在せず、すべての節がsatisfied である場合には、現在の値の割り当てを解として出力し、すべての節がsatisfied でなく、unitの節が存在する場合には、inconsistentであるか否かを判定し、inconsistentでない場合には、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、unitの節が存在しない場合には、binaryの節に最も多く含まれる変数を選択し、同数の場合には、より上位の変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、前記処理でnot-satisfied の節が１つでも存在するかまたはすべての節がsatisfied であるかまたはそれらがinconsistentでない場合には、バックトラック部において前記総合判定部の出力を入力とし、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減するという各処理をフィールドプログラマブルゲートアレイ（ＦＰＧＡ）で実現し、各処理を同時に並列して行い、探索領域を削減することにより、和積形論理式が充足可能かどうかを高速に判定し、その充足解を短時間で求めることができる。
【００１６】
【発明の実施の形態】
以下、図面を用いて本発明の実施の形態について説明する。
【００１７】
図１は、本発明の一実施形態に係る和積形論理式の充足判定装置の構成を示すブロック図である。同図に示す和積形論理式の充足判定装置は、所与の和積形論理式を充足する変数の割り当てが存在するかどうか判定する和積形論理式の充足判定問題を解決する処理を構成するハードウェアをユーザが使用時に内部論理を自由に書き換えることができるフィールドプログラマブルゲートアレイ（以下、ＦＰＧＡと略称する）に代表されるＬＳＩにより構成し、これによりソフトウェアまたはハードウェアで逐次的に評価される各変数の値をＦＰＧＡ等のハードウェアの並列性を利用して同時に評価するとともに、その並列性を活かした探索空間の枝刈りを高速に行うものである。
【００１８】
まず、ＦＰＧＡについて説明する。図２は、ＦＰＧＡの典型的な内部構造を示す図である。典型的なＦＰＧＡはロジックブロック、ロジックブロック間を繋ぐ配線、配線を制御するスイッチで構成されている。ロジックブロックはＬＵＴ（Look-Up Table ）、記憶素子であるフリップフロップにより構成されている。ＬＵＴはｎ入力１出力程度（ｎは３から４程度が多い）の書換え可能なテーブル（ＳＲＡＭ等で構成されることが多い）で、すべての入力値パターンに対する出力値が書き込まれており、任意のｎ入力１出力の論理関数を表現することができる。複数のＬＵＴを接続することによりｎを越える多入力の論理関数を表わすことができる。また、フリップフロップを用いて値を保持することにより、順序回路を作ることが可能である。
【００１９】
次に、図１に示す和積形論理式の充足判定装置の構成および作用を説明する前に、本発明で使用される各種表現および定義について説明する。
【００２０】
（１）ｘi を（ｘi ，１），ｘi ′を（ｘi ，０）と表現する。
【００２１】
（２）各変数ｘi に対してその状態を示す値determined（ｘi ）を定義する。determined（ｘi ）の値が１の時、その変数の値が決定されていることを意味する。初期値は０とする。
【００２２】
（３）各変数ｘi に対して、 depth（ｘi ）を定義する。depth は変数の値が決定された時の探索木の深さの位置を表わす。初期値は０とする。
【００２３】
（４）各変数ｘi に対して、branch（ｘi ）を定義する。branchの値が１の時、その変数の値がbranchの手続きによって決定されたことを表わす。０の時、unitの手続きによって決定されたことを表わす。初期値は０とする。
【００２４】
（５）大域変数 current−depth を定義する。初期値は０とする。
【００２５】
（６）各節（ｘi ，ｖi ）＋（ｘj ，ｖj ）＋（ｘk ，ｖk ）に対して、節の状態をsatisfied からtrinary まで、次のように定義する。
satisfied ：determined（ｘi ）＝１
かつｘi の値がｖi に等しい、
または  determined（ｘj ）＝１
かつｘj の値がｖj に等しい、
または  determined（ｘk ）＝１
かつｘk の値がｖk に等しい。
not-satisfied ：ｘi ，ｘj ，ｘk のすべてのdeterminedが１で、かつどの変数値もｖi ，ｖj ，ｖk に等しくない。
unit：ｘi ，ｘj ，ｘk のいずれかの２つのdeterminedが１で、残りの１つのdeterminedが０、determinedが１の変数の値がｖi ，ｖj ，ｖk が等しくない。
binary：ｘi ，ｘj ，ｘk のいずれかの１つのdeterminedが１で、残りの２つのdeterminedが０、determinedが１の変数の値がｖi ，ｖj ，ｖk に等しくない。
trinary ：ｘi ，ｘj ，ｘk のすべてのdeterminedが０である。
【００２６】
（７）unitの節が存在する場合、unitの節に含まれる変数のうち、値が決まっていない変数はその節の制約を満たすように自動的にその値が決定される。しかし、複数のunitの節が同じ変数に異なる値を割り当てようとする可能性がある。そのような場合、inconsistentと呼ぶ。
【００２７】
次に、図１に示す和積形論理式の充足判定装置の構成について説明する。
【００２８】
図１に示す和積形論理式の充足判定装置は、所与の和積形論理式の各変数ｘi 〜ｘn の値、unit，determined，branch，depth 、および current−depth の値を格納して入出力する変数格納部１と、和積形論理式の各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態を判別する状態判定部３と、該状態判定部３内に設けられ、該状態判定部３で判定された各変数の値、unit，determined，branch，depth 、および current−depth より与えられる論理式の状態からsatisfied ，not-satisfied ，unit，binary，trinary のいずれかにある各節の状態を判定して各節の状態を統合し、この結果、not-satisfied およびunitの節が存在せず、かつすべての節がsatisfied でない場合に、ブランチ出力を発生し、すべての節がsatisfied である場合に、充足出力を発生し、not-satisfied の節が存在せず、かつunitの節が存在し、それらがinconsistentでない場合に、コンシステント・ユニット出力を発生し、not-satisfied の節が１つでも存在するかまたはすべての節がsatisfied またはinconsistentなunitの節が存在する場合、バックトラック出力を発生する総合判定部５と、該総合判定部５からのコンシステント・ユニット出力に応答し、unitの節に含まれるdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定するコンシステント・ユニット部７と、総合判定部５からのブランチ出力に応答し、binaryの節に最も多く含まれる変数を選択し、同数の場合は、より上位の変数を選択し、変数の値、determined、およびbranchをそれぞれ０，１、および１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加するブランチ部９と、総合判定部５からのバックトラック出力に応答し、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合には、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合には、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１に低減するバックトラック部１１と、総合判定部５からの充足出力に応答し、和積形論理式が充足したことを出力する充足出力部１３とを有する。
【００２９】
図１に示す和積形論理式の充足判定装置の各構成部は、すべてＦＰＧＡで実現され、各構成部により各処理をすべて同時に並列して行い、所与の和積形論理式が充足可能かどうかを迅速に判定するとともに、充足解を高速に求めている。
【００３０】
変数格納部１では、変数の個数により必要となる大きさが異なるため、ＦＰＧＡを用いることにより、与えられた問題の変数の個数に応じて、その大きさを変更することができる。
【００３１】
状態判定部３において、節Ｃ1 からＣm は所与の論理式の各節に対応する。変数と節の接続が変数と節の関係を表すので、所与の論理式毎に変更する必要があり、それをＦＰＧＡで実現している。各節の状態はsatisfied ，not-satisfied ，unit，binary，trinary のいずれかであり、総合判定部５は各節の状態をすべて統合し、各変数等が取るべき値をどのように計算するかを決定して、ブランチ出力、充足出力、コンシステント・ユニット出力、バックトラック出力をそれぞれブランチ部９、充足出力部１３、コンシステント・ユニット部７、バックトラック部１１に出力している。
【００３２】
なお、図１に示す和積形論理式の充足判定装置の各構成部はすべてＦＰＧＡで構成することにより、各構成部の各処理を同時に並列して行うことができ、処理の高速化を図ることができるものであるが、各構成部のすべてをＦＰＧＡで構成しなくても、与えられた和積形論理式を構成する部分をＦＰＧＡで構成し、他の構成部を通常のハードウェアで構成しても同様に処理の高速化を図ることができるし、またＦＰＧＡとハードウェアを適宜組み合わせて構成してもよい。
【００３３】
次に、上述したように構成される和積形論理式の充足判定装置をＦＰＧＡで構成するためのＦＰＧＡの内部論理を作成する手順について図３に示すフローチャートを参照して説明する。
【００３４】
図３において、和積形論理式の充足可能性問題が与えられると（ステップＳ１）、この与えられた和積形論理式を分析し、ＨＤＬ（Hardware Description Language ）記述作成プログラムを用いて、和積形論理式の充足解探索に適したハードウェア構成をハードウェア記述言語であるＨＤＬにより記述して出力する（ステップＳ２）。このＨＤＬにより問題を記述し（ステップＳ３）、論理合成プログラムを用いて、記述されたハードウェアのソースから論理合成、論理圧縮等を行い、ＡＮＤ，ＯＲ等のゲートで構成されたネットリストを作成する（ステップＳ４，Ｓ５）。
【００３５】
ＦＰＧＡのマッピングプログラムを用いて、前記論理合成プログラムで作成されるネットリストをＦＰＧＡの構造に適したデータに変換して、ＦＰＧＡマッピングデータを作成し（ステップＳ６，Ｓ７）、このＦＰＧＡマッピングデータをＦＰＧＡ上に転送することにより、和積形論理式の充足解を探索するハードウェアを構成することができる（ステップＳ８）。
【００３６】
このように構成されるＦＰＧＡを動作させることにより、和積形論理式を充足する変数の割り当てが存在するか否かを高速に判定することができるとともに、充足する場合には充足解を迅速に得ることができる。
【００３７】
次に、以上のように構成される和積形論理式の充足判定装置の作用について図４に示すフローチャートを参照して説明する。
【００３８】
まず、所与の和積形論理式のすべての節の状態を判定し（ステップＳ１１）、この判定した各節の状態に対して次に示す各判定処理を行う。
【００３９】
［１］Not Satisfied ：not-satisfied の節が１つでも存在するか否かをチェックし（ステップＳ１３）、存在する場合には、［５］（ステップＳ２７，Ｓ２９）に進む。
【００４０】
［２］Satisfied ：すべての節がsatisfied であるか否かをチェックし（ステップＳ１５）、satisfied なら、ステップＳ１７に進み、現在の値の割り当てが解であり、determinedが０の変数の値はdon't care（０，１のどちらでもよい）である。解を出力して、［５］（ステップＳ２７，Ｓ２９）へ進む。
【００４１】
［３］Unit：unitの節が存在するか否かをチェックし（ステップＳ１９）、存在する場合：
（ａ）それらの節がinconsistentであるか否かをチェックし（ステップＳ２１）、inconsistentでないなら、それらのすべての節に対して、determinedが０の変数ｘl の値を節で指定される値ｖl に設定し、determined（ｘl ）を１にし、branch（ｘl ）を０に設定し、 depth（ｘl ）を current−depth に設定し（ステップＳ２３）、［１］（ステップＳ１１）に戻る。
（ｂ）inconsistentの節が存在するなら、［５］（ステップＳ２７，Ｓ２９）に進む。
【００４２】
［４］Branching ：その他の場合はbinaryの節に（否定、肯定併せて）最も多く含まれる変数ｘl を選択する。同数の場合はより上位の変数を選択し、ｘl の値を０に、determined（ｘl ）を１に、branch（ｘl ）を１に設定し、 depth（ｘl ）を current−depth ＋１に設定し、 current−depth を１増加し（ステップＳ２５）、［１］（ステップＳ１１）戻る。
【００４３】
［５］Backtracking：
（ａ） current−depth が０であるか否かをチェックし（ステップＳ２７）、０であればアルゴリズムを終了する。
（ｂ）各変数ｘi に対して、
（ｂ-1） depth（ｘi ）＝ current−depth かつbranch（ｘi ）＝０ならば、determined（ｘi ）を０に、 depth（ｘi ）を０に設定し、
（ｂ-2） depth（ｘi ）＝ current−depth かつbranch（ｘi ）＝１ならば、ｘi の値を１に設定し、 depth（ｘi ）を current−depth −１に、branch（ｘi ）を０に設定し、
（ｃ） current−depth を１減少し、
（ｄ）main（ステップＳ１１）に戻る（ステップＳ２９）。
【００４４】
なお、図４に示す処理は、ステップＳ１１，Ｓ１３，Ｓ１５，Ｓ１９・・・などのように順次行うように示しているが、本処理をＦＰＧＡで実現する場合には、これらの順次的に行われる各処理をすべて同時に並列して行うようにしているものである。
【００４５】
次に、上述した和積形論理式の充足判定方法について、図５に示す変数等への値の割り当ての遷移を示す具体例をあげて説明する。なお、図５は上から下に向かって時間が進み、（）は値が設定されたことを示す。また、condition の部分のｕ，ｂ，ｓはそれぞれunit，binary，satisfied を示し、depth の部分のｃは current−depth を示す。
【００４６】
図５に示す具体例では、変数をｘi （ｉ＝１，…，４）とし、節をＣ1 ＝（ｘ1 ＋ｘ2 ），Ｃ2 ＝（ｘ1 ＋ｘ3 ′），Ｃ3 ＝（ｘ3 ′＋ｘ4 ），Ｃ4 ＝（ｘ3 ＋ｘ4 ′）とする。
【００４７】
初めに、ｘ1 の値を０に設定する。この時、 depth（ｘ1 ）＝１，determined（ｘ1 ）＝１，branch（ｘ1 ）＝１になる。節についてはＣ1 ，Ｃ2 の状態がunitになる。そのため、ｘ2 の値を１とし、ｘ3 の値を０とする。また、 depth（ｘ2 ）＝ depth（ｘ3 ）＝１，branch（ｘ2 ）＝branch（ｘ3 ）＝０，determined（ｘ2 ）＝determined（ｘ3 ）＝１となる。そしてＣ3 とＣ4 がunitとなるが、これらはinconsistentとなる。 current−depth ＝ depth（ｘ1 ）＝ depth（ｘ2 ）＝ depth（ｘ3 ）であるため、ｘ1 の値は１となる。また、branch（ｘ1 ）＝０， depth（ｘ1 ）＝０となる。そして、determined（ｘ2 ）とdetermined（ｘ3 ）が０になる。それにより、Ｃ1 ，Ｃ2 はsatisfied になる。そしてｘ4 の値を０にする。その時 depth（ｘ4 ）＝１，branch（ｘ4 ）＝１となる。それによりＣ3 はunitになり、よってｘ2 の値を０にする。この時、すべての節は充足され解となる。このように各変数、各節が評価され、値が決定されていく。
【００４８】
【発明の効果】
以上説明したように、本発明によれば、not-satisfied の節が存在するかの判定、すべての節がsatisfied であるかの判定、unitの節が存在するかの判定を行い、not-satisfied の節が存在せず、すべての節がsatisfied である場合には、現在の値の割り当てを解として出力し、すべての節がsatisfied でなく、unitの節が存在する場合には、inconsistentであるか否かを判定し、inconsistentでない場合には、それらのすべての節に対してdeterminedが０の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ１および０に設定し、depth を current−depth に設定し、unitの節が存在しない場合には、binaryの節に最も多く含まれる変数を選択し、同数の場合には、より上位の変数を選択し、その変数の値、determined、およびbranchをそれぞれ０，１，１に設定し、depth を current−depth ＋１に設定し、 current−depth を１増加し、前記処理でnot-satisfied の節が１つでも存在するかまたはすべての節がsatisfied であるかまたはそれらがinconsistentでない場合には、 current−depth が０であるか否かを判定し、０である場合には、処理を終了し、０でない場合には、各変数に対してdepth ＝ current−depth 、かつbranch＝０の場合、determinedおよびdepth を０に設定し、depth ＝ current−depth 、かつbranch＝１の場合、その変数の値を１に設定し、depth を current−depth −１に設定し、かつbranchを０に設定し、更に current−depth を１低減するという各処理をＦＰＧＡで実現し、各処理を同時に並列して行い、探索領域を削減することにより、和積形論理式が充足可能かどうかを高速に判定し、その充足解を短時間で求めることができる。
【図面の簡単な説明】
【図１】本発明の一実施形態に係る和積形論理式の充足判定装置の構成を示すブロック図である。
【図２】ＦＰＧＡの一例の構成を示す図である。
【図３】和積形論理式の充足判定装置をＦＰＧＡで構成するためのＦＰＧＡの内部論理を作成する手順を示すフローチャートである。
【図４】図１に示す和積形論理式の充足判定装置の作用である充足判定方法を示すフローチャートである。
【図５】図４に示す和積形論理式の充足判定方法に対して変数等への値の割り当ての遷移を示す具体例を示す図である。
【符号の説明】
１  変数格納部
３  状態判定部
５  総合判定部
７  コンシステント・ユニット部
９  ブランチ部
１１  バックトラック部
１３  充足出力部
【図１】
0003648370.tif 000002
【図２】
0003648370.tif 000003
【図３】
0003648370.tif 000004
【図４】
0003648370.tif 000005
【図５】
0003648370.tif 000006