cspsat.sat module

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

以下のクラスからなる．

  • SATクラス: SATソルバーのラッパークラス

注釈

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

class cspsat.sat.SAT(command=None, tempdir=None, cnfFile=None, outFile=None, delete=True, maxClauses=None, limit=None, positiveOnly=False, includeAux=False, verbose=0)[ソース]

ベースクラス: object

SATソルバーのラッパークラス．

実際のモデル探索には，指定された外部のSATソルバーを使用する． SATソルバーとしては，DIMACS CNFを入力形式とし，SAT solver competitionの出力形式にしたがって結果を標準出力に出力するものなら任意のプログラムを利用できる．

パラメータ:

  • command (str, optional) -- 利用するSATソルバーのコマンド．指定しなければ defaultCommand を使用する (デフォルト値はWindows系なら"sat4j.bat"，その他は"./sat4j")．

  • tmpdir (str, optional) -- 一時ファイルのディレクトリ名を指定する．指定しなければシステム設定にしたがう．

  • cnfFile (str, optional) -- DIMACS CNFファイル名を指定する．指定しなければ一時ファイルが作成される．

  • outFile (str, optional) -- SATソルバーの出力ファイル名を指定する．指定しなければ一時ファイルが作成される．

  • delete (bool, optional) -- TrueならSATオブジェクトが削除される際にcnfFile, outFileを削除する (デフォルト値はTrue)．

  • maxClauses (int, optional) -- 節数がこの値を超えたら例外を発生する．指定しなければ defaultMaxClauses を使用する (デフォルト値は10000000)．

  • limit (int, optional) -- 実行時間の制限秒数を指定する．指定しなければ defaultLimit を使用する (デフォルト値は600秒)．

  • positiveOnly (bool, optional) -- Trueならモデルに正リテラルのみを含める (デフォルト値はFalse)．

  • includeAux (bool, optional) -- Trueならモデルに補助変数を含める (デフォルト値はFalse)．

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

variables

変数名のリスト．DIMACS CNFファイル中では，このリスト順に変数番号が付けられている．

Type:

list

nclauses

節の個数．

Type:

int

model

最後にSATソルバーで求めたモデル (負リテラルも含む)．

Type:

dict

stats

SATソルバー実行の統計データ．

Type:

dict

commitPosition

commit 関数で保存されたDIMACS CNFファイルの状態(変数数，節数，ファイルサイズ)．

Type:

dict

buffer

DIMACS CNFファイル書き込み用バッファー．

Type:

bytearray

bufLimit

DIMACS CNFファイル書き込み用バッファーの最大サイズ (65000バイト)．

Type:

int

サンプル

>>> sat = SAT() # "./sat4j" (Windowsなら"sat4j.bat")をSATソルバーとして利用する
>>> p = Bool("p") # 命題変数 p
>>> sat.add([ p(1), p(2) ]) # 節 {p(1),p(2)} の追加
>>> sat.solve(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}
defaultCommand = './sat4j'

デフォルトのSATソルバーコマンド (Windows系なら"sat4j.bat"，その他は"./sat4j")．

サンプル

>>> SAT.defaultCommand
'./sat4j'
>>> SAT.defaultCommand = "bin/kissat" # Linuxの場合
>>> SAT.defaultCommand = "wsl bin/kissat" # WindowsでWSLがインストールされている場合
defaultTempdir = None

一時ファイルのディレクトリ名のデフォルト値．Noneならシステム設定にしたがう．

defaultLimit = 600

実行時間の制限秒数のデフォルト値 (600秒)．

サンプル

>>> SAT.defaultLimit
600
>>> SAT.defaultLimit = 100
defaultMaxClauses = 10000000

最大節数のデフォルト値 (10000000節)．

サンプル

>>> SAT.defaultMaxClauses
10000000
>>> SAT.defaultMaxClauses = 1000000
nVars()[ソース]

命題変数の個数を返す．

戻り値:

命題変数の個数．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([ p(1), p(2) ])
>>> sat.nVars()
2
nClauses()[ソース]

節の個数を返す．

戻り値:

節の個数．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([ p(1), p(2) ])
>>> sat.nClauses()
1
updateDimacsHeader()[ソース]

DIMACS CNFファイルのヘッダー情報を更新する．

add(*clauses)[ソース]

複数の節を追加する．

Boolオブジェクトのリストで表現された節を追加する． 命題定数 TRUE を含む節は追加しない．命題定数 FALSE は節から削除される． 節が文字列の場合は，コメントとみなし何もしない．

パラメータ:

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

例外:

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([p(0)] , [p(1)]) # 2つの節 {p(0)}, {p(1)} を追加する
>>> sat.nClauses()
2
find()[ソース]

モデルを探索する．

指定されたSATソルバーを用いてモデルを探索し，モデルが見つかればそれを返す．見つからなければNoneを返す． モデルは，キーがBoolオブジェクトで値が0か1の辞書(dict)である．

戻り値:

モデル．キーがBoolオブジェクトで値が0か1の辞書(dict)である．モデルが見つからなければNone．

サンプル

>>> p = Bool("p") # 命題変数 p
>>> sat = SAT()
>>> sat.add([p(1)], [~p(2)])
>>> model = sat.find() # モデルを求める
>>> model[p(1)] # 求めたモデルにおける p(1) の値
1
>>> model[p(2)] # 求めたモデルにおける p(2) の値
0
getStat(includeAll=False)[ソース]

このソルバーによる実行の集計データを返す．

なお，実行時間などの単位は秒で，CPU時間ではなく経過時間である．

パラメータ:

includeAll (bool, optional) -- Falseならsatフォールドの値は最後のSATソルバー実行の集計データのみである． TrueならすべてのSATソルバー実行の集計データのリストになる (デフォールトはFalse)．

戻り値:

以下からなる辞書(dict)を返す． * result: 実行結果 (SATISFIABLE, UNSATISFIABLE, TIMEOUT, UNKNOWN, None)．複数回のSATソルバーを呼び出しで一度でもSATISFIABLEなら，この値もSATISFIABLEとなる． * ncalls: SATソルバーを呼び出した回数． * nmodels: SATソルバーでモデルを見つけた回数． * time: 関数の実行時間 (秒)． * 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ソルバー呼び出しの実行時間 (秒)．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([p(1), p(2)])
>>> sat.solve(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}
>>> sat.getStat() # satフィールドの値は，最後のSATソルバー呼び出しのみ
{'result': 'SATISFIABLE', 'ncalls': 4, 'nmodels': 3, 'time': 4.027583360671997, 'solving': 4.026149749755859, 'command': None, 'sat': {'result': 'UNSATISFIABLE', 'variables': 2, 'clauses': 4, 'conflicts': 2, 'decisions': 1, 'propagations': 2, 'solving': 1.0061917304992676}}
>>> sat.getStat(True) # satフィールドの値は，すべてのSATソルバー呼び出しを含む
{'result': 'SATISFIABLE', 'ncalls': 4, 'nmodels': 3, 'time': 4.027583360671997, 'solving': 4.026149749755859, 'command': None, 'sat': [{'result': 'SATISFIABLE', 'variables': 2, 'clauses': 1, 'conflicts': 0, 'decisions': 1, 'propagations': 2, 'solving': 1.0059900283813477}, {'result': 'SATISFIABLE', 'variables': 2, 'clauses': 2, 'conflicts': 1, 'decisions': 2, 'propagations': 3, 'solving': 1.005939245223999}, {'result': 'SATISFIABLE', 'variables': 2, 'clauses': 3, 'conflicts': 1, 'decisions': 1, 'propagations': 3, 'solving': 1.0080287456512451}, {'result': 'UNSATISFIABLE', 'variables': 2, 'clauses': 4, 'conflicts': 2, 'decisions': 1, 'propagations': 2, 'solving': 1.0061917304992676}]}
addBlock()[ソース]

最後に求めたモデルをブロックする節を追加する．

self.model に保存されている最後に求めたモデルを否定する節を作成し追加する． これにより複数解を求めることが可能になる． なお，補助変数の値の違いは無視される．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([ p(1), p(2) ])
>>> sat.find()
{p(1): 0, p(2): 1}
>>> sat.addBlock()
>>> sat.find()
{p(1): 1, p(2): 0}
>>> sat.addBlock()
>>> sat.find()
{p(1): 1, p(2): 1}
>>> sat.addBlock()
>>> sat.find() # Noneが返る
commit()[ソース]

現在のDIMACS CNFファイルの状態を返す．

現在のDIMACS CNFファイルの状態 (変数数，節数，ファイルサイズ)を commitPosition に保存し，それを返す． そのデータを cancel 関数に渡せば，DIMACS CNFファイルをその状態に戻すことができる．

戻り値:

現在のDIMACS CNFファイルの状態 (変数数，節数，ファイルサイズ)．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([ p(1), p(2) ])
>>> sat.commit()
{'variables': 2, 'clauses': 1, 'size': 70}
cancel(commitPosition=None)[ソース]

DIMACS CNFファイルの状態を戻す．

commit が返した状態に，DIMACS CNFファイルの状態を戻す． 現在のDIMACS CNFファイルの状態 (変数数，節数，ファイルサイズ)を commitPosition に保存し，それを返す． そのデータを cancel 関数に渡せば，DIMACS CNFファイルをその状態に戻すことができる．

パラメータ:

commitPosition (dict, optional) -- DIMACS CNFファイルの状態 (変数数，節数，ファイルサイズ)． 指定されていなければ commitPosition に保存されている状態を使用する．

戻り値:

使用したcommitPositionの値．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> sat.add([ p(1), p(2) ])
>>> sat.commit()
{'variables': 2, 'clauses': 1, 'size': 70}
>>> sat.add([ ~p(1), ~p(2) ])
>>> sat.solve(num=0)
SATISFIABLE
Model 1: {p(1): 0, p(2): 1}
Model 2: {p(1): 1, p(2): 0}
>>> sat.cancel()
{'variables': 2, 'clauses': 1, 'size': 70}
>>> sat.solve(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}
solutions(cnf=None, num=1)[ソース]

複数のモデルを探索し，それらをyieldするジェネレータ関数．

指定された上限の個数まで解(モデル)を探索し，解が見つかればそれをyieldする． 各モデルは，キーがBoolオブジェクトで値が0か1の辞書(dict)である．

複数のモデルを探索する場合は， addBlock メソッドを用いて，最後に見つかったモデルを否定する節を追加したのち，SATソルバーを再度起動することで他のモデルを求めている． なお，補助変数の値のみが異なっている場合は同じモデルとみなす．

パラメータ:

  • cnf (list of list of Bool, optional) -- CNF式 (節のリスト)．

  • num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)．

列挙:

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

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> cnf = [ [p(1), p(2)] ]
>>> for sol in sat.solutions(cnf, num=0): print(sol)
{p(1): 0, p(2): 1}
{p(1): 1, p(2): 0}
{p(1): 1, p(2): 1}
solve(cnf=None, num=1, stat=False)[ソース]

複数のモデルを探索し出力する．

solutions 関数で指定された上限の個数まで解(モデル)を探索し，出力する． 出力の最初の行で，SATISFIABLEかUNSATISFIABLEかを表示する．

パラメータ:

  • cnf (list of list of Bool, optional) -- CNF式 (節のリスト)．

  • num (int, optional) -- 探索するモデルの最大個数．0なら全解を探索する (デフォルト値は1)．

  • stat (bool, optional) -- Trueなら統計データも表示する (デフォルト値はFalse)．

サンプル

>>> p = Bool("p")
>>> sat = SAT()
>>> cnf = [ [p(1), p(2)] ]
>>> sat.solve(cnf, num=0, stat=True) # 最後のStatは4つ目のモデルが存在しないことの探索
SATISFIABLE
Model 1: {p(1): 0, p(2): 1}
Stat: {'result': 'SATISFIABLE', 'ncalls': 1, 'nmodels': 1, 'time': 1.0037319660186768, 'solving': 1.0032446384429932, 'sat': {'result': 'SATISFIABLE', 'variables': 2, 'clauses': 1, 'conflicts': 0, 'decisions': 1, 'propagations': 2, 'solving': 1.0032446384429932}}
Model 2: {p(1): 1, p(2): 0}
Stat: {'result': 'SATISFIABLE', 'ncalls': 2, 'nmodels': 2, 'time': 2.0091824531555176, 'solving': 2.008450746536255, 'sat': {'result': 'SATISFIABLE', 'variables': 2, 'clauses': 2, 'conflicts': 1, 'decisions': 2, 'propagations': 3, 'solving': 1.0052061080932617}}
Model 3: {p(1): 1, p(2): 1}
Stat: {'result': 'SATISFIABLE', 'ncalls': 3, 'nmodels': 3, 'time': 3.012281894683838, 'solving': 3.0112452507019043, 'sat': {'result': 'SATISFIABLE', 'variables': 2, 'clauses': 3, 'conflicts': 1, 'decisions': 1, 'propagations': 3, 'solving': 1.0027945041656494}}
Stat: {'result': 'SATISFIABLE', 'ncalls': 4, 'nmodels': 3, 'time': 4.0171895027160645, 'solving': 4.01587438583374, 'sat': {'result': 'UNSATISFIABLE', 'variables': 2, 'clauses': 4, 'conflicts': 2, 'decisions': 1, 'propagations': 2, 'solving': 1.004629135131836}}