cspsat.dpll module

DPLLソルバーのモジュール．

以下のクラスからなる．

• DPLLクラス: 命題変数のクラス

注釈

本プログラムは学習用の目的で作成されている． 実用上の問題への適用は想定していない．

class cspsat.dpll.DPLL(verbose=0, interactive=False)

ベースクラス: object

DPLLソルバーのクラス．

パラメータ:

• verbose (int, optional) -- 正ならDPLLソルバーの情報を表示する (デフォルト値は0)．

• interactive (bool, optional) -- 真なら会話的に実行する (デフォルト値はFalse)．

nVars()

命題変数の個数を返す．

戻り値:

命題変数の個数．

nClauses()

節の個数を返す．

戻り値:

節の個数．

toLit(v, negative=0)

変数番号vに対するリテラル番号を返す．

パラメータ:

• v (int) -- 変数番号．

• negative (int, optional) -- 1なら否定 (デフォールト値は0)．

戻り値:

リテラル番号．

toVar(lit)

リテラルlitに対する変数と符号のタプルを返す．

パラメータ:

lit (int) -- リテラル．

戻り値:

変数と符号のタプル．

value(lit)

リテラルlitの現在の真理値を返す．真理値が割当てられていなければNoneを返す．

パラメータ:

lit (int) -- リテラル．

戻り値:

litの真理値 (割当てられていなければNone)．

newVar(vname=None)

新しい変数を追加する．

パラメータ:

vname (str, optional) -- 変数名 (デフォールト値はNone)．

戻り値:

新しい変数番号．

decisionLevel()

現在の決定レベルを返す．

戻り値:

決定レベル．

enqueue(lit, reason=None)

リテラルlitを伝播用キューに追加する．

リテラルlitの値がすでに1であればTrueを返し，伝播用キューには追加しない． リテラルlitの値がすでに0であればFalseを返し，伝播用キューには追加しない． リテラルlitの値が決まっていなければ伝播用キューには追加し，Trueを返す．

パラメータ:

• lit (int) -- リテラル．

• reason (list, optional) -- 理由の節 (デフォールト値はNone)．

戻り値:

衝突が生じなければTrue，衝突があればFalse．

assume(lit)

リテラルlitを仮に真と決定する．

パラメータ:

lit (int) -- リテラル．

戻り値:

衝突が生じなければTrue，衝突があればFalse．

propagateClause(num, lit)

num番目の節に対しリテラルlitの伝播処理を行う．

パラメータ:

• num (int) -- 節の番号．

• lit (int) -- リテラル．

戻り値:

衝突が生じなければTrue，衝突があればFalse．

propagate()

伝播処理を行う．

戻り値:

衝突が生じなければNone，衝突が生じれば衝突のあった節の番号．

cancel()

1レベルのバックトラック処理を行う．

cancelUntil(level)

決定レベルlevelまでバックトラック処理を行う．

パラメータ:

level (int) -- 決定レベル．

newDecision()

値が未割当ての変数を選択し，それを偽と仮に決定する．

戻り値:

負リテラル．未割当ての変数がなければNone．

backtrack()

バックトラック処理を行う．

最後の決定まで戻り，それが正リテラルの決定の間はさらに前の決定に戻る． 負リテラルの決定なら，正リテラルにして決定する．

getModel()

モデルを返す．

戻り値:

モデル．

search(num=1)

モデルの探索を行い，見つかったモデルをyieldするジェネレータ関数．

パラメータ:

num (int,optional) -- 探索するモデルの個数 (0なら全解を探索)．

列挙:

モデル．

getStat()

実行の統計情報を返す．

戻り値:

統計情報．

solutions(clauses=None, num=1)

与えられた節を追加し，モデルをyieldするジェネレータ関数．

パラメータ:

• clauses (list,optional) -- 追加する節のリスト．

• num (int,optional) -- 探索するモデルの個数 (0なら全解を探索)．

列挙:

モデル．

solve(clauses=None, num=1, stat=False)

与えられた節を追加し，モデルを表示する．

パラメータ:

• clauses (list,optional) -- 追加する節のリスト．

• num (int,optional) -- 探索するモデルの個数 (0なら全解を探索)．

• stat (bool,optional) -- 真なら統計情報も表示する．

info(l, msg)

メッセージを表示する．

表示レベルが self.verbose より大きければ表示しない． self.interactive が真ならユーザ入力を待つ．

パラメータ:

• l (int) -- 表示レベル．

• msg (str) -- メッセージ．

var2repr(v, negative=0)

変数の表記文字列を返す関数．

newVarで変数名が与えられていればそれを使用する．

パラメータ:

• v (int) -- 変数番号．

• negative (int,optional) -- 1なら負リテラル．

戻り値:

変数の表記文字列．

lit2repr(lit)

リテラルの表記文字列を返す関数．

パラメータ:

lit (int) -- リテラル．

戻り値:

リテラルの表記文字列．

clause2repr(clause)

節の表記 (リテラルの表記文字列のリスト)を返す関数．

パラメータ:

clause (list) -- 節．

戻り値:

節の表記．

assigns2repr()

現在の値割当ての表記を返す関数．

戻り値:

値割当ての表記．

decisions2repr()

現在の決定リストの表記を返す関数．

戻り値:

決定リストの表記．

watches2repr()

現在の監視リストの表記を返す関数．

戻り値:

監視リストの表記．

addInternalClause(clause)

内部表現の節 (リテラル番号のリスト)を追加する．

パラメータ:

clause (list) -- 節．

addDimacsClause(dimacsLits)

DIMACS形式の節 (正負の変数番号のリスト)を追加する．

パラメータ:

dimacsLits (list) -- DIMACS形式の節．

toDimacsLit(vname)

変数名がvnameの変数をDIMACS形式のリテラル (正負の変数番号)に変換する．

変数名が `~' から始まれば負リテラルとする．

パラメータ:

vname (str) -- 変数名．

戻り値:

DIMACS形式のリテラル．

toDimacsLits(clause)

変数名のリストをDIMACS形式の節に変換する．

変数名が `~' から始まれば負リテラルとする．

パラメータ:

clause (list) -- 変数名のリスト．

戻り値:

DIMACS形式の節．

addClause(clause)

変数名のリストの形式の節を追加する．

変数名が `~' から始まれば負リテラルとする．

パラメータ:

clause (list) -- 変数名のリスト．

add(*clauses)

節のリスト (変数名のリストの形式)を追加する．

パラメータ:

clauses (list) -- 節のリスト．

load(file=None)

ファイルから節を読込んで追加する．

パラメータ:

file (str) -- ファイル名 (Noneなら標準入力)．