(57)【要約】【課題】解の有無の高速判断および、解が得られない原因を高速に原因解析し表示する。【解決手段】ハード制約1に対して緩和リテラルE1を生成する。ハード制約２に対して緩和リテラルE2を生成する。同様にして、各ハード制約に固有の緩和リテラルを割り付ける。CNFエンコーダ１０４は、これらの制約をCNF節にエンコードする。緩和リテラルは、CNF節緩和部１０８にて、CNFに作用する。SATソルバー１０５は、CNFエンコーダ１０４、およびCNF節緩和部１０８が生成した節または仮節を入力として充足解を求める。緩和リテラル最小化部１０６は、上界または下界を更新し、次回求解用に、SATソルバーにCNF節または仮節として入力する。この操作を繰り返した後、緩和リテラル真値数が最小となる最小充足解が得られたら、当該最小充足解に対応する緩和リテラルに対応するハード制約名を、充足しない原因として原因出力部１０７で出力する。【選択図】図９
2019028576.tif 000002
【特許請求の範囲】
【請求項１】
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記ＣＮＦの充足解を得ることによって制約を満たす解を得る方法を、コンピュータに実行させるためのプログラムであって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有の緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に作用させることにより、前記ＣＮＦが充足可能となる充足解を探索する充足解探索手段、
として前記コンピュータを機能させるためのプログラム。
【請求項２】
請求項１に記載したプログラムであって、
前記充足解探索手段による探索の結果として、緩和リテラルの真偽値が得られ、
得られる真偽値に基づいて、緩和リテラルに対応する固有のハード制約名を、充足解が得られない原因として所定の表示部に表示させる表示処理手段、
として前記コンピュータをさらに機能させるためのプログラム。
【請求項３】
請求項２に記載したプログラムであって、
前記緩和リテラルの真値の和がＫ以下となる不等式を前記ＣＮＦにエンコードするエンコード手段、
前記エンコード手段によってエンコードされたＣＮＦに対する複数の充足可能または充足不能の結果を用いて、前記Ｋの充足可能な最小値であるＫ最小値を探索するＫ最小値探索手段、
として前記コンピュータをさらに機能させ、
前記表示処理手段を、前記Ｋ最小値探索手段によって探索されたＫ最小値に対応する固有のハード制約名を、充足解が得られない原因として前記表示部に表示させるように機能させるためのプログラム。
【請求項４】
請求項２に記載したプログラムであって、
前記緩和リテラルを仮節として前記充足解探索手段に入力し、前記充足解探索手段のＵＮＳＡＴコアに基づいて次の求解における仮節を決定することを繰り返し行うことにより、緩和リテラルの真値数が最小となる充足解である最小充足解を探索する最小充足解探索手段、
として前記コンピュータをさらに機能させ、
前記表示処理手段を、前記最小充足解探索手段によって探索された最小充足解に対応する緩和リテラルに対応する固有のハード制約名を、充足解が得られない原因として前記表示部に表示させるように機能させるためのプログラム。
【請求項５】
請求項２に記載したプログラムであって、
前記充足解探索手段による探索の結果として、緩和リテラルの真偽値が得られ、
得られた緩和リテラルの真偽値の否定をＣＮＦ節として追加して前記充足解探索手段を機能させることを繰り返して、充足解が得られない別原因を探索する別原因探索手段として前記コンピュータをさらに機能させ、
前記表示処理手段を、前記別原因探索手段によって探索された別原因を前記表示部に表示させるように機能させるためのプログラム。
【請求項６】
請求項１に記載したプログラムであって、
所定の操作入力部からの制約入力に応じて、前記制約入力を緩和作用がないとする仮節として前記充足解探索手段に入力する入力手段、
前記充足解探索手段を機能させることにより、充足解の有無を前記制約入力の都度判別する充足解有無判別手段、
として前記コンピュータをさらに機能させるためのプログラム。
【請求項７】
請求項６に記載したプログラムであって、
ハード制約を満たさない制約があった場合に、その旨を特定可能な情報を所定の表示部に表示させる表示処理手段、
として前記コンピュータをさらに機能させるためのプログラム。
【請求項８】
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記ＣＮＦの充足解を得ることによって制約を満たす解を得る制約充足問題解決装置であって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有の緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に作用させることにより、前記ＣＮＦが充足可能となる充足解を探索する充足解探索手段、
を備える制約充足問題解決装置。
【請求項９】
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記ＣＮＦの充足解を得ることによって制約を満たす解を得る制約充足問題解決方法であって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有の緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に作用させることにより、前記ＣＮＦが充足可能となる充足解を探索すること、
を含む制約充足問題解決方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、所定の複数の制約条件を充足する制約充足問題において充足解が得られない原因を特定することに寄与する手法等に関する。
【背景技術】
【０００２】
従来より、所定の集団に属するスタッフのスケジュールを最適化するナーススケジューリング問題が一般的に知られている。ナーススケジューリング問題は、制約充足システムでも困難な例として知られている。この種のスケジューリング問題に対する解法として、特許文献１で開示されているように、最適化問題を充足可能性判定問題（SAT）に変換して解く方法が記載されている。また、非特許文献１には、SATソルバーから出力されるUNSATコアを利用して最適化問題を解く方法が記載されている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特許第５８０７９７８号
【特許文献２】特開２００６−００４１５６号公報
【特許文献３】特開平０７−０３６６９７号公報
【非特許文献】
【０００４】
【非特許文献１】Morgado A., Dodaro C., Marques-Silva J. (2014) Core-Guided MaxSAT with Soft Cardinality Con-straints. Principles and Practice of Constraint Programming. CP 2014.Lecture Notes in Computer Science
【非特許文献２】システムＬＳＩ設計自動化技術の基礎  ９７−１１０p 培風館
【非特許文献３】C. Sinz, "Towards an Optimal CNF Encoding of Boolean Cardinality Constraints", in International Conference on Principles and Practices of Constraint Programming , 2005
【発明の概要】
【発明が解決しようとする課題】
【０００５】
特許文献１では、充足判定の反復的な手続きにより充足不能な制約を切り分ける方法が示されている。しかし、この方法では、充足不能の可能性がある制約項目数が膨大となり、結局、何が原因で充足できないのかが分からないことがあった。また、特許文献２では、優先順位が存在する制約について、原因を特定する方法が述べられているが、優先順位のないハード制約については、効力を発揮しない。特許文献１〜３のいずれをとっても、ハード制約が充足しない原因を特定する手段を持っていない。
【０００６】
本発明は、かかる事態に鑑み、充足不能となる原因を明示する方法を提供し、速やかに制約の修正を行うことができるようにすることを目的とする。
【課題を解決するための手段】
【０００７】
本発明は、
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記ＣＮＦの充足解を得ることによって制約を満たす解を得る方法を、コンピュータに実行させるためのプログラムであって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有の緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に作用させることにより、前記ＣＮＦが充足可能となる充足解を探索する充足解探索手段、
として前記コンピュータを機能させるためのプログラムである。
【０００８】
また、他の発明として、
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記ＣＮＦの充足解を得ることによって制約を満たす解を得る制約充足問題解決装置であって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有の緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に作用させることにより、前記ＣＮＦが充足可能となる充足解を探索する充足解探索手段、
を備える制約充足問題解決装置を構成してもよい。
【０００９】
さらに、他の発明として、
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記ＣＮＦの充足解を得ることによって制約を満たす解を得る制約充足問題解決方法であって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有の緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に作用させることにより、前記ＣＮＦが充足可能となる充足解を探索すること、
を含む制約充足問題解決方法を構成してもよい。
【発明の効果】
【００１０】
本発明によれば、ハード制約を満たさない場合、すなわち充足不能の場合にも、その原因を明示することが出来、制約の修正を速やかに行えるようにできる。また、本発明の充足速度は極めて速く、従来不可能であった人が制約セルを入力する間に解の存在チェックが可能である。これを用いれば、予定の入力最中に、充足不能の原因となる入力を防止する効果もある。
【図面の簡単な説明】
【００１１】
【図１】従来のシステム構成例のブロック図である。
【図２】制約システムおける行制約記述例である。
【図３】制約システムにおける列制約記述例である。
【図４】制約システムにおける予定制約記述例である。
【図５】制約システムにおける充足解の例である。
【図６】３制約の関係をベン図で表したものである。
【図７】４制約の関係をベン図で表したものである。
【図８】多数の制約と解の有無の関係を積み木で比喩したものである。
【図９】本発明の構成例である。
【図１０】本発明を装置化したときの構成図である
【図１１】ハード制約名と緩和リテラルの関係を示したものである。
【図１２】ハード制約のCNF上の実装例である。
【図１３】本発明を適用したハード制約のCNF上の緩和例である。
【図１４】従来手法によるハード制約のソフト化例である。
【図１５】ハード制約のCNF上の実装例である。
【図１６】本発明を適用したハード制約のCNF上の緩和例である。
【図１７】従来手法によるハード制約のソフト化例である。
【図１８】制約を論理ゲートで表現したときのCNFとそれを従来方法で緩和したときのCNF式である。
【図１９】制約を論理ゲートで表現したときのCNF式とそれを本発明による方法で緩和したときのCNF式である。
【図２０】本発明による解の存在有無を得るためのブロック図である。
【図２１】緩和リテラルの加算器構成である。
【図２２】緩和リテラルの真値数の最小を求めるアルゴリズムである。
【図２３】仮節とUNSATコアを用いた緩和リテラルの真値数の最小を求めるブロック図である。
【図２４】仮節とUNSATコアを用いて緩和リテラルの真値数の最小を求めるアルゴリズムである。
【図２５】別原因を求めるアルゴリズムである。
【図２６】本発明による方法を使い制約の追加をGUIで入力最中に解の有無を出力している例である。
【図２７】従来方式と本発明による追加変数の総和比較である
【図２８】従来システムでの原因表示例である。
【図２９】本発明を適用した原因の表示例である。
【図３０】間違った制約が入力されている例である。
【発明を実施するための形態】
【００１２】
以下、図面を参照して、本発明を適用した好適な実施形態について説明する。なお、本発明を適用可能な実施形態が以下説明する実施形態に限定されるわけでないことは勿論である。
【００１３】
［１．従来システム］
［１．１  システムの説明］
図１は、従来における勤務の解を得るためのシステムの全体ブロック図である。以下このブロック図について説明する。勤務表は、行制約（行ハード制約）、列制約（列ハード制約）、予定制約（予定ハード制約）から成る。図２の行制約は、各スタッフの勤務パターンに関する制約である。図３の列制約は、各日のスタッフ数等の制約が述べられている。図３の予定制約は、予め決まった勤務や、各スタッフの希望勤務シフト等が入力セルをクリックすることによって入力されている。これらの制約をCNF(Conjunctive Normal Form、和積標準形)と呼ばれる形式の論理式にエンコードし（ＣＮＦエンコーダ）、SATソルバーで解を得ることによって制約に基づいた勤務の解を得るものである。図５は、首尾よく充足解が得られた場合の出力である。
【００１４】
［１．２  SATソルバーの仕事］
次に、SAT問題について説明する。ブール変数へ真偽値を割り当てる問題を充足可能性判定問題(boolean SATisfiablity problem、略してSAT)と呼ぶ。充足可能性判定問題とは、与えられた論理関数に対して、その値を１にする（論理関数を充足する）ような入力変数の割り当てが存在するかどうかを判定する問題である。また、充足可能（SAT）とは、制約式が真になる割り当てが存在することを示す。充足不能（UNSAT）とは、充足する制約式が存在しないことをいう。与えられたCNF式に対して、SATまたはUNSATを示すのがSATソルバーの仕事である。
【００１５】
V p ∈ V を変数(variable) とするとき、L i をリテラルと呼ぶ。
L i = { V p , ~ V p }                
すなわち、リテラルは２値変数であり、ブール変数、またはブール変数の否定である。複数のリテラルの論理和をとったものを節（clause) と呼ぶ。
C j = L j1 ∨ L j2 ∨ ... ∨ L jm            
「節が充足する」とは、節のリテラルのうち、少なくとも一個が真になることである．「節が充足しない」とは、その節のリテラルの全てが偽 になることである．CNF 内では、複数の節が論理積で結ばれる。
C 1 ∧ C 2 ∧ ... ∧ C n           
全ての節を充足（SAT) させてリテラルに値（真/偽) を割り当てて返すのがSAT ソルバーの仕事である。SATを返すときは、充足される割り当ても一緒に返す。充足させる割り当てが一つも存在しないときは、SAT ソルバーは、充足不能を示すUNSAT を返す。例えば、(a ∨ b) ∧ ( ~ b) の入力に対してSAT ソルバーは、a = 真, b = 偽を返す。  (a ∨ b) ∧ ( ~ b) ∧ ( ~ a) の入力に対してSAT ソルバーは、充足させる組み合わせは存在しないのでUNSAT を返す。
【００１６】
［１．３  インクリメンタル動作］
図２０を用いてインクリメンタル動作について説明する。ＣＮＦエンコーダ１０４によってエンコードされ、ＣＮＦ節緩和部１０８によって生成されたCNF節（節）２００は、SATソルバー１０５のメソッド、add_clause()で、SATソルバー１０５へ入力される。入力されたCNF節２００は、SATソルバー１０５をリセットさせない限り、SATソルバー１０５内で継続して維持される。一端、求解が終了した後でも、結果がSATならば、新たな節や、一時的な単項節である仮節（Assumption)を追加して続けて求解を行うことができる。これをインクリメンタル動作という。インクリメンタル動作の利点は、求解の都度に、SATソルバー内部の学習節が追加されて、探索スペースが削減され、特に似て非なる入力に対しては、極めて高速に解の導出が可能になる。
【００１７】
［１．４  仮節］
再び図２０を用いて仮節について説明する。一時的な単項節で、仮節２０１が、リテラルの集合としてSATソルバー１０５のメソッドadd_assumption()で、SATソルバー１０５入力される。add_clause()で入力される節２００は、インクリメンタル動作中SATソルバー１０５内部で維持されるので再入力する必要はない。それに対して仮節（Assumption)２０１は、その求解時の真または偽の仮定であって、次回インクリメンタル動作では、全く同じ入力であっても再入力する必要がある。仮定の全てを含めて正しくアサインすることが出来たら、SATソルバー１０５はSATを返す。もしも仮定通りにアサインできない仮節２０１が一つでもあったならばUNSATを返す。
【００１８】
［１．５  UNSATコア］
一般にSATソルバーに入力される節は、恒久的であり取り消すことはできない。しかし、仮節という単項の節を用いると一時的な節として扱うことが出来る。SATソルバーは、仮節の集合に矛盾（Conflict）を発見したときにUNSATを返すとともにUNSATコアも返すことができる。UNSATコアは、仮説の集合のサブセットであり、その中の少なくとも一つに矛盾が含まれることを示している。充足不能となる可能性の全てを仮節で入力しUNSATが得られたとすれば、UNSATコアは、そのような仮定の下では解がない（UNSAT）理由を示しているとも考えられる。
【００１９】
［２．  本発明の要点］
図９が本発明による解を得るためのシステムの構成図である。本発明では、図１１のように、各ハード制約毎にハード制約緩和リテラル（単に「緩和リテラル」とも称する。）を生成する。緩和リテラルは、対応するハード制約を緩和する目的で生成したリテラルであり、本発明の本質的な部分である。符号１００で示すハード制約１は、複数のハード制約のうちの一つのハード制約であり固有の名前で参照される。符号１０１で示す緩和リテラルE１は、それに対応する緩和リテラルである。符号１０２で示すハード制約２は、別なハード制約であり別な固有の名前で参照される。符号１０２で示す緩和リテラルE２は、それに対応する緩和リテラルである。このようにして、複数のハード制約について、固有のハード制約名には、固有のリテラルをそれぞれのハード制約を緩和する目的で生成する。一方、各ハード制約は符号１０４で示すCNFエンコーダでCNFエンコードされてCNF節になる。緩和リテラルは、CNFエンコーダ１０４が生成したCNF節に作用して緩和作用する。CNFエンコーダ１０４が生成したCNF節、および、符号１０８で示すCNF緩和部が生成するCNF節は、SATソルバー１０５に入力される。第一の要点は、CNF節緩和部１０８（図９）で緩和リテラルが複数の対応するCNF節に作用することである。これにより、解の存在有無が高速に判断可能になる。また、その後の原因解析においても高速に原因を解析することが可能になる。第二の要点は、符号１０６で示す緩和リテラル最小化部の働きにより、この緩和リテラル集合の真値数が最小となるようなSAT解を得ることによって、満たしていないハード制約も最小化することである。これにより、解を満たさない原因の提示が可能になる。緩和リテラル集合の真値数が最小となるようなＳＡＴ解が得られたら、当該ＳＡＴ解に対応する緩和リテラルに対応するハード制約名を、充足しない原因として原因出力部１０７で出力すればよい。
以下、この機構について制約充足システムとして複雑な制約関係にあると言われているナーススケジューリング問題を例にとって説明する。
【００２０】
［３.  ナーススケジューリング問題による実施の形態］
［３.１  従来技術］
ナーススケジューリング問題は、スタッフの勤務を最適化する問題である。勤務シフトのエンコード方法について説明する。リテラルWnds は，スタッフn のd 日の勤務シフトがs であるときtrue，それ以外はfalse というリテラルであるとする。あるスタッフのある日の各々のシフトをリテラル(s 1 , s 2 , s 3 , s 4 ) とすると、true = 1,false = 0 として、例えば、次のようにエンコードできる．
日勤：(1, 0, 0, 0) 入り：(0, 1, 0, 0) 明け：(0, 0, 1, 0) 休み：(0, 0, 0, 1)
【００２１】
ここで、行制約で禁止されている勤務シフトパターン、例えば図２のNo.1「入りの後は明け」制約は、入りの次の日は、〜明け（＝明けでない）
(W nd 入り ∧~ W nd+1 明け)     
の禁止になるから
~ W nd 入り ∨ W nd+1 明け      
と1 個の節で制約可能となる。この様子を図１２に示す。図１２は、従来のハード制約に基づく充足解の出力の流れをソフトウェアの制約論理を用いて表した構成図である。
【００２２】
図１４は、公知の技術及び特許第５８０７９７８号の方法で、ハード制約のソフト化を行った構成図である。各CNF節に、１つのCNF節の出力項が必要となっている。
今、スタッフ数３０人、対象日数が４０日とすると、全体での出力数は、３０×４０＝１２００もの出力変数が必要となる。ソフト出力まで含めて考えたときSATソルバーは必ず充足し何がしかの解を得ることが出来る。ただし、今ハード制約のエラーがないと仮定すると、１２００全ての出力変数がfalseになることが要請されることになる。
【００２３】
［３.２  本発明の原理］
図１３は、本発明における充足解の出力の流れをソフトウェアの制約論理を用いて表した構成図である。図２のNo.1「入りの後は明け」というハード制約をＥ１という１個の緩和リテラルＥ１で複数のCNF節に緩和の作用することが特徴である。具体的に説明する。各ORゲートは、CNF節に対応する。今、緩和リテラルＥ１が、trueであるとすると、各入力に係わらず、各CNFは、無条件に成立する。すなわち、入力がどのような状態にあっても各CNF節は、充足することが保証される。言い換えると、緩和リテラルＥ１の存在により、接続されたCNF節は、無常件に成立する。反対に、緩和リテラルＥ１がfalseであるとすると、図１３は、図１２と等値である。すなわち、この状態では、緩和なしに、各CNF項は成立しなければいけないことになる。なお、図では、分かりやすさのために論理ゲート記号で書いてあるが、ハードウェアのゲート論理ではなく、ソフトウェアの制約論理を表している。ハードウェアのゲート論理と異なるのは、出力から入力への伝播も行われることである。制約ソルバー系においては、双方向に作用する。CNF節が成立するためには、どれか一つの入力がtrueであればよい。緩和リテラルＥ１は、複数のCNFに作用するので、一つでも充足しない節があるとすれば、緩和リテラルがtrueになるように作用する。逆に緩和リテラルがfalseとなるためには、関連する全てのCNFで緩和リテラルなしにCNF節が成立するように入力のみで成立しなければならない。このように緩和リテラルＥ１は、対応するハード制約に関して、関係するCNF節の集約化を行う働きを行う。
【００２４】
同様に、図２のNo.５「５日連続勤務禁止について見てみると
勤務 nd = W nd 入り ∨ W nd 明け ∨ W nd 日勤 )
なので
~ ((W nd入り ∨ W nd 明け ∨ W nd 日勤) ∧
(W nd+1 入り ∨ W nd+1 明け ∨ W nd+1 日勤) ∧
(W nd+2 入り ∨ W nd+2 明け ∨ W nd+2 日勤) ∧
(W nd+3 入り ∨ W nd+3 明け ∨ W nd+3 日勤) ∧
(W nd+4 入り ∨ W nd+4 明け ∨ W nd+4 日勤))              
となるが、勤務＝〜休みなので
~ ( ~ W nd 休み ∧ ~ W nd+1 休み ∧ ~ W nd+2 休み ∧ ~ W nd+3 休み ∧ ~ W nd+4 休み         
となる．これは、CNF 上では一個の節にすることができ、
W nd 休み ∨ W nd+1 休み ∨ W nd+2 休み ∨ W nd+3 休み ∨ W nd+4 休み        
となる。この様子を図１５に示した。図１５は、従来のハード制約の実装である。このままでは、充足不能箇所があると解は得られない。そのために、緩和を行って必ず充足解が得られるようにしたのが、本発明である図１６になる。
一つの緩和リテラルが複数のCNF節の緩和を行うのは図１３と同様である。この例では、任意の5日間の間に休みが少なくとも1日あることが要請される。これを一つでも満足できないときは、緩和リテラルがtrueになることがCNF節充足のための条件でありSATソルバーは、そのように作用する。また、緩和リテラルがfalseになるためには、全てのスタッフの全ての日で５日間内に休みが少なくとも1日あることが要請される。
以上見てきたように、各ハード制約は、対応する僅か1個の緩和リテラルの働きにより必ず充足される。図１７は、公知の技術及び特許第５８０７９７８号の方法で、ハード制約のソフト化を行ったものである。各CNF節に、１つのCNF節の出力項が必要となっている。
【００２５】
［３.３  従来方式との本発明との比較］
一般にCNF節数と変数数は、求解速度と相関があるとされており、CNF節数、変数数は少ない程速く求められる傾向にある。一般的なSATソルバーの実装においては、一変数あたり数十バイトのオブジェクト容量が必要とされる。記憶容量の制限、キャッシュヒット率の観点からも変数の個数は少ないほどよい。それ故、本発明の方法は、図１４の公知の方法に比べ求解速度が速くなる。解の有無チェックの速度、その後の原因解析においても、求解速度が速くなる。また、本発明は、原因解析において、緩和リテラルは、ユーザが直接記した制約名と緩和リテラルが一対一で対応する。緩和リテラルと対応CNF節は、一対多対応である。一方、従来方式は、ユーザが直接記した制約名とソフト出力変数とは、一対多対応、ソフト出力変数と対応CNF節は、一対一となる。充足しない節を最小化するのが、従来方式のソフト化という発想であるが、個々のCNF節の非充足は、原因解析においては、必ずしもユーザにとって必要な情報ではない。本発明は、緩和リテラルと対応CNF節は、一対多対応により、個々のCNF節の非充足は集約化され一個のハード制約名に対応することになる。これにより、原因がより分かり易くなり制約の修正も速やかに行える効果がある。
【００２６】
図１８に、各論理ゲートをハード制約と見立てたときのハードCNF式と、そのCNFをソフト化した場合のCNF式を示す。全ての論理式は、AND、OR、NOTで表せるから、この表を使えば、任意のハード制約をソフト化できる。たとえば、ORゲートは、その出力をCとすると３つの節が必要になる。XORゲートでは、４つの節が必要になることが分かる。
【００２７】
図１９は、本発明による方法を一般化し、各論理ゲートについて適用したものをまとめたものである。ハード制約がCNFで表現できるということは論理関数で表現可能であることを意味する。すべての論理関数は、AND,OR,NOTの組み合わせで表現可能であるから、この表を用いれば、CNFで表現された任意のハード制約を緩和リテラルを用いて直接に緩和できる。すなわち、緩和のための補助変数や節の増加なしに緩和することが可能になる。この点において、本発明は図１８の従来方式に比べて優れている。
【００２８】
［３.４  解の有無の判定］
図２０は、本発明を用いた解の有無の高速判定を行うブロック図である。本発明のエッセンスであるCNF節緩和部１０８については、［３．２  本発明の原理］で詳しく説明した。生成されたCNF節は、SATソルバーのメソッド、add_clause()で、節がSATソルバー１０５へ入力される。インクリメンタル動作を利用して、その都度、解の存在有無を高速に判定することができる。緩和リテラルがtrueであると、ハード制約を緩和することになるので、全緩和リテラルがfalse状態、すなわち、緩和なし状態を仮定すればよい。緩和リテラルなしと等値状態にしてSATならば、解は全ハード制約は緩和なしに解が存在することになる。もしUNSATならば、仮定（仮節のリテラルの真偽値）の少なくとも一つに誤りがあったことになる。この仮定動作は、仮節２０１を使って機能させることが出来る。仮節は、節とは違って、次回求解では維持されない。その都度、SATソルバーのメソッド、add_assumption()で入力する必要がある。［３．２］で説明したように、緩和リテラル数は、従来システムと比して十分に小さいのでそのオーバヘッドは小さく、高速に解の有無を判定できるのが、本発明の効果である。さらに具体的な実装方法について説明する。例えば、図４では、スタッフの勤務の希望がGUIのセルで入力される。勤務希望は、月毎に変わるが、その他の制約は、変わらないことが多い。あるいは、UNDOやREDOといった、GUI上の操作で「取り消し」や「やり直し」ということも考慮の必要がある。その際、節として入力してしまうと、それまでの節と矛盾することがあるので、仮節で入力する必要がある。そこで、スタッフの希望については、仮節で入力し、恒久的な制約については節で入力する。例えば、スタッフn,日ｄ、勤務シフトsをその日シフト勤務の希望とすれば、リテラルWndsを仮節として入力すればよい。このようにして、緩和リテラルおよび、GUIからの制約入力２０４を仮節２０１としてSATソルバー１０５に入力する。インクリメンタル動作で追加変更されるCNFは全体に比べればわずかなので、前回までの学習節が効いて求解速度もより高速になる。これにより、人がGUI入力最中に解の有無を知ることができ、解がない入力を回避でき、解がないという事態を予防できる効果もある。なお、UNSATの場合、インクリメンタル動作を維持したまま、原因解析に移ってもよい。
【００２９】
［３．５  普遍的な課題］
CNFによる制約システムの解と原因の関係を考察する。CNFにより記述された制約は、制約の論理積を取ったものの集合である。例えば、３つの制約がある制約では、求める解は、３つの集合のAND部分を意味している。この様子を図６に示す。同様に、4つの集合の場合を図７に示す。制約数が多くなればなるほど解の範囲は狭まりより解を見つけるのが困難になっていく。今日のナーススケジューリング問題は、制約数が数十万を超えることが珍しくない。この様子は、図８のように制約を積み木と見立て、積み重ねていく様子に例えられる。すなわち、制約という積み木をどんどん積み上げて行くと、一つ一つの制約は難しくなくても、すべての制約を満たさないといけないので次第に難しくなっていく。積みすぎて、崩れてしまった状態が解のない状態である。崩れた原因が、最後の積み木にあるのか、それとも、途中の積み木にあるのか、崩れ去った後では、よく分からない。間接の原因の一つは、最後の積み木にあるかもしれないが、途中で不安定な積み木があったとすれば、そちらが主因の可能性も否定できない。このように解がない原因は、複数の制約の相互作用による結果であって、原因の追究は困難を伴うことが理解される。さらに状況を複雑にしているのはハード制約である。
ソフト制約ならば、優先度や重みを附加することで、その制約の重要性を予め与えることにより、より重要な制約について重みをおいて原因を追究することができるが、ハード制約においては、全てを充足することが暗黙の前提になっており、そのような手法は使うことができない。これは、特定の制約充足システムに固有な課題ではなく、ハード制約を持つ全ての制約充足システムの普遍的な課題である。
【００３０】
［３．６  解のない原因の解決方法］
［３.４  解の有無の判定］により、高速に解の有無の判定を終えて解がないことが明らかになったのならば、次にやるべきステップは、解がない原因の提示である。解がない原因は、満たさない制約を最小化することで顕在化できる。CNF節単位でみれば、制約数は、数十万にも及ぶ可能性があるが、これを最小化して提示したとしても、その解は、無数とも言える別解があり、人間が原因として納得するには至らないということは、課題で述べた通りである。単に満たさない制約を最小化するのではなく、ユーザ自身が定義した制約名に対応する制約について、満たさない制約を最小化することで、どの制約が主因となって満たさなかったのかという人間の納得感が得られるようになるのである。それには、固有の制約名について固有の緩和リテラルを設け、緩和リテラルの真値数の最小化を行えばよい。緩和リテラルの真値数の最小化を行うには、特許第５８０７９７８号で開示されているように、図２１の加算和が、Ｋ以下であるという制約を附加しそれに対して充足可能かどうかを見る、という探索操作を複数回行えば可能になる。図２２にこのアルゴリズムを示す。緩和リテラルは、加算器１２０に入力される。加算器はCNF上の1進加算器であり、入力されたビットが整形されてビットS1、S2...Sｋに出力される。CNF上の1進加算器の実装方法は、例えば非特許文献３に記載されている。
個々の緩和リテラルをEiとするとき
ΣEi<=K
を基数制約という。初期の上界Kは、基数制約で制約することなしにSAT解を得ることで得ることができる。すなわちSAT解があるときの緩和リテラルの真値数が上界Kになる。このとき、１進加算器の出力Skはtrue、 Sk+1は、falseになっている。上界Kをデクリメントするには、上界Kに対応するビットSkをfalseにすればよい。すなわち、Sk=falseとしてSATソルバに節として入力する。節として入力するには、SATソルバーのメソッドadd_clauseを使う。add_clauseで入力した節は、次回求解でもSATソルバー内部で保持されているが、デクリメントする限りにおいてこの操作は矛盾しない。Ｋ以下で満足する命題は、K+1以下でも満足するからである。このようにして、SAT解が続く限り、緩和リテラルが真になる数を少なくしていくことができる。この操作をUNSATになるまで続ける。SATからUNSATになる直前のSAT解が緩和リテラルの真値数が最小の解である。
【００３１】
［３．７  最小化の別解法］
真値数が最小の解を求める別解法として、非特許文献１の仮節（Assumption)とUNSATコアを用いる方法もある。図２３にこの様子を示した。一般的な節は、SATソルバーのメソッドadd_clauseで、節毎にSATソルバーに入力される。これに対して、仮節は、単項の集合として、add_assumptionで与えられる。節と仮節が入力し終わるとメソッドsolve()をコールすることで、求解動作をさせることができる。解が見つからないとき、SATソルバーは、メソッドget_conflict()でUNSATコアを返す。解がないということは、UNSATコアで返されるリテラル集合、すなわち、仮節の一部の仮定が間違っていたことを示している。図２４にこの方法を用いた最小値探索のアルゴリズムを示す。初期は、全ての緩和リテラルをfalseとして仮節設定する。この操作は、緩和が全く必要ないと仮定をしていることに相当する。この状態でSAT解があれば、緩和なしで解があることを意味する。UNSATであれば、下界（LB）をインクリメントし、UNSATコアに基づいて、次の仮節集合をおよび節を設定する。インクリメンタル動作を行い続けてUNSATからSATになったとき、緩和リテラルの真値数が最小の解が得られる。
【００３２】
［３．８  別原因の解法］
緩和リテラルが一つに収束したとしても、別原因が存在する可能性がある。図２５は、別原因を列挙するアルゴリズムである。別原因を列挙するには、解として得られた緩和リテラルの真偽値の否定をＣＮＦ節として追加してインクリメンタル動作をさせればよい。UNSATになったら、それ以上の原因はないということである。
【００３３】
［３．９  表示・出力］
［３．９．１  解の存在有無の表示・出力］
人間が、求解した結果でまず知りたいのは、解の有無である。解が存在するのならば、解自体を表示すればよい。解の表示は、特許第５８０７９７８号で開示されているように、例えば、リテラルWnds は、スタッフn のd 日の勤務シフトがs であるときtrueとエンコードしたとき、Wndsが真という解がSATソルバーで得られたとするなら、スタッフn のd 日の勤務シフトは sである、として表示すればよい。あるいは、図５のように勤務シフトをラベル化した行列表示にしてもよい。一方、解がない場合、［３.４  解の有無の判定］において、SATソルバーからUNSATが返された場合は、全てのハード制約のうち満たせない制約が少なくとも一つ存在するということである。言い換えれば、ハード制約を満たさない制約があった場合には、「解がありません。」、「ハード制約を満たせません。」「エラーがあります。」等のメッセージを所定の表示装置（表示部）に表示させたり、所定の出力装置（出力部）に出力すればよい。これらのメッセージは、ハード制約を満たさない制約があった場合に、その旨を特定可能な情報に相当する。
【００３４】
［３．９．２  解が存在しない原因の表示・出力］
解が存在しないと判明したのならば、次のステップは、解が存在しない理由の明示である。［３．６  解のない原因の解決方法］、［３．７  最小化の別解法］により、緩和リテラルが真値になる数の最小状態でのSAT解が判明する。SAT解から、原因を表示する操作は、次のようにする。緩和リテラルのうち真になっているものが、緩和なしでは、解が得られない制約である。図１１では、緩和リテラルとハード制約名とのマッピングが定義されているから、この表を逆引きすれば、緩和リテラルが真に対応するハード制約名が分かる。これを原因として所定の表示装置（表示部）に表示させたり、所定の出力装置（出力部）に出力すればよい。
【００３５】
［３．９．３  別原因の表示・出力］
［３．８  別原因の解法］において、図２５のループを周るごとに、別な緩和リテラルが真の組み合わせ(集合)解が得られる。このとき、緩和リテラルが真になっているものが、緩和なしでは、解が得られない制約である。図１１では、緩和リテラルとハード制約名とのマッピングが定義されているから、この表を逆引きすれば、緩和リテラルが真に対応するハード制約名が分かる。これを別原因として所定の表示装置（表示部）に表示させたり、所定の出力装置（出力部）に出力すればよい。
【００３６】
［３．１０  制約充足システム］
本発明は、必ず守るべき制約がCNFで表現されていれば、上述した実施形態に限らず、各種の制約充足システムに適用可能である。すなわち、スケジューリング問題に限らず、例えば、パズル作成問題、配送計画問題、生産計画問題、輸送問題等にも適用することが可能である。
【００３７】
［４．実施例］
図１０は、本発明に係る制約充足問題解決装置１の機能構成の一例を示す図である。この制約充足問題解決装置１は、上記のように、スケジューリング問題に限らず、パズル作成問題、配送計画問題、生産計画問題、輸送問題等の各種の制約充足問題に対する充足解を探索することで、制約充足問題を解決するために用いられる装置である。
【００３８】
制約充足問題解決装置１は、例えば、処理部１０と、操作部２０と、表示部３０と、音出力部４０と、通信部５０と、時計部６０と、記憶部９０とを備えて構成され、各部がバスによって接続されたコンピュータシステムである。
【００３９】
処理部１０は、記憶部９０に記憶されているシステムプログラム等の各種のプログラムに従って、自装置の各部を統括的に制御する制御処理及び処理装置であり、ＣＰＵやＤＳＰ等のプロセッサやＡＳＩＣ等の電気電子素子を有して構成される。処理部１０は、本発明における充足解探索手段、エンコード手段、Ｋ最小値探索手段、最小充足解探索手段、別原因探索手段、入力手段、充足解有無判別手段及び表示処理手段として機能する。
【００４０】
操作部２０は、キーボードやマウス、タッチパネル等を有して構成される操作入力装置である。操作部２０からは、前述したＧＵＩからの制約入力等の各種の情報が入力され、入力された各種の情報を処理部１０に出力する。操作部２０は、本発明における所定の操作入力部の一例である。
【００４１】
表示部３０は、ＬＣＤ等で構成されるディスプレイを有する表示装置であり、処理部１０から出力される表示制御信号に基づいて各種の表示を行う。この表示部３０には、処理部１０が所定の表示処理を行うことで、［３．９  表示］で述べた解の存在有無または解が存在しない原因等の各種の情報が表示される。表示部３０は、本発明における所定の表示部の一例である。
【００４２】
音出力部４０は、スピーカ等で構成される音出力装置であり、処理部１０から出力される音出力制御信号に基づく各種の音出力を行う。
【００４３】
通信部５０は、各種の外部装置との間で通信を行うための通信装置であり、有線ケーブルを用いて有線通信を行うための有線通信モジュールや、各種の無線通信規格に則って無線通信を行うための無線通信モジュール等を有して構成される。
【００４４】
時計部６０は、システムクロックやハードウェアクロック等の時計を有して構成される内部時計であり、計時情報を処理部１０に出力する。
【００４５】
記憶部９０は、ＲＯＭやＥＥＰＲＯＭ、ＲＡＭ等のメモリやハードディスク等の外部記憶装置を有して構成される記憶装置であり、システムプログラムや前述した各種のフローチャートに対応する処理を実行するためのプログラムやデータを記憶する。記憶部９０には、各種のプログラム９０１と各種のデータ９０３とが記憶される。
【００４６】
プログラム９０１には、処理部１０によって読み出され、前述した原理や各種のフローチャートに対応する処理を実行するためのプログラムが含まれる。また、データ９０３には、処理部１０が前述した原理や各種のフローチャートに対応する処理を実行する際に必要な処理用のデータや処理中のデータが含まれる。
【００４７】
なお、ここでは、制約充足問題解決装置１が備える操作部２０から、前述したＧＵＩからの制約入力等の各種の情報が入力されることとして説明した。しかし、必ずしもこのようにしなければならないわけではなく、自装置と通信接続された外部装置が備える操作部を介して、前述したＧＵＩからの制約入力等の各種の情報が制約充足問題解決装置１に入力されるようにしてもよい。つまり、本発明における所定の操作入力部には、制約充足問題解決装置１が備える操作部２０に限らず、制約充足問題解決装置１と通信接続された外部装置が備える操作部も含まれる。
【００４８】
また、ここでは、制約充足問題解決装置１の処理部１０が、［３．９  表示］で述べた解の存在有無または解が存在しない原因等の各種の情報を自装置の表示部３０に表示させる表示処理を行うこととして説明した。しかし、必ずしもこのようにしなければならないわけではなく、処理部１０が、自装置と通信接続された外部装置が備える表示部に、上記の各種の情報を表示させる表示処理を行うようにしてもよい。つまり、本発明における所定の表示部には、制約充足問題解決装置１が備える表示部３０に限らず、制約充足問題解決装置１と通信接続された外部装置が備える表示部も含まれる。
【００４９】
また、処理部１０が、上記の各種の情報を、音出力部４０に音出力させるようにしてもよいし、不図示の外部出力基板や外部出力端子を介して外部出力させるようにしてもよい。
【００５０】
また、本発明に係るプログラムやデータは、制約充足問題解決装置１の記憶部９０に記憶させておいて利用するに限らず、他の各種のコンピュータや装置に記憶させて利用するようにすることも可能である。さらに、本発明に係るプログラムやデータを、光ディスクやフラッシュメモリ等の各種の情報記録媒体に記録させて利用するようにすることも可能である。
【００５１】
［適用例１  解の有無の高速判定］
図２０の実施形態をナース勤務表に適用したのが、図２６である。例えば、公休である勤務ラベル「公」を一つ入力すると、左画面に「エラーはありませんでした。」と表示されている。「公」を連続して入力している間にも解の有無が図２０の実施により判断されて、左画面に「エラーはありませんでした。」と各入力に対応して表示されている。セルをクリックする間の短い時間内に解の有無を高速に判定していることが分かる。解が存在しない場合は、その旨のメッセージが出力され、続いて原因解析に移っている。ナーススケジューリングのような複雑に制約が絡む勤務表作成においては、このようなユーザ入力中に解の有無、解がない場合の原因の表示の実装が永く望まれていたが、本発明により初めて可能になった。また、図２７は、従来方法と本発明との追加変数の個数の比較を示しており、本発明の優位性を示している。
【００５２】
［適用例２  解のない主因の提示］
従来方法による原因の列挙を行ったのが、図２８である。原因として６４０個もの列挙を行っている。従来方法では、ハード制約名だけをピックアップしたとしても多数のハード制約名に渡っているので、どれが主因なのかが分からない。従ってどれを修正すればよいか分からない。同じ問題に対し、本発明による列挙を行ったのが、図２９である。図２９では、SATソルバーのインクリメンタル動作により、徐々に緩和リテラルの真値数を減らしている。最終的に1個の原因「平日日勤者10名以上」を特定している。指摘している制約を見てみると、図３０のように、「平日日勤者10名以上」のところが、13名に設定していることが分かる。つまり、ソルバー側では、平日13人というスタッフを確保しようとしたが確保できなかったので解がなかったということが分かる。「平日日勤者10名以上」という制約名から、本来の意図としては、「10名以上」と入力すべきところ、「13名以上」を入力してしまったミスであると推察できる。本発明によって、明確に主因の提示が可能になったことが確認された。
このように、本発明は、制約開発時の設計ミスに起因する原因発見にも効力を発揮する。
【符号の説明】
【００５３】
１    制約充足問題解決装置
１０  処理部
２０  操作部
３０  表示部
４０  音出力部
５０  通信部
６０  時計部
９０  記憶部
９０１  プログラム
９０３  データ
１００  ハード制約名の例
１０１  １００に対応する緩和リテラル
１０２  ハード制約名の例
１０３  １０２に対応する緩和リテラル
１０４  CNFエンコーダ
１０５  SATソルバー
１０６  緩和リテラル最小化部
１０７  原因出力部
１０８  CNF節緩和部
１２０  緩和リテラルの加算器
１２１  緩和リテラル加算器1進出力のビット１
１２２  緩和リテラル加算器1進出力のビット２
１２３  緩和リテラル加算器1進出力のビットK
２００  CNF節
２０１  仮節（Assumption)集合
２０２  UNSATコア
２０３  下界制約更新部
２０４  GUIからの制約入力
【図１】
2019028576.tif 000003
【図２】
2019028576.tif 000004
【図３】
2019028576.tif 000005
【図４】
2019028576.tif 000006
【図５】
2019028576.tif 000007
【図６】
2019028576.tif 000008
【図７】
2019028576.tif 000009
【図８】
2019028576.tif 000010
【図９】
2019028576.tif 000011
【図１０】
2019028576.tif 000012
【図１１】
2019028576.tif 000013
【図１２】
2019028576.tif 000014
【図１３】
2019028576.tif 000015
【図１４】
2019028576.tif 000016
【図１５】
2019028576.tif 000017
【図１６】
2019028576.tif 000018
【図１７】
2019028576.tif 000019
【図１８】
2019028576.tif 000020
【図１９】
2019028576.tif 000021
【図２０】
2019028576.tif 000022
【図２１】
2019028576.tif 000023
【図２２】
2019028576.tif 000024
【図２３】
2019028576.tif 000025
【図２４】
2019028576.tif 000026
【図２５】
2019028576.tif 000027
【図２６】
2019028576.tif 000028
【図２７】
2019028576.tif 000029
【図２８】
2019028576.tif 000030
【図２９】
2019028576.tif 000031
【図３０】
2019028576.tif 000032
【手続補正書】
【提出日】平成29年12月11日(2017.12.11)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記Ｃ
ＮＦの充足解を得ることによって制約を満たす解を得る方法を、コンピュータに実行させ
るためのプログラムであって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有であり前記ＣＮＦの各入力の状態に係わらず前記ＣＮＦを充足させることを可能とする緩和リテラルを持たせ、前記固有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に入力させることにより、
前記ＣＮＦが充足可能となる充足解を探索する充足解探索手段、
として前記コンピュータを機能させるためのプログラム。
【請求項２】
請求項１に記載したプログラムであって、
前記充足解探索手段による探索の結果として、緩和リテラルの真偽値が得られ、
得られる真偽値に基づいて、緩和リテラルに対応する固有のハード制約名を、充足解が
得られない原因として所定の表示部に表示させる表示処理手段、
として前記コンピュータをさらに機能させるためのプログラム。
【請求項３】
請求項２に記載したプログラムであって、
前記緩和リテラルの真値の和がＫ以下となる不等式を前記ＣＮＦにエンコードするエン
コード手段、
前記エンコード手段によってエンコードされたＣＮＦに対する複数の充足可能または充
足不能の結果を用いて、前記Ｋの充足可能な最小値であるＫ最小値を探索するＫ最小値探
索手段、
として前記コンピュータをさらに機能させ、
前記表示処理手段を、前記Ｋ最小値探索手段によって探索されたＫ最小値に対応する固
有のハード制約名を、充足解が得られない原因として前記表示部に表示させるように機能
させるためのプログラム。
【請求項４】
請求項２に記載したプログラムであって、
前記緩和リテラルを仮節として前記充足解探索手段に入力し、前記充足解探索手段のＵ
ＮＳＡＴコアに基づいて次の求解における仮節を決定することを繰り返し行うことにより
、緩和リテラルの真値数が最小となる充足解である最小充足解を探索する最小充足解探索
手段、
として前記コンピュータをさらに機能させ、
前記表示処理手段を、前記最小充足解探索手段によって探索された最小充足解に対応す
る緩和リテラルに対応する固有のハード制約名を、充足解が得られない原因として前記表
示部に表示させるように機能させるためのプログラム。
【請求項５】
請求項２に記載したプログラムであって、
前記充足解探索手段による探索の結果として、緩和リテラルの真偽値が得られ、
得られた緩和リテラルの真偽値の否定をＣＮＦ節として追加して前記充足解探索手段を
機能させることを繰り返して、充足解が得られない別原因を探索する別原因探索手段とし
て前記コンピュータをさらに機能させ、
前記表示処理手段を、前記別原因探索手段によって探索された別原因を前記表示部に表
示させるように機能させるためのプログラム。
【請求項６】
請求項１に記載したプログラムであって、
所定の操作入力部からの制約入力に応じて、前記制約入力を緩和作用がないとする仮節
として前記充足解探索手段に入力する入力手段、
前記充足解探索手段を機能させることにより、充足解の有無を前記制約入力の都度判別
する充足解有無判別手段、
として前記コンピュータをさらに機能させるためのプログラム。
【請求項７】
請求項６に記載したプログラムであって、
ハード制約を満たさない制約があった場合に、その旨を特定可能な情報を所定の表示部
に表示させる表示処理手段、
として前記コンピュータをさらに機能させるためのプログラム。
【請求項８】
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記Ｃ
ＮＦの充足解を得ることによって制約を満たす解を得る制約充足問題解決装置であって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有であり前記ＣＮＦの各入力の状態に係わらず前記ＣＮＦを充足させることを可能とする緩和リテラルを持たせ、前記固
有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に入力させることにより、
前記ＣＮＦが充足可能となる充足解を探索する充足解探索手段、
を備える制約充足問題解決装置。
【請求項９】
複数の制約条件を充足する制約充足問題において制約をＣＮＦにエンコードし、前記Ｃ
ＮＦの充足解を得ることによって制約を満たす解を得る制約充足問題解決方法であって、
前記制約は、必ず守るべき制約である複数のハード制約を含み、
前記複数のハード制約に固有の制約名に対応する固有であり前記ＣＮＦの各入力の状態に係わらず前記ＣＮＦを充足させることを可能とする緩和リテラルを持たせ、前記固
有の緩和リテラルを前記ハード制約に対応する複数のＣＮＦ節に入力させることにより、
前記ＣＮＦが充足可能となる充足解を探索すること、
を含む制約充足問題解決方法。