特許
J-GLOBAL ID：200903027101732607
和積形論理式の充足判定方法および装置
発明者：
,
,
出願人/特許権者：
代理人 (1件)：
三好 秀和 (外1名)
公報種別：公開公報
出願番号（国際出願番号）：特願平9-357677
公開番号（公開出願番号）：特開平11-184840
出願日： 1997年12月25日
公開日（公表日）： 1999年07月09日
要約：
【要約】【課題】 和積形論理式の充足判定問題を高速に解析することができる和積形論理式の充足判定方法および装置を提供する。【解決手段】 not-satisfied の節が存在するかの判定、全ての節がsatisfiedであるかの判定、unitの節が存在するかの判定を行い(ステップS13,S15,S19)、not-satisfied の節が存在せず、全ての節がsatisfied である場合は現在の値の割り当てを解として出力し、not-satisfied の節が存在するか、全ての節がsatisfied であるかまたはinconsistentでなく、 current-depth が0である場合は処理を終了し、0でない場合は各変数に対してdepth = current-depthでbranch=0なら、determinedおよびdepth を0に設定し、depth = current-depth かつbranch=1の場合その変数の値を1に設定し、depth を current-depth -1に設定し、branchを0に設定し、 current-depth を1低減する各処理をFPGAで実現し、各処理を同時に並列して行う。
請求項（抜粋）：
所与の和積形論理式を充足する変数の割り当てが存在するかどうかを判定する和積形論理式の充足判定方法であって、前記和積形論理式のすべての節の状態を判定する第1のステップと、この判定した節の状態においてnot-satisfied の節が存在するか否かを判定し、not-satisfied の節が存在する場合には、第6のステップに進む第2のステップと、第2のステップにおいてnot-satisfied の節が存在しない場合には、すべての節がsatisfied であるか否かを判定し、satisfied である場合には、現在の値の割り当てが解であり、determinedが0の変数の値はdon't careであり、前記解を出力して、第6のステップに進む第3のステップと、第3のステップにおいてすべての節がsatisfied でない場合には、unitの節が存在するか否かを判定し、unitの節が存在する場合には、それらの節がinconsistentであるか否かを判定し、inconsistentである場合には、第6のステップに進み、inconsistentでない場合には、それらのすべての節に対してdeterminedが0の変数の値を節で指定される値に設定し、determinedおよびbranchをそれぞれ1および0に設定し、depth を current-depth に設定し、第1のステップに戻る第4のステップと、第4のステップにおいてunitの節が存在しない場合には、binaryの節に最も多く含まれる変数を選択し、同数の場合には、より上位の変数を選択し、その変数の値、determined、およびbranchをそれぞれ0,1,1に設定し、depth を current-depth +1に設定し、 current-depth を1増加し、第1のステップに戻る第5のステップと、current-depth が0であるか否かを判定し、0である場合には、処理を終了し、0でない場合には、各変数に対してdepth = current-depth 、かつbranch=0の場合には、determinedおよびdepth を0に設定し、depth = current-depth 、かつbranch=1の場合には、その変数の値を1に設定し、depth を current-depth -1に設定し、かつbranchを0に設定し、更に current-depth を1低減し、第1のステップに戻る第6のステップとを有することを特徴とする和積形論理式の充足判定方法。
引用特許：
出願人引用 (6件)
全件表示
審査官引用 (3件)
前のページに戻る
