JP3648370B2

JP3648370B2 - Satisfaction judgment method and apparatus for sum product type logic

Info

Publication number: JP3648370B2
Application number: JP35767797A
Authority: JP
Inventors: 敬之須山; 真横尾; 宏澤田
Original assignee: Nippon Telegraph and Telephone Corp; NTT Inc USA
Current assignee: NTT Inc; NTT Inc USA
Priority date: 1997-12-25
Filing date: 1997-12-25
Publication date: 2005-05-18
Anticipated expiration: 2017-12-25
Also published as: JPH11184840A

Description

【０００１】
【発明の属する技術分野】
本発明は、所与の和積形式の２値論理式を充足する変数の値の割り当てが存在するかどうかを判定する問題を解析し、充足するときには充足解を出力する和積形論理式の充足判定方法および装置に関する。
【０００２】
【従来の技術】
まず、和積形論理式の充足可能性問題について説明する。２値変数ｘ_iは真か偽のいずれかをとる（それぞれを１と０で表わす）。変数の否定ｘ_i′（否定はダッシュ「′」で表すものとする）は変数の値が０の時１、１の時０となる。変数およびその否定をリテラルと呼ぶ。リテラルｌ_k（ｋ＝０，…，ｍ）の和ｌ₀＋ｌ₁＋，…，ｌ_mは節と呼ばれる。演算、和（＋）により、節はリテラルが１つでも１である場合には１となり、そうでない場合は０となる。和積形論理式とは、節をＣ_n（ｎ＝０，…，ｐ）とすると、節の積（Ｃ₀・Ｃ₁・，…，・Ｃ_p）である。演算、積（・）により、論理式はすべての節が１であるときに１となり、それ以外の時は０となる。充足可能性問題は与えられた論理式を真（すなわち１）とする変数への値の割り当てが存在するかどうかを調べる問題であり、１とする変数への割り当てを充足解と呼ぶ。
【０００３】
例えば、変数が（ｘ₅，ｘ₄，ｘ₃，ｘ₂，ｘ₁）で、節がＣ₁＝ｘ₅＋ｘ₄＋ｘ₁，Ｃ₂＝ｘ₄＋ｘ₃＋ｘ₁′，Ｃ₃＝ｘ₅＋ｘ₂＋ｘ₁′の場合、変数への値の割り当てが、（ｘ₅，ｘ₄，ｘ₃，ｘ₂，ｘ₁）＝（０，０，１，１，１）の時にすべての節が１になるため、この論理式は充足可能であり、（０，０，１，１，１）が充足解の１つである。
【０００４】
和積形論理式の充足判定問題は変数の数が増大するにつれて、変数への値の割り当ての数が指数関数的に増大していき、変数の数が大きい場合に解くことが困難な問題として知られている。この問題を解く最も単純な方法はすべての変数の組み合わせを調べ上げることであるが、変数の数が大きくなるとこの方法は時間がかかりすぎ、現実的ではなくなる。そこで、これまでに汎用計算機上で実行するための様々な方法（アルゴリズム）が考え出されていた。
【０００５】
また、本発明者らが提案した和積形論理式の充足判定問題解析方法および装置（特願平８−２４６２４４号）においては、変数の評価の順番が固定であったため、ソフトウェアを汎用計算機上で実行する場合のように変数の評価の順番を変更しながら評価を進めていく場合に比べ、削減可能な探索領域が少なかった。
【０００６】
【発明が解決しようとする課題】
上述したように、従来、和積形論理式の変数への値の割り当ておよび変数の評価などを計算機を用いて逐次的に行う方法では時間がかかる。また、特願平８−２４６２４４号で提案した方法および装置では変数の評価順が変更できないという欠点がある。
【０００７】
本発明は、上記に鑑みてなされたもので、その目的とするところは、和積形論理式の充足判定問題を高速に解析することができる和積形論理式の充足判定方法および装置を提供することにある。
【０００８】
【課題を解決するための手段】
上記目的を達成するため、請求項１記載の本発明は、所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定方法にあって、状態判定部の節毎のパートにおいて、変数格納部の各変数毎の値、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 を１に低減するバックトラック部１１と、総合判定部５からの充足出力に応答し、和積形論理式が充足したことを出力する充足出力部１３とを有する。
【００２９】
図１に示す和積形論理式の充足判定装置の各構成部は、すべてＦＰＧＡで実現され、各構成部により各処理をすべて同時に並列して行い、所与の和積形論理式が充足可能かどうかを迅速に判定するとともに、充足解を高速に求めている。
【００３０】
変数格納部１では、変数の個数により必要となる大きさが異なるため、ＦＰＧＡを用いることにより、与えられた問題の変数の個数に応じて、その大きさを変更することができる。
【００３１】
状態判定部３において、節Ｃ₁からＣ_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（ｉ＝１，…，４）とし、節をＣ₁＝（ｘ₁＋ｘ₂），Ｃ₂＝（ｘ₁＋ｘ₃′），Ｃ₃＝（ｘ₃′＋ｘ₄），Ｃ₄＝（ｘ₃＋ｘ₄′）とする。
【００４７】
初めに、ｘ₁の値を０に設定する。この時、 depth（ｘ₁）＝１，determined（ｘ₁）＝１，branch（ｘ₁）＝１になる。節についてはＣ₁，Ｃ₂の状態がunitになる。そのため、ｘ₂の値を１とし、ｘ₃の値を０とする。また、 depth（ｘ₂）＝ depth（ｘ₃）＝１，branch（ｘ₂）＝branch（ｘ₃）＝０，determined（ｘ₂）＝determined（ｘ₃）＝１となる。そしてＣ₃とＣ₄がunitとなるが、これらはinconsistentとなる。 current₋depth ＝ depth（ｘ₁）＝ depth（ｘ₂）＝ depth（ｘ₃）であるため、ｘ₁の値は１となる。また、branch（ｘ₁）＝０， depth（ｘ₁）＝０となる。そして、determined（ｘ₂）とdetermined（ｘ₃）が０になる。それにより、Ｃ₁，Ｃ₂はsatisfied になる。そしてｘ₄の値を０にする。その時 depth（ｘ₄）＝１，branch（ｘ₄）＝１となる。それによりＣ₃はunitになり、よってｘ₂の値を０にする。この時、すべての節は充足され解となる。このように各変数、各節が評価され、値が決定されていく。
【００４８】
【発明の効果】
以上説明したように、本発明によれば、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 を１低減するという各処理をＦＰＧＡで実現し、各処理を同時に並列して行い、探索領域を削減することにより、和積形論理式が充足可能かどうかを高速に判定し、その充足解を短時間で求めることができる。
【図面の簡単な説明】
【図１】本発明の一実施形態に係る和積形論理式の充足判定装置の構成を示すブロック図である。
【図２】ＦＰＧＡの一例の構成を示す図である。
【図３】和積形論理式の充足判定装置をＦＰＧＡで構成するためのＦＰＧＡの内部論理を作成する手順を示すフローチャートである。
【図４】図１に示す和積形論理式の充足判定装置の作用である充足判定方法を示すフローチャートである。
【図５】図４に示す和積形論理式の充足判定方法に対して変数等への値の割り当ての遷移を示す具体例を示す図である。
【符号の説明】
１変数格納部
３状態判定部
５総合判定部
７コンシステント・ユニット部
９ブランチ部
１１バックトラック部
１３充足出力部[0001]
BACKGROUND OF THE INVENTION
The present invention analyzes the problem of determining whether there is an assignment of the value of a variable that satisfies a binary formula in a given sum-product form, and outputs a satisfaction solution when satisfied. The present invention relates to a satisfaction determination method and apparatus.
[0002]
[Prior art]
First, the satisfiability problem of sum-product type logical expressions will be described. Binary variable x _i Is either true or false (respectively represented by 1 and 0). Negation of variable x _i ′ (Negation is represented by a dash “′”) is 1 when the value of the variable is 0, and 0 when the value of the variable is 1. A variable and its negation are called literals. Literal l _k Sum l of (k = 0, ..., m) ₀ + L ₁ +, ..., l _m Is called a clause. By the operation, the sum (+), the clause becomes 1 if even one literal is 1, otherwise it becomes 0. A sum-form formula is a C clause _n (N = 0, ..., p), the product of clauses (C ₀ ・ C ₁ ・・・・・, ・ C _p ). Due to the operation, product (•), the logical expression becomes 1 when all the clauses are 1, and 0 otherwise. The satisfiability problem is a problem to check whether there is an assignment of a value to a variable for which a given logical expression is true (that is, 1). The assignment to a variable of 1 is called a satisfiability solution.
[0003]
For example, if the variable is (x _Five , X _Four , X _Three , X ₂ , X ₁ ) ₁ = X _Five + X _Four + X ₁ , C ₂ = X _Four + X _Three + X ₁ ', C _Three = X _Five + X ₂ + X ₁ In the case of ′, the value assignment to the variable is (x _Five , X _Four , X _Three , X ₂ , X ₁ ) = (0,0,1,1,1), all the clauses become 1, so this logical expression can be satisfied, and (0,0,1,1,1) is one of the satisfactory solutions. It is.
[0004]
As the number of variables increases, the number of assignments of values to variables grows exponentially as the number of variables increases, and it is difficult to solve when the number of variables is large. Are known. The simplest way to solve this problem is to look up all combinations of variables, but as the number of variables increases, this method takes too much time and becomes impractical. So far, various methods (algorithms) have been devised for execution on general-purpose computers.
[0005]
In addition, in the method and apparatus for analyzing the satisfaction of a product-product logical expression proposed by the present inventors (Japanese Patent Application No. 8-246244), the order of evaluation of the variables is fixed, so the software is installed on a general-purpose computer. Compared to the case where the evaluation is advanced while changing the order of the evaluation of the variables as in the case of executing in (3), the search area that can be reduced is small.
[0006]
[Problems to be solved by the invention]
As described above, conventionally, it takes time in a method of sequentially assigning values to variables of sum-product logic formulas and evaluating variables using a computer. Further, the method and apparatus proposed in Japanese Patent Application No. 8-246244 has a drawback that the order of evaluation of variables cannot be changed.
[0007]
The present invention has been made in view of the above, and an object of the present invention is to provide a satisfaction determination method and apparatus for a sum product type logical expression that can quickly analyze the satisfaction determination problem of a sum type logical expression. There is to do.
[0008]
[Means for Solving the Problems]
In order to achieve the above object, the present invention according to claim 1 is a satisfaction determination method of a sum product type logical expression for determining whether there is an assignment of a variable that satisfies a given sum product type logical expression. In the part for each clause of the state determination unit, the values of each variable in the variable storage unit, the state of the variables of determined, branch, and depth are input, and the states of all the clauses of the sum product type logical expression are determined. 1 and the output of the first step in the overall determination unit of the state determination unit as input, determine whether or not a not-satisfied clause exists in the determined state of the clause, and determine the not-satisfied clause Is present, the second step proceeds to the sixth step, and the output of the first step is input to the comprehensive determination unit of the state determination unit, and a not-satisfied clause exists in the second step. If the current value assignment is the solution, det The value of the variable whose ermined is 0 is don't care, and the third step of the state determination unit receives the output as an input, outputs the solution from the satisfaction output unit, and proceeds to the sixth step. When the overall determination unit of the state determination unit receives the output of the first step and all the nodes are not satisfied in the third step, it is determined whether or not the unit node exists, and the unit node Is determined, whether or not the clauses are inconsistent. If inconsistent, the process proceeds to step 6. If not, the comprehensive determination is performed in the consistent unit. The output of the part is input, and for all of those clauses, the value of the variable whose determined is 0 is set to the value specified in the clause, the determined and branch are set to 1 and 0, respectively, and the depth is set to current_depth And in the first step The output of the first step is input to the fourth step and the comprehensive determination unit of the state determination unit, and if the unit clause does not exist in the fourth step, the output of the comprehensive determination unit is input to the branch unit And select the variable most contained in the binary section, set the variable's value, determined, and branch to 0, 1, 1 respectively, set depth to current_depth + 1, increase current_depth by 1, The fifth step of returning to the step and the output of the comprehensive determination unit in the backtrack unit are input, and it is determined whether or not current_depth is 0. If it is 0, the process is terminated, and if it is not 0 For each variable, if depth = current_depth and branch = 0, the determined and depth are set to 0, and if depth = current_depth and branch = 1, the value of that variable is set to 1. And set depth to current_de The gist of the present invention is to have a sixth step of setting pth-1 and setting branch to 0, further reducing current_depth by 1, and returning to the first step.
[0009]
In the first aspect of the present invention, in the part for each section of the state determination section, the value of each variable in the variable storage section, the state of the variable of determined, branch, and depth are input, and the not-satisfied section If there is no not-satisfied clause and all clauses are satisfied , Output the current value assignment as a solution, and if all clauses are not satisfied and a unit clause exists, determine if they are inconsistent, and if they are not inconsistent, all of them If the value of the variable whose determined is 0 for the clause is set to the value specified in the clause, the determined and branch are set to 1 and 0 respectively, the depth is set to current-depth, and the unit clause does not exist To select the variables most contained in the binary clause and , Select a higher-order variable, set its value, determined and branch to 0, 1, 1 respectively, set depth to current-depth +1, increase current-depth by 1, If there is at least one not-satisfied clause, or if all clauses are satisfied or they are not inconsistent, determine whether current-depth is zero, and if it is zero If the process is not 0 and depth = current-depth and branch = 0 for each variable, then determined and depth are set to 0, and depth = current-depth and branch = 1. If the variable is set to 1, the depth is set to current-depth -1, the branch is set to 0, and the current-depth is further reduced by 1 to repeat the search region. Whether or not the sum formula can be satisfied by reducing Constant and can be determined the satisfaction solution.
[0010]
Further, the present invention according to claim 2 is a satisfaction determination method for a sum product type logical expression that determines whether there is an assignment of a variable that satisfies a given sum product type logical expression, In the part for each clause, a first step for determining the status of all clauses of the sum-form logical expression using the value of each variable in the variable storage unit, the state of the variable of determined, branch, and depth as inputs, When the output of the first step is input to the general determination unit of the state determination unit, it is determined whether or not a not-satisfied clause exists in the determined state of the clause, and if a not-satisfied clause exists If the output of the first step is input to the second step that proceeds to the sixth step and the overall determination unit of the state determination unit, and there is no not-satisfied clause in the second step, all To determine whether the clause in the book is satisfied If it is fied, the assignment of the current value is the solution, the value of the variable whose determined is 0 is don't care, and the output is input to the comprehensive determination unit of the state determination unit. When the output of the first step is input to the third step that outputs the solution and proceeds to the sixth step, and the overall determination unit of the state determination unit, and all the clauses are not satisfied in the third step , Determine whether there is a unit clause, and if there are unit clauses, determine whether these clauses are inconsistent. If they are inconsistent, go to the sixth step. If it is not inconsistent, the output of the comprehensive judgment unit is input to the consistent unit unit, and the values of variables whose determined value is 0 are set to the values specified in the clauses for all of the clauses. 1 each for determined and branch And the depth is set to current-depth, the output of the first step is input to the fourth step that returns to the first step, and the overall determination unit of the state determination unit. In the fourth step If the unit clause does not exist, the branch unit selects the variable that is included most in the binary clause by using the output of the comprehensive judgment unit as an input, and sets the value of the variable, determined, and branch to 0, 1, A fifth step of setting 1, depth to current-depth +1, increasing current-depth by 1, and returning to the first step;
In the backtrack unit, the output of the comprehensive determination unit is used as an input, and it is determined whether or not current-depth is 0. If it is 0, the process is terminated. If depth = current-depth and branch = 0, then determined and depth are set to 0. If depth = current-depth and branch = 1, the value of the variable is set to 1. the depth is set to current-depth -1, the branch is set to 0, the current-depth is further reduced by 1, and the sixth step returns to the first step. The gist is that all processes in the steps are realized by a field programmable gate array (FPGA) and all processes are performed in parallel at the same time.
[0011]
In the present invention according to claim 2, in the part for each section of the state determination section, the value of each variable in the variable storage section, the state of the variable of determined, branch, and depth are input, and the section of not-satisfied If there is no not-satisfied clause and all clauses are satisfied , Output the current value assignment as a solution, and if all clauses are not satisfied and a unit clause exists, determine if they are inconsistent, and if they are not inconsistent, all of them If the value of the variable whose determined is 0 for the clause is set to the value specified in the clause, the determined and branch are set to 1 and 0 respectively, the depth is set to current-depth, and the unit clause does not exist To select the variables most contained in the binary clause and , Select a higher-order variable, set its value, determined and branch to 0, 1, 1 respectively, set depth to current-depth +1, increase current-depth by 1, If there is at least one not-satisfied clause, or if all clauses are satisfied or they are not inconsistent, the output of the comprehensive judgment unit is input to the backtrack unit, and current-depth is 0. If it is 0, the process is terminated. If it is not 0, the depth and the depth are set to 0 when depth = current−depth and branch = 0 for each variable. If depth = current-depth and branch = 1, set the value of that variable to 1, set depth to current-depth -1, set branch to 0, and set current-depth to Each process of reducing 1 by field programmer It is realized with a Lugate array (FPGA), each process is performed in parallel, and the search area is reduced, so that it is possible to quickly determine whether a sum-product type logical expression can be satisfied, and to satisfy the satisfaction solution in a short time Can be sought.
[0012]
Furthermore, the present invention as defined in claim 3 is a sum product type logical expression satisfaction determination device for determining whether or not there is an assignment of a variable that satisfies a given sum product type logical expression. , The value of each variable in the variable storage unit, the state of the variable of determined, branch, and depth are input, and the value of each variable of the product-form formula, unit, determined, branch, depth, and current-depth State determination means for determining the state of a given logical expression, variable storage means for storing values of each variable, unit, determined, branch, depth, and current-depth of the sum-form logical expression; and the state The value of each variable determined by the determination means, the state of the logical expression given by unit, determined, branch, depth, and current-depth, for each clause in any one of saturated, not-satisfied, unit, binary, trinary Judging the state and integrating the state of each section, If the not-satisfied and unit clauses do not exist and all clauses are not satisfied, generate branch output, and if all clauses are satisfied, generate satisfied output, and not-satisfied clauses If there are no unit clauses and they are not inconsistent, they generate a consistent unit output and there is at least one not-satisfied clause or all units are either satisfied or inconsistent If there is a clause, the overall judgment means for generating the backtrack output, and in response to the consistent unit output from the overall judgment means, the value of the variable whose determined is 0 is specified in the clause The consistent unit means for setting the determined and branch to 1 and 0 and setting the depth to current-depth, and the branch output from the comprehensive judgment means. Answer, select the variable that is contained most in the binary section, if it is the same number, select the higher-order variable, set the variable value, determined, and branch to 0, 1, and 1, respectively. In response to the backtrack output from the branch means that increments current-depth by 1 and the comprehensive judgment means, and determines whether or not current-depth is 0. In the case, the process is terminated, and if not 0, depth = current-depth is set for each variable, and if branch = 0, determined and depth are set to 0, and depth = current-depth, If branch = 1, the value of the variable is set to 1, the depth is set to current-depth-1, the branch is set to 0, and the current-depth is further reduced to 1. And in response to the satisfaction output from the comprehensive determination means, And summarized in that form logical expression and an sufficiency output means for outputting that satisfied.
[0013]
In the third aspect of the present invention, in the part for each section of the state determination section, the value of each variable in the variable storage section, the state of the variable of determined, branch, and depth are input, and the not-satisfied section If there is no not-satisfied clause and all clauses are satisfied , Output the current value assignment as a solution, and if all clauses are not satisfied and a unit clause exists, determine if they are inconsistent, and if they are not inconsistent, all of them If the value of the variable whose determined is 0 for the clause is set to the value specified in the clause, the determined and branch are set to 1 and 0 respectively, the depth is set to current-depth, and the unit clause does not exist To select the variables most contained in the binary clause and , Select a higher-order variable, set its value, determined and branch to 0, 1, 1 respectively, set depth to current-depth +1, increase current-depth by 1, If there is at least one not-satisfied clause, or if all clauses are satisfied or they are not inconsistent, the output of the comprehensive judgment unit is input to the backtrack unit, and current-depth is 0. If it is 0, the process is terminated. If it is not 0, the depth and the depth are set to 0 when depth = current−depth and branch = 0 for each variable. If depth = current-depth and branch = 1, set the value of that variable to 1, set depth to current-depth -1, set branch to 0, and set current-depth to Repeat the process of reducing 1 and search By reducing the frequency, it is determined whether KazuTsumorukatachi logical expression is satisfiable, can obtain the satisfaction solution.
[0014]
The invention according to claim 4 is a satisfaction determination apparatus for a sum product type logical expression for determining whether or not there is an assignment of a variable that satisfies a given sum product type logical expression. The value of each variable in the variable storage means and the state of the variable of determined, branch, and depth are input, and are given from the values of each variable of the sum product type logical formula, unit, determined, branch, depth, and current-depth State determination means for determining the state of the logical expression, variable storage means for storing values of each variable, unit, determined, branch, depth, and current-depth of the sum-form logical expression, and the state determination means The state of each clause in any of saturated, not-satisfied, unit, binary, trinary from the state of the logical expression given by the value of each variable, unit, determined, branch, depth, and current-depth Judgment and integration of the state of each section, as a result, not-sa If tisfied and unit clauses do not exist and all clauses are not satisfied, branch output is generated.If all clauses are satisfied, satisfied output is generated and not-satisfied clauses are present. If there are no unit clauses and they are not inconsistent, consistent unit output is generated, and there is at least one not-satisfied clause, or all clauses are satisfied or inconsistent In response to the consistent unit output from the comprehensive determination unit and the comprehensive unit that generates the backtrack output, the value of the variable whose determined value is 0 is specified in the unit. The consistent unit means to set the value, set the determined and branch to 1 and 0, respectively, and set the depth to current-depth, from the comprehensive judgment means of the state judgment means In response to the launch output, the output of the comprehensive judgment means is input to the consistent unit means, and the variable that is included most in the binary section is selected. If the number is the same, the higher-order variable is selected, and the variable The value, determined, and branch are set to 0, 1, and 1, respectively, the depth is set to current-depth +1, and current-depth is incremented by 1, and the response to the backtrack output from the comprehensive determination unit Then, it is determined whether or not current-depth is 0. If it is 0, the process is terminated. If it is not 0, depth = current-depth and branch = 0 are set for each variable. In this case, determined and depth are set to 0, and if depth = current-depth and branch = 1, the value of the variable is set to 1, depth is set to current-depth -1, and Set branch to 0 and then current-dept backtracking means for reducing h to 1 and satisfaction output means for outputting that the sum product type logical expression is satisfied in response to the satisfaction output from the comprehensive judgment means, and each of the means is field programmable. The gist of the present invention is that it is realized by a gate array (FPGA), and each process is simultaneously performed in parallel by each means.
[0015]
In the present invention according to claim 4, in the part for each section of the state determination section, the value of each variable in the variable storage section, the state of the variable of determined, branch, and depth are input, and the not-satisfied section If there is no not-satisfied clause and all clauses are satisfied , Output the current value assignment as a solution, and if all clauses are not satisfied and a unit clause exists, determine if they are inconsistent, and if they are not inconsistent, all of them If the value of the variable whose determined is 0 for the clause is set to the value specified in the clause, the determined and branch are set to 1 and 0 respectively, the depth is set to current-depth, and the unit clause does not exist To select the variables most contained in the binary clause and , Select a higher-order variable, set its value, determined and branch to 0, 1, 1 respectively, set depth to current-depth +1, increase current-depth by 1, If there is at least one not-satisfied clause, or if all clauses are satisfied or they are not inconsistent, the output of the comprehensive judgment unit is input to the backtrack unit, and current-depth is 0. If it is 0, the process is terminated. If it is not 0, the depth and the depth are set to 0 when depth = current−depth and branch = 0 for each variable. If depth = current-depth and branch = 1, set the value of that variable to 1, set depth to current-depth -1, set branch to 0, and set current-depth to Each process of reducing 1 by field programmer It is realized with a Lugate array (FPGA), each process is performed in parallel, and the search area is reduced, so that it is possible to quickly determine whether a sum-product type logical expression can be satisfied, and to satisfy the satisfaction solution in a short time Can be sought.
[0016]
DETAILED DESCRIPTION OF THE INVENTION
Hereinafter, embodiments of the present invention will be described with reference to the drawings.
[0017]
FIG. 1 is a block diagram showing a configuration of a product-product logical expression satisfaction determination apparatus according to an embodiment of the present invention. The satisfaction determination device for sum-product type logical expressions shown in the figure performs processing for solving the satisfaction determination problem of sum-product type logical expressions that determines whether there is an assignment of a variable that satisfies a given sum-product type logical expression. The hardware to be configured is composed of an LSI typified by a field programmable gate array (hereinafter abbreviated as FPGA) that allows the user to freely rewrite the internal logic when in use, thereby enabling sequential evaluation with software or hardware. The value of each variable is simultaneously evaluated using the parallelism of the hardware such as FPGA, and the search space is pruned at high speed utilizing the parallelism.
[0018]
First, the FPGA will be described. FIG. 2 is a diagram showing a typical internal structure of the FPGA. A typical FPGA is composed of logic blocks, wiring connecting the logic blocks, and switches for controlling the wiring. The logic block includes a LUT (Look-Up Table) and a flip-flop that is a storage element. The LUT is a rewritable table (often composed of SRAM, etc.) with about n inputs and 1 output (n is often about 3 to 4), and output values for all input value patterns are written. It is possible to express a logic function of n inputs and 1 output. By connecting a plurality of LUTs, a multi-input logical function exceeding n can be expressed. In addition, a sequential circuit can be formed by holding a value using a flip-flop.
[0019]
Next, various expressions and definitions used in the present invention will be described before describing the configuration and operation of the product-product logical expression satisfaction determination apparatus shown in FIG.
[0020]
(1) x _i (X _i , 1), x _i ′ (X _i , 0).
[0021]
(2) Each variable x _i A value indicating the state for determined (x _i ) Is defined. determined (x _i When the value of) is 1, it means that the value of the variable has been determined. The initial value is 0.
[0022]
(3) Each variable x _i For depth (x _i ) Is defined. depth represents the position of the depth of the search tree when the value of the variable is determined. The initial value is 0.
[0023]
(4) Each variable x _i For branch (x _i ) Is defined. A branch value of 1 indicates that the variable value has been determined by the branch procedure. When it is 0, it is determined by the unit procedure. The initial value is 0.
[0024]
(5) Define the global variable current-depth. The initial value is 0.
[0025]
(6) Each clause (x _i , V _i ) + (X _j , V _j ) + (X _k , V _k ), We define the state of the clause from saturated to trinary as follows:
satisfied: determined (x _i ) = 1
And x _i Value is v _i be equivalent to,
Or determined (x _j ) = 1
And x _j Value is v _j be equivalent to,
Or determined (x _k ) = 1
And x _k Value is v _k be equivalent to.
not-satisfied: x _i , X _j , X _k All determined of 1 and any variable value _i , V _j , V _k Is not equal to
unit: x _i , X _j , X _k The value of a variable whose two determined is 1 and the remaining one is 0 and determined is 1 is v _i , V _j , V _k Are not equal.
binary: x _i , X _j , X _k One of the determined is 1 and the remaining two determined are 0 and determined is 1 and the value of the variable is v _i , V _j , V _k Is not equal to
trinary: x _i , X _j , X _k All determined in are zero.
[0026]
(7) When there is a unit clause, among the variables included in the unit clause, variables whose values are not determined are automatically determined so as to satisfy the constraints of the clause. However, multiple unit clauses may try to assign different values to the same variable. In such a case, it is called inconsistent.
[0027]
Next, a configuration of the product-product logical expression satisfaction determination apparatus shown in FIG. 1 will be described.
[0028]
The satisfaction determination device for sum-product type logical expressions shown in FIG. _i ~ X _n Variable storage unit 1 that stores and inputs / outputs the values of unit, united, branched, branch, depth, and current-depth, and the values of each variable of the product-form logical unit, unit, determined, branch, depth, and a state determination unit 3 for determining a state of a logical expression given by current-depth, and a value of each variable, unit, determined, branch, depth provided in the state determination unit 3 and determined by the state determination unit 3 , And the state of the logical expression given by current-depth, determine the state of each clause in any of saturated, not-satisfied, unit, binary, or trinary, and integrate the states of each clause. If the satisfied and unit clauses do not exist and all clauses are not satisfied, branch output is generated.If all clauses are satisfied, satisfied output is generated and not-satisfied clauses are present. And there are unit clauses and they are not inconsistent If there is at least one not-satisfied clause, or if all clauses are satisfied or inconsistent, then there is a comprehensive decision unit 5 that generates a backtrack output. In response to the consistent unit output from the overall judgment unit 5, the value of the variable whose determined is 0 in the unit clause is set to the value specified in the clause, and the determined and branch are set to 1 and 0, respectively. Set depth to current ₋ In response to the branch output from the consistent unit unit 7 to be set to the depth and the comprehensive judgment unit 5, select the variable that is contained most in the binary section, and if the number is the same, select the higher-order variable, Set the variable value, determined, and branch to 0, 1, and 1, respectively, and set depth to current ₋ set depth +1 and current ₋ In response to the backtrack output from the branch unit 9 that increases the depth by 1 and the comprehensive judgment unit 5, ₋ It is determined whether or not depth is 0. If it is 0, the process is terminated. If it is not 0, depth = current for each variable. ₋ If depth and branch = 0, set determined and depth to 0 and depth = current ₋ If depth and branch = 1, set the variable value to 1 and set depth to current ₋ Set depth -1, set branch to 0, and further current ₋ A backtrack unit 11 that reduces the depth to 1 and a satisfaction output unit 13 that outputs that the sum product type logical expression is satisfied in response to the satisfaction output from the comprehensive determination unit 5.
[0029]
Each component part of the product-product-logic-expression-satisfaction determination device shown in FIG. 1 is realized by an FPGA, and each component performs all processes in parallel at the same time, so that a given product-product logic formula can be satisfied. Whether or not it is quickly determined and a satisfactory solution is demanded at high speed.
[0030]
In the variable storage unit 1, the required size varies depending on the number of variables, and therefore the size can be changed according to the number of variables in question by using the FPGA.
[0031]
In the state determination unit 3, the node C ₁ To C _m Corresponds to each clause of a given logical expression. Since the connection between the variable and the clause represents the relationship between the variable and the clause, it is necessary to change for each given logical expression, which is realized by the FPGA. The state of each clause is either saturated, not-satisfied, unit, binary, or trinary, and the overall judgment unit 5 integrates all the states of each clause and how to calculate the value that each variable should take The branch output, the sufficiency output, the consistent unit output, and the backtrack output are output to the branch section 9, the sufficiency output section 13, the consistent unit section 7, and the backtrack section 11, respectively.
[0032]
It should be noted that, by configuring all the components of the product-product logical expression satisfaction determination device shown in FIG. 1 with an FPGA, the processing of each component can be performed in parallel at the same time, thereby speeding up the processing. However, even if not all of the components are configured with FPGA, the portion constituting the given sum-product type logical expression is configured with FPGA, and the other components are configured with ordinary hardware. Even if configured, the processing speed can be similarly increased, or an FPGA and hardware may be combined as appropriate.
[0033]
Next, a procedure for creating the internal logic of the FPGA for constructing the satisfaction determination device of the sum-product-type logical formula configured as described above with the FPGA will be described with reference to the flowchart shown in FIG.
[0034]
In FIG. 3, when a satisfiability problem of a sum product type logical expression is given (step S1), the given sum product type logical expression is analyzed and summed using a HDL (Hardware Description Language) description creation program. A hardware configuration suitable for searching for a satisfying solution of a product logical expression is described in HDL, which is a hardware description language, and output (step S2). The problem is described in HDL (step S3), and a logic synthesis program is used to perform logic synthesis, logic compression, etc. from the described hardware source to create a netlist composed of gates such as AND and OR. (Steps S4 and S5).
[0035]
Using the FPGA mapping program, the netlist created by the logic synthesis program is converted into data suitable for the FPGA structure to create FPGA mapping data (steps S6 and S7), and this FPGA mapping data is converted into the FPGA. By transferring the data upward, it is possible to configure hardware for searching for a satisfying solution of a sum-product logical expression (step S8).
[0036]
By operating the FPGA configured as described above, it is possible to quickly determine whether there is an assignment of a variable that satisfies the sum-form logical expression, and to quickly satisfy the satisfaction solution if it is satisfied. Can be obtained.
[0037]
Next, the operation of the sum-product-formula satisfaction determination device configured as described above will be described with reference to the flowchart shown in FIG.
[0038]
First, the states of all the clauses of a given sum product type logical expression are determined (step S11), and the following determination processes are performed on the determined states of the clauses.
[0039]
[1] Not Satisfied: Check whether there is at least one not-satisfied clause (step S13), and if it exists, proceed to [5] (steps S27, S29).
[0040]
[2] Satisfied: Check whether all clauses are satisfied (step S15). If satisfied, proceed to step S17, where the current value assignment is the solution and the value of the variable whose determined is 0 is don 't care (can be 0 or 1). The solution is output and the process proceeds to [5] (steps S27 and S29).
[0041]
[3] Check whether the Unit: unit clause exists (step S19).
(A) It is checked whether or not those clauses are inconsistent (step S21). If they are not inconsistent, the variable x whose determined is 0 is set for all the clauses. _l The value v specified in the clause _l Set to determined (x _l ) To 1, branch (x _l ) To 0 and depth (x _l ) Is set to current-depth (step S23), and the process returns to [1] (step S11).
(B) If there is an inconsistent clause, proceed to [5] (steps S27 and S29).
[0042]
[4] Branching: In other cases, the variable x included most in the binary clause (both negative and positive) _l Select. If the number is the same, select the higher-order variable and x _l Value of 0, determined (x _l ) To 1, branch (x _l ) To 1 and depth (x _l ) Is set to current-depth + 1, current-depth is incremented by 1 (step S25), and [1] (step S11) is returned.
[0043]
[5] Backtracking:
(A) It is checked whether or not current-depth is 0 (step S27). If it is 0, the algorithm is terminated.
(B) Each variable x _i Against
(B-1) depth (x _i ) = Current ₋ depth and branch (x _i ) = 0, determined (x _i ) To 0, depth (x _i ) To 0,
(B-2) depth (x _i ) = Current ₋ depth and branch (x _i ) = 1, x _i Is set to 1 and depth (x _i ) Current ₋ At depth -1, branch (x _i ) To 0,
(C) current ₋ Decrease depth by 1,
(D) Return to main (step S11) (step S29).
[0044]
Note that the processing shown in FIG. 4 is shown to be performed sequentially as in steps S11, S13, S15, S19, etc., but when this processing is realized by an FPGA, these steps are performed sequentially. Each process is performed in parallel at the same time.
[0045]
Next, the above-described sum-product-formula satisfaction determination method will be described with reference to a specific example showing the transition of value assignment to variables and the like shown in FIG. In FIG. 5, the time advances from the top to the bottom, and () indicates that a value has been set. Moreover, u, b, and s in the condition part indicate unit, binary, and saturated, respectively, and c in the depth part is current. ₋ Indicates depth.
[0046]
In the specific example shown in FIG. _i (I = 1,..., 4) and the clause is C ₁ = (X ₁ + X ₂ ), C ₂ = (X ₁ + X _Three ′), C _Three = (X _Three '+ X _Four ), C _Four = (X _Three + X _Four ′).
[0047]
First, x ₁ Set the value of to 0. At this time, depth (x ₁ ) = 1, determined (x ₁ ) = 1, branch (x ₁ ) = 1. C for clauses ₁ , C ₂ The state becomes unit. Therefore, x ₂ The value of is 1 and x _Three The value of is assumed to be 0. Also, depth (x ₂ ) = Depth (x _Three ) = 1, branch (x ₂ ) = Branch (x _Three ) = 0, determined (x ₂ ) = Determined (x _Three ) = 1. And C _Three And C _Four Becomes unit, but these are inconsistent. current ₋ depth = depth (x ₁ ) = Depth (x ₂ ) = Depth (x _Three ), X ₁ The value of is 1. Also, branch (x ₁ ) = 0, depth (x ₁ ) = 0. And determined (x ₂ ) And determined (x _Three ) Becomes 0. As a result, C ₁ , C ₂ Becomes satisfied. And x _Four Set the value of to 0. Then depth (x _Four ) = 1, branch (x _Four ) = 1. C _Three Becomes unit, so x ₂ Set the value of to 0. At this time, all the clauses are satisfied and become solutions. In this way, each variable and each clause are evaluated and a value is determined.
[0048]
【The invention's effect】
As described above, according to the present invention, it is determined whether a not-satisfied clause exists, whether all clauses are satisfied, whether a unit clause exists, and not-satisfied If no clauses exist and all clauses are satisfied, the assignment of the current value is output as a solution, and if all clauses are not satisfied and a unit clause exists, they are inconsistent If it is not inconsistent, set the value of the variable whose determined is 0 for all those clauses to the value specified in the clause, and set the determined and branch to 1 and 0, respectively. , Depth is current ₋ If it is set to depth and the unit clause does not exist, the variable that is included most in the binary clause is selected, and if it is the same number, the higher-level variable is selected and the value of that variable, determined, and Set branch to 0, 1, 1 and depth to current ₋ set depth +1 and current ₋ If the depth is incremented by 1 and there is at least one not-satisfied clause in the above process, or if all clauses are satisfied or they are not inconsistent, ₋ It is determined whether or not depth is 0. If it is 0, the process is terminated. If it is not 0, depth = current for each variable. ₋ If depth and branch = 0, set determined and depth to 0 and depth = current ₋ If depth and branch = 1, set the value of that variable to 1 and set depth to current ₋ Set depth -1, set branch to 0, and further current ₋ Each process of reducing the depth by 1 is realized by FPGA, each process is performed in parallel and the search area is reduced, and it is judged at high speed whether the sum product type logical expression can be satisfied, and the satisfaction solution Can be obtained in a short time.
[Brief description of the drawings]
FIG. 1 is a block diagram illustrating a configuration of a product-product logical expression satisfaction determination device according to an embodiment of the present invention.
FIG. 2 is a diagram illustrating a configuration of an example of an FPGA.
FIG. 3 is a flowchart showing a procedure for creating the internal logic of the FPGA for configuring the sum-of-product logical expression satisfaction determination device with the FPGA;
4 is a flowchart showing a satisfaction determination method which is an operation of the satisfaction determination device for a sum product type logical expression shown in FIG. 1; FIG.
FIG. 5 is a diagram showing a specific example showing a transition of assignment of values to variables or the like with respect to the satisfaction determination method of the sum product type logical expression shown in FIG. 4;
[Explanation of symbols]
1 Variable storage
3 State determination part
5 comprehensive judgment section
7 Consistent unit
9 Branch
11 Backtrack
13 Satisfaction output part

Claims

A satisfiability determination method for a sum-product formula that determines whether there is an assignment of a variable that satisfies a given sum-product formula,
In the part for each clause of the state determination unit, the value of each variable in the variable storage unit and the state of the variable of determined, branch, and depth are input, and the first state for determining the states of all the clauses of the sum product type logical expression And the steps
When the output of the first step is input to the overall determination unit of the state determination unit, it is determined whether or not a not-satisfied clause exists in the determined state of the clause, and if a not-satisfied clause exists A second step proceeding to a sixth step;
If the output of the first step is input to the general determination unit of the state determination unit, and a not-satisfied clause exists in the second step, the current value assignment is the solution, and the variable whose determined is 0 The value is don't care, the output from the comprehensive determination unit of the state determination unit is input, the solution is output from the sufficiency output unit, and the third step proceeds to the sixth step;
When the output of the first step is input to the general determination unit of the state determination unit and all the clauses are not satisfied in the third step, it is determined whether or not the unit clause is present. If it exists, it is determined whether or not those clauses are inconsistent. If they are inconsistent, the process proceeds to the sixth step. If they are not inconsistent, the comprehensive determination section in the consistent unit section. the output of the input is set to a value determined for all these sections are specified in the section the value of the variable of 0, set the determined and branch, respectively 1 and 0, to set the depth to current_depth A fourth step returning to the first step;
In the overall determination unit of the state determination unit, the output of the first step is input, and in the fourth step, when the unit clause does not exist , the output of the comprehensive determination unit is input to the branch unit and the binary node is the most. Fifth step of selecting the included variable, setting the value of the variable, determined and branch to 0, 1, 1 respectively, setting depth to current_depth + 1, incrementing current_depth by 1, and returning to the first step When,
In the backtrack unit, the output of the comprehensive determination unit is used as an input, and it is determined whether or not current_depth is 0. If it is 0, the process is terminated, and if it is not 0, for each variable, If depth = current_depth and branch = 0, set determined and depth to 0, if depth = current_depth and branch = 1, set the value of the variable to 1 and set depth to current_depth-1 And the branch is set to 0, the current_depth is further reduced by 1, and the sixth step returns to the first step;
A satisfaction determination method for a product-product logical expression, characterized by comprising:

A satisfiability determination method for a sum product logic formula that determines whether there is an assignment of a variable that satisfies a given sum product formula,
In the part for each clause of the state determination unit, the value of each variable in the variable storage unit and the state of the variable of determined, branch, and depth are input, and the first state for determining the states of all the clauses of the sum product type logical expression And the steps
When the output of the first step is input to the general determination unit of the state determination unit, it is determined whether or not a not-satisfied clause exists in the determined state of the clause, and if a not-satisfied clause exists A second step proceeding to a sixth step;
When the output of the first step is input to the overall determination unit of the state determination unit and there are no not-satisfied clauses in the second step, it is determined whether or not all the clauses are satisfied and satisfied If the current value assignment is the solution, the value of the variable whose determined value is 0 is don't care, and the output from the comprehensive determination unit of the state determination unit is input, and the satisfaction output unit A third step of outputting a solution and proceeding to a sixth step;
When the output of the first step is input to the general determination unit of the state determination unit and all the clauses are not satisfied in the third step, it is determined whether or not the unit clause is present. If it exists, it is determined whether or not those clauses are inconsistent. If they are inconsistent, the process proceeds to step 6. If they are not inconsistent, the comprehensive determination unit in the consistent unit unit. For all of those clauses, set the value of the variable whose determined is 0 to the value specified in the clause, set the determined and branch to 1 and 0, respectively, and set the depth to current-depth A fourth step to set and return to the first step;
When the overall determination unit of the state determination unit receives the output of the first step and the unit clause does not exist in the fourth step, the output of the comprehensive determination unit is the input of the branch unit and the binary node is the most. Select a variable that contains a lot, set its value, determined and branch to 0, 1, and 1, respectively, set depth to current-depth +1, increase current-depth by 1, first step A fifth step back to
In the backtrack unit, the output of the comprehensive determination unit is input, and it is determined whether or not current-depth is 0. If it is 0, the process is terminated. If depth = current-depth and branch = 0, then determined and depth are set to 0. If depth = current-depth and branch = 1, the value of the variable is set to 1. setting depth to current-depth -1 and setting branch to 0, further reducing current-depth by 1 and returning to the first step,
A fulfillment determination method for a sum product type logical expression, wherein all the processes in the first to sixth steps are realized by a field programmable gate array (FPGA), and all the processes are performed simultaneously in parallel.

A satisfiability determination device for sum-product-formulas that determines whether there is an assignment of variables that satisfies a given sum-product-formula,
In the part for each clause, the value of each variable in the variable storage unit, the state of the variable of determined, branch, and depth are input, and the value of each variable of the product-form formula, unit, determined, branch, depth, and state determination means for determining the state of a logical expression given by current-depth;
Variable storage means for storing the value of each variable, unit, determined, branch, depth, and current-depth of the sum-form logical expression;
From each variable value determined by the state determination means, unit, determined, branch, depth, and the state of a logical expression given by current-depth, each of which is in any of saturated, not-satisfied, unit, binary, trinary Determines the state of the clauses and merges the state of each clause, resulting in a branch output if there are no not-satisfied and unit clauses and all clauses are not saturated, and all clauses If satisfied, generate a satisfied output, if there is no not-satisfied clause, and if there are unit clauses and they are not inconsistent, generate a consistent unit output, and not-satisfied If there is one clause or if all clauses are in a unit of saturated or inconsistent units, a comprehensive judgment means that generates a backtrack output,
In response to the consistent unit output from the comprehensive judgment means, the value of the variable whose determined is 0 in the unit clause is set to the value specified in the clause, and the determined and branch are set to 1 and 0, respectively. , A consistent unit means for setting depth to current-depth;
In response to the branch output from the comprehensive judgment means, select the variable that is contained most in the binary section, and if the number is the same, select the higher-order variable and set the value of the variable, determined, and branch to 0, Branch means for setting 1 and 1 and setting depth to current-depth +1 and increasing current-depth by 1;
In response to the backtrack output from the comprehensive determination means, it is determined whether or not current-depth is 0. If it is 0, the process is terminated, and if it is not 0, for each variable If depth = current-depth and branch = 0, determined and depth are set to 0. If depth = current-depth and branch = 1, the value of the variable is set to 1, and depth Backtracking means for setting current-depth -1 and branch to 0, and further reducing current-depth to 1;
Satisfaction output means for outputting that the sum product logical expression is satisfied in response to a satisfaction output from the comprehensive judgment means.

A satisfiability determination device for sum-product-formulas that determines whether there is an assignment of variables that satisfies a given sum-product-formula,
In the part for each clause, the value of each variable of the variable storage means, the state of the variable of determined, branch, and depth are input, and the value of each variable of the sum product form, unit, determined, branch, depth, and state determination means for determining the state of a logical expression given by current-depth;
Variable storage means for storing the value of each variable, unit, determined, branch, depth, and current-depth of the sum-form logical expression;
From each variable value determined by the state determination means, unit, determined, branch, depth, and the state of a logical expression given by current-depth, each of which is in any of saturated, not-satisfied, unit, binary, trinary Determines the state of the clauses and merges the state of each clause, resulting in a branch output if there are no not-satisfied and unit clauses and all clauses are not saturated, and all clauses If satisfied, generate a satisfied output, if there is no not-satisfied clause, and if there are unit clauses and they are not inconsistent, generate a consistent unit output, and not-satisfied If there is one clause or if all clauses are in a unit of saturated or inconsistent units, a comprehensive judgment means that generates a backtrack output,
In response to the consistent unit output from the comprehensive judgment means, the value of the variable whose determined is 0 in the unit clause is set to the value specified in the clause, and the determined and branch are set to 1 and 0, respectively. , A consistent unit means for setting depth to current-depth;
In response to the branch output from the comprehensive judgment means, select the variable that is contained most in the binary section, and if the number is the same, select the higher-order variable and set the value of the variable, determined, and branch to 0, Branch means for setting 1 and 1 and setting depth to current-depth +1 and increasing current-depth by 1;
In response to the backtrack output from the comprehensive determination means, it is determined whether or not current-depth is 0. If it is 0, the process is terminated, and if it is not 0, for each variable If depth = current-depth and branch = 0, determined and depth are set to 0. If depth = current-depth and branch = 1, the value of the variable is set to 1, and depth Backtracking means for setting current-depth -1 and branch to 0, and further reducing current-depth to 1;
In response to the satisfaction output from the comprehensive judgment means, the satisfaction output means for outputting that the sum product logical expression is satisfied,
A sum product logical expression satisfaction determination device, wherein each means is realized by a field programmable gate array (FPGA), and all the processes are simultaneously performed in parallel by each means.