cspsat.util module
cspsat のユーティリティー．
以下の定義からなる．
CspsatException例外: 例外を表すクラス．
CspsatTimeout例外: タイムアイト例外を表すクラス．
Boolクラス: 命題変数およびリテラルを表すクラス．
TRUEオブジェクト: 真を表す命題定数．
FALSEオブジェクト: 偽を表す命題定数．
Varクラス: 整数変数を表すクラス．
Wsumクラス: 線形和を表すクラス．
Binaryクラス: ビット列演算を符号化するためのクラス．クラスメソッドを含む．
SeqCounterクラス: 基数制約を符号化するためのクラス．クラスメソッドからなる．
Preprocessorクラス: 制約のSAT符号化の前処理のためのクラス．
注釈
本プログラムは学習用の目的で作成されている． 実用上の問題への適用は想定していない． Copyright (c) 2025-- Naoyuki Tamura Licensed under the MIT License
- exception cspsat.util.CspsatTimeout[ソース]
ベースクラス:
CspsatExceptioncspsatモジュールのタイムアウト例外を表すクラス．
- class cspsat.util.Bool(name=None, positive=True, internal=False)[ソース]
ベースクラス:
object命題変数およびリテラルを表すクラス．
同じ命題変数名と同じ符号を持つBoolオブジェクトは同一とみなされる．
- パラメータ:
name (str, optional) -- 命題変数名の文字列．命題変数名を指定しなければ新たな名前を付けた補助変数を生成する． 変数名が "TRUE" あるいは "FALSE" は命題定数とみなされる． 変数名が "?" から始まる場合，補助変数とみなされる． 変数名に "#", "~", "=", "@" を含んではならない (内部的に利用しているため)．
positive (bool, optional) -- リテラルの符号．Trueなら正リテラル，Falseなら負リテラルである．指定しなければTrue．
internal (bool, optional) -- 内部的に作成することを表すフラグ．指定しなければFalse．
サンプル
>>> p = Bool("p") # 命題変数名が"p"のBoolオブジェクトを返す >>> Bool() # 新たな補助変数を生成して返す ?1 >>> p == Bool("p") True >>> ~p # 負リテラル ~p >>> Bool("p", False) == ~p True >>> p == ~~p True >>> abs(~p) # 符号を除いた命題変数を返す p >>> TRUE # 真の命題定数 TRUE >>> FALSE # 偽の命題定数 FALSE >>> TRUE == ~FALSE True >>> p(1,2) # 命題変数名が"p(1,2)"のBoolオブジェクトを生成する p(1,2) >>> p(1) == p("1") # どちらの命題変数名も"p(1)"になり，同じBoolオブジェクトとみなされる True
- cspsat.util.TRUE = TRUE
真を表す命題定数 (Boolオブジェクト)．
- cspsat.util.FALSE = FALSE
偽を表す命題定数 (Boolオブジェクト)．
- class cspsat.util.Var(name=None)[ソース]
ベースクラス:
object整数変数を表すクラス．
同じ整数変数名を持つVarオブジェクトは同一とみなされる．
- パラメータ:
name (str, optional) -- 整数変数名の文字列．整数変数名を指定しなければ新たな名前を付けた補助変数を生成する． 変数名が "?" から始まる場合，補助変数とみなされる． 変数名に "#", "~", "=", "@" を含んではならない (内部的に利用しているため)．
サンプル
>>> x = Var("x") # 整数変数名が"x"のVarオブジェクトを返す >>> Var() # 新たな補助変数を生成して返す ?1 >>> x(1) == x("1") # どちらの整数変数名も"x(1)"になり，同じVarオブジェクトとみなされる True
- class cspsat.util.Wsum(wsum=None, c=0)[ソース]
ベースクラス:
object線形和を表すクラス．
整数変数(
Var)あるいは命題変数(Bool)の線形和を表す． 線形和 \(a_1 x_1 + a_2 x_2 + \cdots + a_n x_n + c\) は \(\textrm{Wsum}(\{x_1:a_1, x_2:a_2, \ldots, x_n:a_n\}, c)\) として表される．- パラメータ:
wsum (dict, optional) -- 変数をキーとし，値が係数(int)の辞書(dict)． 定数のみ整数変数のみ命題変数のみでもよい．
c (int, optional) -- 定数部分．
- wsum
変数をキーとして，値が係数の辞書(dict)． 係数が0の場合は含まれない．
- Type:
dict
- c
定数部分．
- Type:
int
サンプル
>>> x = Var("x") >>> Wsum() # 0 Wsum({}, 0) >>> Wsum(x) # x Wsum({x: 1}, 0) >>> Wsum(x).mul(3).add(1) # 3*x+1 Wsum({x: 3}, 1)
- variables()[ソース]
この線形和に含まれる整数変数のリストを返す．
- 戻り値:
整数変数(
Var)のリストを返す．
サンプル
>>> x = Var("x") >>> Wsum(x(1)).add(x(2)).variables() dict_keys([x(1), x(2)])
- coef(v)[ソース]
この線形和に含まれる変数vの係数を返す．
サンプル
>>> x = Var("x") >>> Wsum(x).mul(3).coef(x) 3 >>> Wsum(x).mul(3).coef(x(1)) 0
- isConstant()[ソース]
この線形和が定数ならTrueを返す．
- 戻り値:
この線形和が定数ならTrue，そうでないならFalse．
サンプル
>>> x = Var("x") >>> Wsum(x).isConstant() False >>> Wsum(x).sub(x).isConstant() True
- where(v, d)[ソース]
この線形和で変数vの値がdに等しいとした場合の線形和を返す．
- パラメータ:
- 戻り値:
整数変数vがdに等しいとした場合の線形和を返す．整数変数vが含まれなければ，この線形和そのものを返す．
サンプル
>>> x = Var("x") >>> Wsum(x(1)).add(x(2)).where(x(1), 2) Wsum({x(2): 1}, 2) >>> Wsum(x(1)).add(x(2)).where(x(3), 2) Wsum({x(1): 1, x(2): 1}, 0)
- mul(a)[ソース]
この線形和を定数倍した線形和を返す．
- パラメータ:
a (int) -- 定数倍の値．
- 戻り値:
この線形和をa倍した線形和．
サンプル
>>> x = Var("x") >>> Wsum(x).add(1).mul(3) Wsum({x: 3}, 3)
- neg()[ソース]
この線形和をマイナスにした線形和を返す．
- 戻り値:
この線形和をマイナスにした線形和を返す．
サンプル
>>> x = Var("x") >>> Wsum(x).add(1).neg() Wsum({x: -1}, -1)
- add(other)[ソース]
この線形和に他の線形和を加えた線形和を返す．
- パラメータ:
other (Wsum) -- 加える線形和．Wsumオブジェクトでない場合は，いったんWsumオブジェクトに変換したのち加えられる．
- 戻り値:
和の線形和を返す．
サンプル
>>> x = Var("x") >>> Wsum(x).add(1) Wsum({x: 1}, 1) >>> Wsum(x).add(x) Wsum({x: 2}, 0)
- sub(other)[ソース]
この線形和から他の線形和を引いた線形和を返す．
- パラメータ:
other (Wsum) -- 引く線形和．Wsumオブジェクトでない場合は，いったんWsumオブジェクトに変換したのち加えられる．
- 戻り値:
差の線形和を返す．
サンプル
>>> x = Var("x") >>> Wsum(x).sub(1) Wsum({x: 1}, -1) >>> Wsum(x).sub(x) Wsum({}, 0)
- value(model)[ソース]
与えられた値割当てにおけるこの線形和の値を返す．
- パラメータ:
model (dict) -- 変数に対する値が定められた辞書(dict)．
- 戻り値:
線形和の値．
サンプル
>>> x = Var("x") >>> Wsum(x).add(1).value({ x:2 }) 3
- toExpr()[ソース]
この線形和を表す式のデータ(
cspsat.csp参照)を返す．- 戻り値:
線形和を表す式 (list)．
サンプル
>>> x = Var("x") >>> w = Wsum({x(1): 2, x(2): 1}, 3) >>> w.toExpr() ['+', ['*', x(1), 2], ['*', x(2), 1], 3]
- class cspsat.util.Binary[ソース]
ベースクラス:
objectビット列演算を符号化するためのクラス．クラスメソッドを含む．
ビット列は
Boolのリストで，最下位ビットが先頭とする．- bins
bins[i] は i ビット目に対する命題論理式のリストを保持する． その和の最下位ビットが i ビット目を表す． bins[i][j] に現れる命題論理式は以下のいずれかの形をしている (xiはリテラル)．
リテラル (
Bool)["and", x1, x2, ..., xn]
["or", x1, x2, ..., xn]
["xor", x1, x2]
- Type:
list of list
- classmethod eqK(xx, k)[ソース]
ビット列xxについて xx == k を表すCNF式を生成するジェネレータ関数．
- パラメータ:
xx (list) --
Boolのリスト．k (int) -- 比較する整数．
- 列挙:
xx == k を表すCNF式．
- classmethod neK(xx, k)[ソース]
ビット列xxについて xx != k を表すCNF式を生成するジェネレータ関数．
- パラメータ:
xx (list) --
Boolのリスト．k (int) -- 比較する整数．
- 列挙:
xx != k を表すCNF式．
- classmethod geK(xx, k)[ソース]
ビット列xxについて xx >= k を表すCNF式を生成するジェネレータ関数．
- パラメータ:
xx (list) --
Boolのリスト．k (int) -- 比較する整数．
- 列挙:
xx >= k を表すCNF式．
- classmethod gtK(xx, k)[ソース]
ビット列xxについて xx > k を表すCNF式を生成するジェネレータ関数．
- パラメータ:
xx (list) --
Boolのリスト．k (int) -- 比較する整数．
- 列挙:
xx > k を表すCNF式．
- classmethod leK(xx, k)[ソース]
ビット列xxについて xx <= k を表すCNF式を生成するジェネレータ関数．
- パラメータ:
xx (list) --
Boolのリスト．k (int) -- 比較する整数．
- 列挙:
xx <= k を表すCNF式．
- classmethod ltK(xx, k)[ソース]
ビット列xxについて xx < k を表すCNF式を生成するジェネレータ関数．
- パラメータ:
xx (list) --
Boolのリスト．k (int) -- 比較する整数．
- 列挙:
xx < k を表すCNF式．
- add(xx, a=1)[ソース]
このBinaryオブジェクトにビット列xxを加える．
- パラメータ:
xx (list of Bool) -- 加えるビット列 (リテラルのリスト)．
a (int, optional) -- 指定すれば a*xx を加える．
- addPower(xx, n, a=1)[ソース]
このBinaryオブジェクトに xx^n*a を加える．
- パラメータ:
xx (list of Bool) -- ビット列 (リテラルのリスト)．
n (int) -- ベキ乗．
a (int, optional) -- 指定しなければ1．
- class cspsat.util.BinaryEquation(encoder)[ソース]
ベースクラス:
objectビット列演算のためのクラス．
- パラメータ:
encoder (LogEncoder) -- 利用するLogEncoderを指定する．
サンプル
>>> encoder = LogEncoder() >>> b = BinaryEquation(encoder) >>> x = Var("x") >>> encoder.defInt(x, 0, 10) >>> b.addPower(x, 2) >>> b.addNum(-5) >>> cnf = b.cmp0(">=") # x**2 - 5 >= 0 のCNF式
- add(x, a=1)[ソース]
整数変数の定数倍 (x*a)を加える．
- パラメータ:
x (Var) -- 加える整数変数．
a (int,optional) -- 定数倍の値 (指定しなければ1)．
- class cspsat.util.SeqCounter[ソース]
ベースクラス:
object基数制約を符号化するためのクラス．クラスメソッドからなる．
- classmethod eqK(xx, k)[ソース]
基数制約 xx[0] + xx[1] + ... == k を逐次カウンタ法でSAT符号化したCNF式をyieldするジェネレータ関数．
- パラメータ:
xx (list of Bool) -- リテラルのリスト．
k (int) -- 整数．
- 列挙:
CNF式．
- classmethod neK(xx, k)[ソース]
基数制約 xx[0] + xx[1] + ... != k を逐次カウンタ法でSAT符号化したCNF式をyieldするジェネレータ関数．
- パラメータ:
xx (list of Bool) -- 命題変数のリスト．
k (int) -- 整数．
- 列挙:
CNF式．
- classmethod geK(xx, k)[ソース]
基数制約 xx[0] + xx[1] + ... >= k を逐次カウンタ法でSAT符号化したCNF式をyieldするジェネレータ関数．
- パラメータ:
xx (list of Bool) -- 命題変数のリスト．
k (int) -- 整数．
- 列挙:
CNF式．
- classmethod gtK(xx, k)[ソース]
基数制約 xx[0] + xx[1] + ... > k を逐次カウンタ法でSAT符号化したCNF式をyieldするジェネレータ関数．
- パラメータ:
xx (list of Bool) -- 命題変数のリスト．
k (int) -- 整数．
- 列挙:
CNF式．
- class cspsat.util.Preprocessor(encoder, introduceAux=False)[ソース]
ベースクラス:
objectSAT符号化の前処理のためのクラス．
制約を符号化し拡張CNF式を生成する．
拡張CNF (XCNF)の形式は以下の通り．ここで pi はリテラルで，n>=0 である．
[p1, ..., pn] (通常の節)
[p1, ..., pn, C] (Cを含む節)
C は以下のいずれかである．ここで W は線形和を表している式，kは整数定数である．
["_eq0", W] (W == 0 を表す)
["_ne0", W] (W != 0 を表す)
["_le0", W] (W <= 0 を表す)
["leK", [p1, ..., pn], K] (p1+...+pn <= k を表す)
- パラメータ:
encoder (Encoder) -- 使用するEncoder．
introduceAux (bool,optional) -- 真なら符号化時に補助変数を導入する (指定しないなら偽)．
DirectEncoder,OrderEncoderからの利用では真を指定している．
- toWsum(s)[ソース]
制約充足問題の式sを表す線形和を返す．
- パラメータ:
s (list) -- 制約充足問題の式．
- 戻り値:
sを表す線形和．
- 例外:
CspsatException -- 式の構文が間違っている．
- isBC(w)[ソース]
線形和wが基数制約に変換できるかどうかを調べる．
すなわち w のすべての変数のドメインが{0,1}で，係数が-1か1である．
- パラメータ:
w (Wsum) -- 線形和．
- 戻り値:
基数制約に変換できるなら真を返す．