cspsat.functions module

便利な関数群．

cspsat モジュールの便利な関数群をまとめている．

命題論理式の記法 (Pは命題変数．A1, A2, ..., Anは命題論理式)
名称など	命題論理式の記法
真	TRUE
偽	FALSE
命題変数 p	Bool("p")
補リテラル	~P
否定	["not", A1], ["!", A1]
論理積	["and", A1, ..., An], ["&&", A1, ..., An]
論理和	["or", A1, ..., An], ["\|\|", A1, ..., An]
含意	["imp", A1, A2], ["=>", A1, A2]
同値	["equ", A1, A2], ["<=>", A1, A2]
排他的論理和	["xor", A1, ..., An], ["^", A1, ..., An]

注釈

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

cspsat.functions.variables(f)[ソース]

命題論理式に含まれている命題変数の集合を返す．

パラメータ:: f -- 命題論理式．命題論理式の記法については functions 参照．
戻り値:: Bool オブジェクトの集合．

サンプル

>>> p = Bool("p")
>>> variables(["and", p(1), ~p(2), p(2)])
{p(1), p(2)}

cspsat.functions.assignments(vs)[ソース]

与えられた命題変数のリストに対し，可能な値割当てをyieldするジェネレータ関数．各値割当ては，命題変数(Bool オブジェクト)をキーとする辞書(dict)で，値は0か1．

パラメータ:: vs -- 命題変数(Bool オブジェクト)のリスト．
列挙:: 値割当てを表す辞書(dict)．

サンプル

>>> p = Bool("p")
>>> list(assignments([p(1),p(2)]))
[{p(1): 0, p(2): 0}, {p(1): 0, p(2): 1}, {p(1): 1, p(2): 0}, {p(1): 1, p(2): 1}]

cspsat.functions.value(f, a)[ソース]

与えられた命題論理式 f と値割当て a に対し，f の真理値を返す関数．

命題論理式 f はいったん toNF 関数で否定・論理積・論理和のみの式に変換され，その後，真理値を計算する．値割当て中に含まれない命題変数の真理値はNoneになる．否定の引数の式の真理値がNoneの場合，否定の真理値はNoneになる．論理積の引数の真理値に0がある場合，論理積の真理値は0になる．論理積の引数の真理値に0がなくNoneがある場合，論理積の真理値はNoneになる．論理和の引数の真理値に1がある場合，論理和の真理値は1になる．論理和の引数の真理値に1がなくNoneがある場合，論理和の真理値はNoneになる．

パラメータ:

f -- 命題論理式．命題論理式の記法については functions 参照．
a (dict) -- 値割当ての辞書(dict)．キーは Bool オブジェクトで表される命題変数，値は0か1．

戻り値:

f の真理値 (0か1かNone)．

例外:

CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> value(["not",p], {p: 1})
0
>>> value(["not",p], {}) # Noneが返される

cspsat.functions.truthTable(*fs)[ソース]

与えられた命題論理式 f1, f2, ... の真理値表を出力する関数．

パラメータ:: *fs -- 命題論理式 f1, f2, ... の列．命題論理式の記法については functions 参照．
例外:: CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> truthTable(["and",p(1),p(2)], ["or",p(1),p(2)])
| p(1) | p(2) | ['and', p(1), p(2)] | ['or', p(1), p(2)] |
|------|------|---------------------|--------------------|
|   0  |   0  |          0          |          0         |
|   0  |   1  |          0          |          1         |
|   1  |   0  |          0          |          1         |
|   1  |   1  |          1          |          1         |

cspsat.functions.isValid(f)[ソース]

与えられた命題論理式 f が恒真かどうかを判定する関数．

命題論理式 f に対するすべての値割当てで f の真理値が1ならば恒真としてTrueを返す． f に含まれる命題変数の個数を $n$ とすると $2^n$ の時間がかかる．

パラメータ:: f -- 命題論理式．命題論理式の記法については functions 参照．
戻り値:: f が恒真ならTrue．そうでなければFalse．
例外:: CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> isValid(["or",p,~p])
True

cspsat.functions.isSat(f)[ソース]

与えられた命題論理式 f が充足可能かどうかを判定する関数．

命題論理式 f に対するある値割当てで f の真理値が1ならば充足可能としてTrueを返す． f に含まれる命題変数の個数を $n$ とすると $2^n$ の時間がかかる．

パラメータ:: f -- 命題論理式．命題論理式の記法については functions 参照．
戻り値:: f が充足可能ならTrue．そうでなければFalse．
例外:: CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> isSat(["or",p(1),p(2)])
True
>>> isSat(["and",p,~p])
False

cspsat.functions.isEquiv(f1, f2)[ソース]

与えられた命題論理式 f1, f2 が論理的に同値かどうかを判定する関数．

命題論理式 ["equ",f1,f2] が恒真なら f1 と f2 が論理的に同値としてTrueを返す． f1, f2 に含まれる命題変数の個数を $n$ とすると $2^n$ の時間がかかる．

パラメータ:

f1 -- 命題論理式．命題論理式の記法については functions 参照．
f2 -- 命題論理式．

戻り値:

f1 と f2 が論理的に同値ならTrue．そうでなければFalse．

例外:

CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> isEquiv(p, ["and",p,p])
True

cspsat.functions.models(f, num=1)[ソース]

与えられた命題論理式 f の複数のモデルを探索し，それらをyieldするジェネレータ関数．

命題論理式 f のすべての値割当て a に対し，a が f のモデルなら a をyieldする．探索するモデルの最大個数を num で指定できる． f に含まれる命題変数の個数を $n$ とすると $2^n$ の時間がかかる．

パラメータ:

f -- 命題論理式．命題論理式の記法については functions 参照．
num (int) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)．

列挙:

見つかったモデル．キーが Bool オブジェクトで値が0か1の辞書(dict)である．

例外:

CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> for model in models(["or",p(1),p(2)], num=0): print(model)
{p(1): 0, p(2): 1}
{p(1): 1, p(2): 0}
{p(1): 1, p(2): 1}

cspsat.functions.toNF(f)[ソース]

与えられた命題論理式 f を，論理演算子として否定・論理積・論理和だけを含む同値な式に変換する．

含意 $A \Rightarrow B$ は $(\lnot A) \lor B$ に変換する．同値 $A \Leftrightarrow B$ は $((\lnot A) \lor B) \land (A \lor (\lnot B))$ に変換する．排他的論理和 $A \oplus B$ は $(A \lor B) \land ((\lnot A) \lor (\lnot B))$ に変換する．

パラメータ:: f -- 命題論理式．
戻り値:: 論理演算子として否定・論理積・論理和だけを含む命題論理式．
例外:: CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> toNF(["not",["xor",p(1),p(2)]])
['not', ['and', ['or', p(1), p(2)], ['or', ['not', p(1)], ['not', p(2)]]]]

cspsat.functions.toNNF(f, positive=True)[ソース]

与えられた命題論理式 f を否定標準形に変換する．

否定標準形は，リテラル(Bool オブジェクト)および論理積と論理和のみが現れる命題論理式である．いったん f を toNF 関数で否定・論理積・論理和だけを含む式に変換したのち， $\lnot \lnot A$ を $A$ に， $\lnot (A \land B)$ を $(\lnot A) \lor (\lnot B)$ に， $\lnot (A \lor B)$ を $(\lnot A) \land (\lnot B)$ に置き換える操作を再帰的に繰り返している．

パラメータ:

f -- 命題論理式．
positive (bool, optional) -- Falseなら ["not",f] を否定標準形に変換する(デフォルト値はTrue)．

戻り値:

否定標準形の命題論理式．

例外:

CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> toNNF(["not",["xor",p(1),p(2)]])
['or', ['and', ~p(1), ~p(2)], ['and', p(1), p(2)]]

cspsat.functions.toCNF(f, simplify=True, formula=False)[ソース]

与えられた命題論理式 f を論理積標準形(CNF)に変換する．

CNF式は複数の節の論理積であり，各節は複数のリテラルの論理和である．いったん f を toNNF 関数で否定標準形に変換したのち，分配法則を用いて $A \lor (B \land C)$ を $(A \lor B) \land (A \lor C)$ に置き換える操作を再帰的に繰り返している．

simplify=True の場合，以下の方法でCNF式を簡単化する．

節から命題定数 FALSE を削除する
節に命題定数 TRUE が含まれていれば，その節をCNF式から削除する
節にリテラル p と補リテラル ~p が含まれていれば，その節をCNF式から削除する
節中に同じリテラルが重複して現れていれば，1つにまとめる

formula=True を指定すれば，結果が節のリストではなく，命題論理式を返す．

f に含まれる命題変数の個数を $n$ とすると最悪の場合CNF式のサイズは $2^n$ になる (たとえば $(p_1 \land q_1)\lor(p_2 \land q_2)\lor\cdots\lor(p_n \land q_n)$ の場合)．

パラメータ:

f -- 命題論理式．命題論理式の記法については functions 参照．
simplify (bool, optional) -- Falseなら得られたCNF式を簡単化しない(デフォルト値はTrue)．
formula (bool, optional) -- 節のリストでなく，命題論理式を返す．

戻り値:

CNF式．CNF式は節のリストであり，各節はリテラルのリストである．

例外:

CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> toCNF(["not",["xor",p(1),p(2)]])
[[~p(1), p(2)], [p(1), ~p(2)]]
>>> toCNF(["not",["xor",p(1),p(2)]], simplify=False)
[[~p(1), p(1)], [~p(1), p(2)], [~p(2), p(1)], [~p(2), p(2)]]
>>> toCNF(["not",["xor",p(1),p(2)]], formula=True)
['and', ['or', ~p(1), p(2)], ['or', p(1), ~p(2)]]

cspsat.functions.toDNF(f, simplify=True, formula=False)[ソース]

与えられた命題論理式 f を論理和標準形(DNF)に変換する．

DNF式は複数の連言節の論理和であり，各連言節は複数のリテラルの論理積である．いったん ["not",f] を toCNF 関数でCNF式に変換したのち， CNF式中の各リテラルを否定することでDNF式を求めている．

simplify=True の場合，簡単化したDNF式を返す．

formula=True を指定すれば，命題論理式を返す．

f に含まれる命題変数の個数を $n$ とすると最悪の場合DNF式のサイズは $2^n$ になる

パラメータ:

f -- 命題論理式．命題論理式の記法については functions 参照．
simplify (bool, optional) -- Falseなら得られたDNF式を簡単化しない(デフォルト値はTrue)．
formula (bool, optional) -- 連言節のリストでなく，命題論理式を返す．

戻り値:

DNF式．DNF式は連言節のリストであり，各連言節はリテラルのリストである．

例外:

CspsatException -- 論理式の構文エラー．

サンプル

>>> p = Bool("p")
>>> toDNF(["not",["xor",p(1),p(2)]])
[[p(1), p(2)], [~p(1), ~p(2)]]
>>> toDNF(["not",["xor",p(1),p(2)]], formula=True)
['or', ['and', p(1), p(2)], ['and', ~p(1), ~p(2)]]

cspsat.functions.ge1(xx)[ソース]

at-least-one基数制約の節をyieldするジェネレータ関数．

xx = [x1, x2, ..., xn] のとき，節 {x1, x2, ..., xn} をyieldする．

パラメータ:: xx (list) -- リテラル(Bool オブジェクト)リスト．
列挙:: 基数制約を符号化した節．

サンプル

>>> p = Bool("p")
>>> for clause in ge1([p(1), p(2), p(3)]): print(clause)
[p(1), p(2), p(3)]

cspsat.functions.le1(xx)[ソース]

at-most-one基数制約の節をyieldするジェネレータ関数．

xx = [x1, x2, ..., xn] のとき，すべての xi, xj の組合せに対し節 {xi, xj} をyieldする．この方法はペアワイズ法と呼ばれる．一般には Encoder クラスに実装されている逐次カウンタ法のほうが良い．

パラメータ:: xx (list) -- リテラル(Bool オブジェクト)リスト．
列挙:: 基数制約を符号化した節．

サンプル

>>> p = Bool("p")
>>> for clause in le1([p(1), p(2), p(3)]): print(clause)
[~p(1), ~p(2)]
[~p(1), ~p(3)]
[~p(2), ~p(3)]

cspsat.functions.eq1(xx)[ソース]

exact-one基数制約の節をyieldするジェネレータ関数．

ge1 関数，le1 関数を用いて必要な節をyieldする．一般には Encoder クラスに実装されている逐次カウンタ法のほうが良い．

パラメータ:: xx (list) -- リテラル(Bool オブジェクト)リスト．
列挙:: 基数制約を符号化した節．

サンプル

>>> p = Bool("p")
>>> for clause in eq1([p(1), p(2), p(3)]): print(clause)
[p(1), p(2), p(3)]
[~p(1), ~p(2)]
[~p(1), ~p(3)]
[~p(2), ~p(3)]

cspsat.functions.geK(xx, k)[ソース]

at-least-k基数制約の節をyieldするジェネレータ関数．

xx = [x1, x2, ..., xn] のとき，xi から n-k+1 個のリテラルを選択するすべての組合せに対し，選んだリテラルからなる節をyieldする．すなわち n-k+1 個のリテラルがすべて偽になる場合を排除している．この方法はバイノミナル法と呼ばれる．一般には Encoder クラスに実装されている逐次カウンタ法のほうが良い．

パラメータ:

xx (list) -- リテラル(Bool オブジェクト)リスト．
k (int) -- kの値．

列挙:

基数制約を符号化した節．

サンプル

>>> p = Bool("p")
>>> for clause in geK([p(1), p(2), p(3)], 2): print(clause)
[p(1), p(2)]
[p(1), p(3)]
[p(2), p(3)]

cspsat.functions.leK(xx, k)[ソース]

at-most-k基数制約の節をyieldするジェネレータ関数．

xx = [x1, x2, ..., xn] のとき，xi から k+1 個のリテラルを選択するすべての組合せに対し，選んだリテラルの否定からなる節をyieldする．すなわち k+1 個のリテラルがすべて真になる場合を排除している．この方法はバイノミナル法と呼ばれる．一般には Encoder クラスに実装されている逐次カウンタ法のほうが良い．

パラメータ:

xx (list) -- リテラル(Bool オブジェクト)リスト．
k (int) -- kの値．

列挙:

基数制約を符号化した節．

サンプル

>>> p = Bool("p")
>>> for clause in leK([p(1), p(2), p(3)], 2): print(clause)
[~p(1), ~p(2), ~p(3)]

cspsat.functions.eqK(xx, k)[ソース]

exact-k基数制約の節をyieldするジェネレータ関数．

geK 関数，leK 関数を用いて必要な節をyieldする．一般には Encoder クラスに実装されている逐次カウンタ法のほうが良い．

パラメータ:

xx (list) -- リテラル(Bool オブジェクト)リスト．
k (int) -- kの値．

列挙:

基数制約を符号化した節．

サンプル

>>> p = Bool("p")
>>> for clause in eqK([p(1), p(2), p(3)], 2): print(clause)
[p(1), p(2)]
[p(1), p(3)]
[p(2), p(3)]
[~p(1), ~p(2), ~p(3)]

cspsat.functions.statData = None: ソルバー実行の統計データを保存するグローバル変数

cspsat.functions.status(lastOnly=True)[ソース]

SATソルバー (SAT)またはCSPソルバー (Solver)実行の統計データ．

SAT.getStat, Solver.getStat 参照．

戻り値:: ソルバー実行の統計データ．

cspsat.functions.defaultTimeout = 600: タイムアウト秒数のデフォルト値を保存するグローバル変数

cspsat.functions.getTimeout()[ソース]

タイムアウト秒数のデフォルト値を返す．

戻り値:: タイムアウト秒数のデフォルト値．

>>> getTimeout()
600

cspsat.functions.setTimeout(timeout)[ソース]

タイムアウト秒数のデフォルト値を設定する．

パラメータ:: timeout (int) -- タイムアウト秒数．

>>> setTimeout(100)
>>> getTimeout()
100

cspsat.functions.solutionsSAT(cnf, command=None, num=1, positiveOnly=False, includeAux=False, verbose=0, timeout=None, tempdir=None)[ソース]

与えられたCNF式のモデルをSATソルバーで探索しyieldするジェネレータ関数．

SAT.solutions 参照．

パラメータ:

cnf (list of list of Bool) -- CNF式 (節のリスト)．
command (str, optional) -- 利用するSATソルバーのコマンド． SAT のcommand参照．
num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)． SAT.solutions のnum参照．
positiveOnly (bool, optional) -- Trueならモデルに正リテラルのみを含める (デフォルト値はFalse)． SAT のpositveOnly参照．
includeAux (bool, optional) -- Trueならモデルに補助変数を含める (デフォルト値はFalse)． SAT のincludeAux参照．
verbose (int, optional) -- 負なら結果を出力しない．正ならSATソルバーの情報を表示する (デフォルト値は0)． SAT のverobse参照．
timeout (int, optional) -- この関数の実行時間のタイムアウト秒数を指定する (デフォルト値は600秒)． setTimeout でデフォルト値を変更できる．
tempdir (str, optional) -- 一時ファイルのディレクトリ名 (デフォルト値はNone)．

列挙:

CNF式のモデル．命題変数(Bool オブジェクト)をキーとする辞書(dict)で，値は0か1．

サンプル

>>> p = Bool("p")
>>> cnf = [ [p(1), p(2)] ]
>>> for sol in solutionsSAT(cnf, num=0): print(sol)
{p(1): 0, p(2): 1}
{p(1): 1, p(2): 0}
{p(1): 1, p(2): 1}
>>> for sol in solutionsSAT(cnf, num=0): print(f"p(1)={sol[p(1)]}, p(2)={sol[p(2)]}")
p(1)=0, p(2)=1
p(1)=1, p(2)=0
p(1)=1, p(2)=1
>>> for sol in solutionsSAT(cnf, num=0): print((sol, status()))
({p(1): 0, p(2): 1}, {'variables': 2, 'clauses': 1, 'conflicts': 0, 'decisions': 1, 'propagations': 2, 'solving': 0.709282636642456})
({p(1): 1, p(2): 0}, {'variables': 2, 'clauses': 2, 'conflicts': 1, 'decisions': 2, 'propagations': 3, 'solving': 0.30728840827941895})
({p(1): 1, p(2): 1}, {'variables': 2, 'clauses': 3, 'conflicts': 1, 'decisions': 1, 'propagations': 3, 'solving': 0.33997058868408203})

cspsat.functions.solveSAT(cnf, command=None, num=1, positiveOnly=False, includeAux=False, verbose=0, timeout=None, stat=False, tempdir=None)[ソース]

与えられたCNF式のモデルをSATソルバーで探索し出力する．

SAT.solve 参照．

パラメータ:

cnf (list of list of Bool) -- CNF式 (節のリスト)．
command (str, optional) -- 利用するSATソルバーのコマンド． SAT のcommand参照．
num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)． SAT.solve のnum参照．
positiveOnly (bool, optional) -- Trueならモデルに正リテラルのみを含める (デフォルト値はFalse)． SAT のpositveOnly参照．
includeAux (bool, optional) -- Trueならモデルに補助変数を含める (デフォルト値はFalse)． SAT のincludeAux参照．
verbose (int, optional) -- 負なら結果を出力しない．正ならSATソルバーの情報を表示する (デフォルト値は0)． SAT のverobse参照．
timeout (int, optional) -- この関数の実行時間のタイムアウト秒数を指定する (デフォルト値は600秒)． setTimeout でデフォルト値を変更できる．
stat (bool, optional) -- Trueなら統計データも表示する (デフォルト値はFalse)． SAT.getStat 参照．
tempdir (str, optional) -- 一時ファイルのディレクトリ名 (デフォルト値はNone)．

サンプル

>>> p = Bool("p")
>>> cnf = [ [p(1), p(2)] ]
>>> solveSAT(cnf, num=0)
SATISFIABLE
Model 1: {p(1): 0, p(2): 1}
Model 2: {p(1): 1, p(2): 0}
Model 3: {p(1): 1, p(2): 1}
>>> solveSAT(cnf, num=0, stat=True)
SATISFIABLE
Model 1: {p(1): 0, p(2): 1}
Stat: {'variables': 2, 'clauses': 1, 'conflicts': 0, 'decisions': 1, 'propagations': 2, 'solving': 0.30565834045410156}
Model 2: {p(1): 1, p(2): 0}
Stat: {'variables': 2, 'clauses': 2, 'conflicts': 1, 'decisions': 2, 'propagations': 3, 'solving': 0.34708118438720703}
Model 3: {p(1): 1, p(2): 1}
Stat: {'variables': 2, 'clauses': 3, 'conflicts': 1, 'decisions': 1, 'propagations': 3, 'solving': 0.3393073081970215}
Stat: {'variables': 2, 'clauses': 4, 'conflicts': 2, 'decisions': 1, 'propagations': 2, 'solving': 0.303924560546875}

cspsat.functions.solutionsCSP(csp, encoder=None, command=None, num=1, positiveOnly=False, includeAux=False, verbose=0, timeout=None, tempdir=None)[ソース]

与えられたCSP(制約充足問題)をCNF式にSAT符号化し，得られたCNF式の解(モデル)をSATソルバーで探索し， CSPの解(モデル)に変換してyieldするジェネレータ関数．

Solver.solutions 参照．

パラメータ:

csp -- CSP．制約のシーケンス．制約の記法については cspsat.csp 参照．
encoder (Encoder | str, optional) -- 使用するSAT符号化．Encoderのインスタンスならそれを用いる．文字列の場合，"d"から始まるなら DirectEncoder, "l"から始まるなら LogEncoder, それ以外なら OrderEncoder を用いる．
command (str, optional) -- 利用するSATソルバーのコマンド． SAT のcommand参照．
num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)． Solver.solutions のnum参照．
positiveOnly (bool, optional) -- Trueならモデルに正リテラルのみを含める (デフォルト値はFalse)． Solver のpositveOnly参照．
includeAux (bool, optional) -- Trueならモデルに補助変数を含める (デフォルト値はFalse)． Solver のincludeAux参照．
verbose (int, optional) -- 負なら結果を出力しない．正ならSATソルバーの情報を表示する (デフォルト値は0)． Solver のverbose参照．
timeout (int, optional) -- この関数の実行時間のタイムアウト秒数を指定する (デフォルト値は600秒)． setTimeout でデフォルト値を変更できる．
tempdir (str, optional) -- 一時ファイルのディレクトリ名 (デフォルト値はNone)．

列挙:

CSPのモデル．命題変数(Bool オブジェクト)あるいは整数変数(Var オブジェクト)をキーとする辞書(dict)で，値は整数．

サンプル

>>> x = Var("x")
>>> csp = [ ["int",x(1),1,3], ["int",x(2),1,3], [">",x(1),x(2)] ]
>>> for sol in solutionsCSP(csp, num=0): print(sol)
{x(1): 2, x(2): 1}
{x(1): 3, x(2): 1}
{x(1): 3, x(2): 2}

cspsat.functions.solveCSP(csp, encoder=None, command=None, num=1, positiveOnly=False, includeAux=False, verbose=0, timeout=None, stat=False, tempdir=None)[ソース]

与えられたCSP(制約充足問題)をCNF式にSAT符号化し，得られたCNF式の解(モデル)をSATソルバーで探索し， CSPの解(モデル)に変換して出力する．

Solver.solve 参照．

パラメータ:

csp -- CSP．制約のシーケンス．制約の記法については cspsat.csp 参照．
encoder (Encoder | str, optional) -- 使用するSAT符号化．Encoderのインスタンスならそれを用いる．文字列の場合，"d"から始まるなら DirectEncoder, "l"から始まるなら LogEncoder, それ以外なら OrderEncoder を用いる．
command (str, optional) -- 利用するSATソルバーのコマンド． SAT のcommand参照．
num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)． Solver.solutions のnum参照．
positiveOnly (bool, optional) -- Trueならモデルに正リテラルのみを含める (デフォルト値はFalse)． Solver のpositveOnly参照．
includeAux (bool, optional) -- Trueならモデルに補助変数を含める (デフォルト値はFalse)． Solver のincludeAux参照．
verbose (int, optional) -- 負なら結果を出力しない．正ならSATソルバーの情報を表示する (デフォルト値は0)． Solver のverbose参照．
timeout (int, optional) -- この関数の実行時間のタイムアウト秒数を指定する (デフォルト値は600秒)． setTimeout でデフォルト値を変更できる．
stat (bool, optional) -- Trueなら統計データも表示する (デフォルト値はFalse)． Solver.getStat 参照．
tempdir (str, optional) -- 一時ファイルのディレクトリ名 (デフォルト値はNone)．

サンプル

>>> x = Var("x")
>>> csp = [ ["int",x(1),1,3], ["int",x(2),1,3], [">",x(1),x(2)] ]
>>> solveCSP(csp, num=0)
SATISFIABLE
Model 1: {x(1): 2, x(2): 1}
Model 2: {x(1): 3, x(2): 1}
Model 3: {x(1): 3, x(2): 2}
>>> solveCSP(csp, num=0, stat=True) # 順序符号化 (OrderEncoder)
SATISFIABLE
Model 1: {x(1): 2, x(2): 1}
Stat: {'variables': 4, 'clauses': 5, 'conflicts': 0, 'decisions': 2, 'propagations': 4, 'solving': 0.3538937568664551, 'encoding': 0.0009377002716064453}
Model 2: {x(1): 3, x(2): 1}
Stat: {'variables': 4, 'clauses': 6, 'conflicts': 0, 'decisions': 1, 'propagations': 4, 'solving': 0.36089038848876953, 'encoding': 0.0009377002716064453}
Model 3: {x(1): 3, x(2): 2}
Stat: {'variables': 4, 'clauses': 7, 'conflicts': 1, 'decisions': 1, 'propagations': 5, 'solving': 0.39816951751708984, 'encoding': 0.0009377002716064453}
Stat: {'variables': 4, 'clauses': 7, 'conflicts': 1, 'decisions': 1, 'propagations': 5, 'solving': 0.39816951751708984, 'encoding': 0.0009377002716064453}
>>> solveCSP(csp, num=0, stat=True, encoder="direct") # 直接符号化 (DirectEncoder)
SATISFIABLE
Model 1: {x(1): 2, x(2): 1}
Stat: {'variables': 6, 'clauses': 11, 'conflicts': 0, 'decisions': 3, 'propagations': 6, 'solving': 0.40071797370910645, 'encoding': 0.0010752677917480469}
Model 2: {x(1): 3, x(2): 1}
Stat: {'variables': 6, 'clauses': 12, 'conflicts': 0, 'decisions': 2, 'propagations': 6, 'solving': 0.39261484146118164, 'encoding': 0.0010752677917480469}
Model 3: {x(1): 3, x(2): 2}
Stat: {'variables': 6, 'clauses': 13, 'conflicts': 1, 'decisions': 2, 'propagations': 10, 'solving': 0.38961291313171387, 'encoding': 0.0010752677917480469}
Stat: {'variables': 6, 'clauses': 13, 'conflicts': 1, 'decisions': 2, 'propagations': 10, 'solving': 0.38961291313171387, 'encoding': 0.0010752677917480469}

cspsat.functions.saveSAT(cnf, fileName)[ソース]

CNF式をファイルに保存する．

CNF式は節のシーケンス(リストなど)であり，各節はリテラル(Bool オブジェクト)のリストである．節が文字列の場合はコメントとして扱われ，そのままファイルに書き込まれる (文字列の先頭が "#" でない場合は先頭に "# " を追加する)．保存したCNF式はloadSAT関数でロードできる．

パラメータ:

cnf -- CNF式．リテラルのリストのシーケンス．
fileName (str) -- ファイル名．

サンプル

>>> p = Bool("p")
>>> cnf = [ [ p(1), p(2) ]]
>>> saveSAT(cnf, "/tmp/foo.sat")
>>> cnf = loadSAT("/tmp/foo.sat")
>>> solveSAT(cnf)
SATISFIABLE
Model 1: {p(1): 0, p(2): 1}

cspsat.functions.loadSAT(fileName)[ソース]

ファイルからCNF式を読み込み，各節をyieldするジェネレータ関数．

各行が節を表すが，空行および # から始まる行はコメントとして処理される．各リテラルは1つ以上の空白文字で区切られているとし，負リテラルは ~ から始まるとする．命題変数名には # あるいは ~ から始まらない任意の文字列を使用できる．

パラメータ:: fileName (str) -- ファイル名．
列挙:: 読み込んだCNF式．

cspsat.functions.saveDimacs(cnf, fileName)[ソース]

CNF式をDIMACS CNF形式に変換しファイルに保存する．

パラメータ:

cnf -- CNF式．リテラルのリストのシーケンス．
fileName (str) -- ファイル名．

サンプル

>>> p = Bool("p")
>>> cnf = [ [ p(1), p(2) ], [ ~p(1), ~p(2) ] ]
>>> saveDimacs(cnf, "/tmp/foo.cnf")

cspsat.functions.saveCSP(csp, fileName)[ソース]

CSPをJSON形式でファイルに保存する． Boolオブジェクトは先頭に "$" を付け加えた文字列に変換する． Varオブジェクトは先頭に "@" を付け加えた文字列に変換する．

パラメータ:

cnf -- CSP．
fileName (str) -- ファイル名．

cspsat.functions.loadCSP(fileName)[ソース]

JSON形式でCSPが保存されたファイルからCSPを読み込みyieldするジェネレータ関数．

先頭に "$" がある文字列はBoolオブジェクトに変換する．先頭に "@" がある文字列はVarオブジェクトに変換する．

パラメータ:: fileName (str) -- ファイル名．
列挙:: 読み込んだCSPのデータ．