cspsat.csp module
制約充足問題(CSP)のSAT符号化のモジュール．
以下のクラスからなる．
Solverクラス: 制約ソルバーのクラス．
Encoderクラス: SAT符号化の基底クラス
DirectEncoderクラス: 直接符号化・支持符号化のクラス
OrderEncoderクラス: 順序符号化のクラス
LogEncoderクラス: 対数符号化のクラス
以下の記法の説明でA1, A2, ..., Anは制約．X1, X2, ..., Xnは式，L1, L2, ..., Lnはリテラルまたはドメインが0,1の整数変数を表す．
名称など |
宣言の記法 |
備考 |
|---|---|---|
整数変数 |
["int", lb, ub] |
|
最小化 |
["minimize", X] |
|
最大化 |
["maximize", X] |
|
コメント |
["comment", ...], ["#", ...] |
名称など |
式の記法 |
備考 |
|---|---|---|
整数定数 |
n |
0, 1, -1, 2, -2などの整数 |
整数変数 |
Var(\(x\)) |
\(x\) は変数名の文字列 |
リテラル |
p, ~p |
pは |
マイナス |
["-", X1] |
|
加算 |
["+", X1, ..., Xn] |
|
減算 |
["-", X1, X2] |
|
定数乗算 |
["*", X1, X2] |
X1またはX2は整数定数 |
定数除算 |
["div", X, n], ["//", X, n] |
nは正の整数定数. |
定数剰余 |
["mod", X, n], ["%", X, n] |
nは正の整数定数. |
絶対値 |
["abs", X] |
|
最小値 |
["min", X1, ..., Xn] |
|
最大値 |
["max", X1, ..., Xn] |
|
if式 |
["if", A, X, Y] |
|
Xのiビット目 |
["bit", X, i] |
iは0以上の整数定数. |
名称など |
制約の記法 |
備考 |
|---|---|---|
真 |
TRUE |
|
偽 |
FALSE |
|
命題変数 |
Bool(\(p\)) |
\(p\) は変数名の文字列 |
負リテラル |
~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] |
|
\(X_1 = X_2\) |
["eq", X1, X2], ["==", X1, X2] |
|
\(X_1 \ne X_2\) |
["ne", X1, X2], ["!=", X1, X2] |
|
\(X_1 \ge X_2\) |
["ge", X1, X2], [">=", X1, X2] |
|
\(X_1 > X_2\) |
["gt", X1, X2], [">", X1, X2] |
|
\(X_1 \le X_2\) |
["le", X1, X2], ["<=", X1, X2] |
|
\(X_1 < X_2\) |
["lt", X1, X2], ["<", X1, X2] |
|
\(\sum L_i = k\) (exact-k制約) |
["eqK", [L1,...,Ln], k] |
kは整数定数 |
\(\sum L_i \ne k\) |
["neK", [L1,...,Ln], k] |
kは整数定数 |
\(\sum L_i \ge k\) (at-least-k制約) |
["geK", [L1,...,Ln], k] |
kは整数定数 |
\(\sum L_i > k\) |
["gtK", [L1,...,Ln], k] |
kは整数定数 |
\(\sum L_i \le k\) (at-most-k制約) |
["leK", [L1,...,Ln], k] |
kは整数定数 |
\(\sum L_i < k\) |
["ltK", [L1,...,Ln], k] |
kは整数定数 |
名称など |
グローバル制約の記法 |
備考 |
|---|---|---|
alldifferent制約 |
["alldifferent", X1, ..., Xn] |
|
辞書順比較 |
["lexCmp", cmp, [X1,...,Xn], [Y1,...,Yn]] |
|
乗算比較 |
["mulCmp", cmp, X, Y, Z] |
|
ベキ乗比較 |
["powCmp", cmp, X, n, Y] |
|
ビット列 |
["bits", [X1,...,Xn], X] |
|
ビット |
["bit", X, i] |
注釈
本プログラムは学習用の目的で作成されている． 実用上の問題への適用は想定していない．
- class cspsat.csp.Solver(encoder=None, sat=None, command=None, positiveOnly=False, includeAux=False, verbose=0)[ソース]
ベースクラス:
object制約ソルバーのクラス．
- パラメータ:
sat (SAT, optional) -- 使用する
SATソルバーオブジェクト．指定しなければcommandで指定したSATソルバーを用いる．command (str, optional) -- 利用するSATソルバーのコマンド．指定しなければ
./sat4jが利用される(Windowsなら.\sat4j.bat)．SATのcommand参照．positiveOnly (bool, optional) -- Trueならモデルに正リテラルのみを含める (デフォールトはFalse)．
SATのpositiveOnly参照．includeAux (bool, optional) -- Trueならモデルに補助変数を含める (デフォールトはFalse)．
SATのincludeAux参照．verbose (int, optional) -- 正なら実行の詳細情報を表示する (デフォールトは0)．
- stats
ソルバー実行の統計データ．
- Type:
dict
- add(*constraints)[ソース]
制約をSAT符号化したCNF式をSATソルバーに追加する．
Encoder.put,Encoder.encode,SAT.addを呼び出す．ただし制約が
["minimize", w]あるいは["maximize", w]の場合は最小化あるいは最大化する線形和を設定する．- パラメータ:
constraints (list) -- 制約のリスト．
- find()[ソース]
SATソルバーに追加されている制約充足問題の解をSATソルバーで求めて制約充足問題の解に変換して返す．
- 戻り値:
見つかった制約充足問題のモデル．モデルが見つからなければNone．
- getStat(includeAll=False)[ソース]
このソルバーによる実行の統計データを返す．
なお，実行時間などの単位は秒で，CPU時間ではなく経過時間である．
- パラメータ:
includeAll (bool, optional) -- Falseならsatフォールドの値は最後のSATソルバー実行の統計データのみである． TrueならすべてのSATソルバー実行の統計データのリストになる (デフォールトはFalse)．
- 戻り値:
以下からなる辞書(dict)を返す．
result: 実行結果 (SATISFIABLE, UNSATISFIABLE, MINIMUM n, MAXIMUM n, TIMEOUT, UNKNOWN, None)．
ncalls: SATソルバーを呼び出した回数．
nmodels: SATソルバーでモデルを見つけた回数．
time: 関数の実行時間 (秒)．
encoding: SAT符号化にかかった時間 (累積値，秒)．
solving: SATソルバーの実行にかかった時間 (累積値，秒)．
command: SATソルバーのコマンド．
sat: SATソルバーの統計データ (includeAllがFalseなら最後の統計データ，Trueならすべての統計データのリスト)．
SATソルバーの統計データ(satフィールド)は，以下からなるdictである．
result: SATソルバーの実行結果 (SATISFIABLE, UNSATISFIABLE, TIMEOUT, UNKNOWN, None)．
variables: CNF式の命題変数の個数．
clauses: CNF式の節の個数．
conflicts: SATソルバー実行での衝突の回数．
decisions: SATソルバー実行での決定の回数．
propagations: SATソルバー実行での伝播の回数．
solving: SATソルバー呼び出しの実行時間 (秒)．
- solutions(csp, num=1)[ソース]
与えられた制約充足問題の複数のモデルを探索し，それらをyieldするジェネレータ関数．
指定された上限の個数までモデルを探索し，モデルが見つかればそれをyieldする． 最小化あるいは最大化する線形和が指定されている場合は，制約最適問題として最適解を二分探索する． ただし，最小化問題の場合，線形和が最適値未満なら常に充足不能，最適値以上なら常に充足可能と仮定している． 同様に，最大化問題の場合，線形和が最適値より大きいなら常に充足不能，最適値以下なら常に充足可能と仮定している． なお，複数のモデルを探索において，補助変数の値のみが異なっている場合は同じモデルとみなされる．
- パラメータ:
csp (list) -- 制約充足問題 (制約のリスト)．
num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォールトは1)．
- 列挙:
見つかったモデル．
- class cspsat.csp.Encoder(functionHooks=None, constraintHooks=None, verbose=0)[ソース]
ベースクラス:
object制約充足問題(CSP)をSAT符号化する抽象基底クラス．
- パラメータ:
functionHooks (optional) -- 式の符号化時に呼び出すフック関数のリスト．指定しなければ
defaultFunctionHooksを使用する．constraintHooks (optional) -- 制約の符号化時に呼び出すフック関数のリスト．指定しなければ
defaultConstraintHooksを使用する．verbose (int, optional) -- 正なら実行の詳細情報を表示する (デフォールトは0)．
- Atrributes:
solver (Solver): このオブジェクトを利用する制約ソルバーのクラス．
- defaultFunctionHooks = [<function defaultFunctionHook>]
式の符号化時に呼び出されるフック関数のリスト．デフォールト値は
defaultFunctionHookのみのリスト．サンプル
>>> Encoder.defaultFunctionHooks [<function defaultFunctionHook at 0x722f0efa0540>] >>> def myFunctionHook(f, encoder): ... match f: ... case ["++", x]: ... f = ["+", x, 1] ... return f ... >>> Encoder.defaultFunctionHooks.append(myFunctionHook)
- defaultConstraintHooks = [<function defaultConstraintHook>]
制約の符号化時に呼び出されるフック関数のリスト．デフォールト値は
defaultConstraintHookのみのリスト．サンプル
>>> Encoder.defaultConstraintHooks >>> def myConstraintHook(c, encoder): ... match c: ... case ["even", x]: ... (lb, ub) = encoder.getBound(x) ... y = Var() ... encoder.put(["int", y, int(lb/2), int(ub/2)]) ... c = ["==", x, ["+", y, y]] ... return c ... >>> Encoder.defaultConstraintHooks.append(myConstraintHook)
- delimEq = '=='
v=k を表す命題変数の区切り文字．
- delimGe = '>='
v>=k を表す命題変数の区切り文字．
- delimBit = '@'
v+lbのkビット目を表す命題変数の区切り文字．
- defInt(v, lb, ub)[ソース]
整数変数をCSPに追加する．節は生成しない．
節は内部的な制約 ["_int", v, lb, ub] で別に生成する．
- パラメータ:
v (Var) -- 整数変数．
lb (int) -- 整数変数の下限値．
ub (int) -- 整数変数の上限値．
- 例外:
CspsatException -- vがVarオブジェクトでない，あるいは下限値が上限値より大きい，あるいはすでにvが宣言されている．
- getBound(s)[ソース]
制約充足問題の式sの下限値と上限値を返す．
- パラメータ:
s (list) -- 制約充足問題の式．
- 戻り値:
sの下限値lbと上限値ubの対 (lb,ub)．
- 例外:
CspsatException -- 式の構文が間違っている．
- varEqK(v, k, a=1)[ソース]
a*v==kを表す命題変数を返す．
DirectEncoder,OrderEncoderで使用．
- encodeInt(v)[ソース]
整数変数をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
v (Var) -- 整数変数．
- 列挙:
CNF式．
- encodeWsumEq0(w)[ソース]
線形和の式 w==0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumNe0(w)[ソース]
線形和の式 w!=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumLe0(w)[ソース]
線形和の式 w<=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encode()[ソース]
追加された制約をSAT符号化した節をyieldするジェネレータ関数．
ただし制約が
["minimize", x]あるいは["maximize", x]の場合は最小化あるいは最大化する線形和を設定する．- 列挙:
SAT符号化した節．
- decode(satModel, includeAux=False)[ソース]
SATのモデルを制約充足問題のモデルに変換する．
- パラメータ:
satModel (dict) -- SATのモデル．
- 戻り値:
制約充足問題のモデル．
- class cspsat.csp.DirectEncoder(functionHooks=None, constraintHooks=None, verbose=0)[ソース]
ベースクラス:
Encoder直接符号化・支持符号化を実装したクラス．
- varToBool(v)[ソース]
Encoder.varToBoolのDirectEncoderでの実装
- encodeWsumEq0(w)[ソース]
線形和の式 w==0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumNe0(w)[ソース]
線形和の式 w!=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumLe0(w)[ソース]
線形和の式 w<=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- class cspsat.csp.OrderEncoder(functionHooks=None, constraintHooks=None, verbose=0)[ソース]
ベースクラス:
Encoder順序符号化を実装したクラス．
- varToBool(v)[ソース]
Encoder.varToBoolのOrderEncoderでの実装
- encodeWsumEq0(w)[ソース]
線形和の式 w==0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumNe0(w)[ソース]
線形和の式 w!=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumLe0(w)[ソース]
線形和の式 w<=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- class cspsat.csp.LogEncoder(functionHooks=None, constraintHooks=None, verbose=0)[ソース]
ベースクラス:
Encoder対数符号化を実装したクラス．
- varEqK(v, k, a=1)[ソース]
a*v==kを表す命題変数を返す．
DirectEncoder,OrderEncoderで使用．
- varToBool(v)[ソース]
Encoder.varToBoolのLogEncoderでの実装
- encodeInt(v)[ソース]
整数変数をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
v (Var) -- 整数変数．
- 列挙:
CNF式．
- encodeWsumEq0(w)[ソース]
線形和の式 w==0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumNe0(w)[ソース]
線形和の式 w!=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．
- encodeWsumLe0(w)[ソース]
線形和の式 w<=0 をSAT符号化したCNF式をyieldするジェネレータ関数．
Encoderの派生クラスで実装する必要がある．
- パラメータ:
w (Wsum) -- 線形和．
- 列挙:
CNF式．