./ais.py [options] n
n: AISの要素の個数-m: 制約モデルの番号を指定する-m0: Sugarのalldifferentを使用-m1: alldifferentに大野の方法を使用 (未実装)
-t: 自明な解を除去する- 最初および最後の差が1でない解を探す
--bc=: ブール基数制約の符号化方法を指定するsugar: Sugarの式sinz: SinzのSequential Counter法sinz2: SinzのSequential Counter法を改良
-v: Sugarの解の検証
# CSPの作成
./ais.py -m0 10 >/tmp/ais.csp
# Sugarの実行
sugar -vv /tmp/ais.csp >/tmp/ais.log
# 結果の検証
./ais.py -v 10 </tmp/ais.log
- https://oeis.org/A075458
- https://mathworld.wolfram.com/QueenGraph.html
- https://mathworld.wolfram.com/DominationNumber.html
./qdp.py [options] n d
-
n: クイーングラフのサイズ ($n\times n$ ) -
d: クイーンの個数の上限 -
-m: 制約モデルの番号を指定する-
-m0: 補助変数なし -
-m1: 各行，各列，各対角線でのクイーンの有無を表す補助変数を利用 (未実装)
-
-
--bc=: ブール基数制約の符号化方法を指定する-
sugar: Sugarの式 -
sinz: SinzのSequential Counter法 -
sinz2: SinzのSequential Counter法を改良
-
-
-v: Sugarの解の検証
# CSPの作成
./qdp.py -m0 --bc=sinz 8 5 >/tmp/qdp.csp
# Sugarの実行
sugar -vv /tmp/qdp.csp >/tmp/qdp.log
# 結果の検証
./qdp.py -v 8 5 </tmp/qdp.log
./nqueens.py [options] n
-
n: クイーングラフのサイズ ($n\times n$ )，クイーンの個数 ($n$ ) -
-m: 制約モデルの番号を指定する-
-m0: 各行と各列にはexact1制約，各対角線にはatmost1制約を使用 -
-m1: 各対角線に対しクイーンの有無を表す補助ブール変数を導入し，その和がnに等しい制約を追加
-
-
--bc=: ブール基数制約の符号化方法を指定する (sugar,sinz,sinz2) -
-v: Sugarの解の検証
# CSPの作成
./nqueens.py -m0 --bc=sinz 8 >/tmp/nqueens.csp
# Sugarの実行
sugar -vv /tmp/nqueens.csp >/tmp/nqueens.log
# 結果の検証
./nqueens.py -v 8 </tmp/nqueens.log
./qgcp.py [options] n
-
n: クイーングラフのサイズ ($n\times n$ )，色数 ($n$ ) -
-m: 制約モデルの番号を指定する-
-m0: Sugarのalldifferentを使用 -
-m1: alldifferentに大野の方法を使用
-
-
-x: 対称性を除去する (最初の行の色を指定する) -
--bc=: ブール基数制約の符号化方法を指定する (sugar,sinz,sinz2) -
-v: Sugarの解の検証
# CSPの作成
./qgcp.py -m0 --bc=sinz 5 >/tmp/qgcp.csp
# Sugarの実行
sugar -vv /tmp/qgcp.csp >/tmp/qgcp.log
# 結果の検証
./qgcp.py -v 5 </tmp/qgcp.log
./costasarray.py [options] n
n: 要素の個数-m: 制約モデルの番号を指定する-m0: Sugarのalldifferentを使用-m1: alldifferentに大野の方法を使用 (未実装)
--bc=: ブール基数制約の符号化方法を指定する (sugar,sinz,sinz2)-v: Sugarの解の検証
# CSPの作成
./costasarray.py -m0 5 >/tmp/costasarray.csp
# Sugarの実行
sugar -vv /tmp/costasarray.csp >/tmp/costasarray.log
# 結果の検証
./costasarray.py -v 5 </tmp/costasarray.log
以下のようにして動作を確認できる．
$ python -i util.py
>>> new_name()
'_T1'
>>> new_name()
'_T2'
>>> v("x", 1, 2)
'x_1_2'
>>> t("x", 1, 2)
'_x_1_2'
>>> c("+", 1, 2)
'(+ 1 2)'
>>> c("+", 1, c("+", 2, 3, 4))
'(+ 1 (+ 2 3 4))'
>>> atleast_1(["x1","x2","x3"])
; atleast_1 x1 x2 x3
(or (> x1 0) (> x2 0) (> x3 0))
>>> atleast_1([v("x",1),v("x",2),v("x",3)])
; atleast_1 x_1 x_2 x_3
(or (> x_1 0) (> x_2 0) (> x_3 0))
>>> atmost_1([v("x",1),v("x",2),v("x",3)])
; atmost_1 x_1 x_2 x_3
(<= (+ x_1 x_2) 1)
(<= (+ x_1 x_3) 1)
(<= (+ x_2 x_3) 1)
>>> quit()
例えば以下のようにして生成されるCSPの内容を確認する．
./ais.py -m0 -t 5 | less
また，Sugarで実行できるかどうかを確認する．
./ais.py -m0 -t 5 >/tmp/ais.csp
sugar -vv /tmp/ais.csp
./ais.py -m0 -t 5 >/tmp/ais.csp
sugar -vv /tmp/ais.csp >/tmp/ais.log 2>&1
./ais.py -v 5 </tmp/ais.log
2>&1は標準エラー出力を標準出力にリダイレクトするVerify OKと表示されれば正しい解
Sugarの実行結果をコンソールにも表示したい場合は以下のようにする．
./ais.py -m0 -t 5 >/tmp/ais.csp
sugar -vv /tmp/ais.csp 2>&1 | tee /tmp/ais.log
./ais.py -v 5 </tmp/ais.log
./ais.py -m0 -t 20 >/tmp/ais.csp
sugar -vv /tmp/ais.csp >/tmp/ais.log 2>&1 &
バックグラウンド処理が終了するまで待つ
./ais.py -v 20 </tmp/ais.log
&はバックグラウンド処理tail -f /tmp/ais.logで出力を確認できる (C-cで終了)．jobsでバックグラウンド処理が終了したかどうかを確認できる- 処理を中断したければ
kill %1などを実行する
h: ヘルプの表示 (qで終了)q: 終了f: 1画面進む (b: 1画面戻るd: 半画面進むu: 半画面戻る/: 前向き検索?: 後ろ向き検索n: 検索の再実行&: 検索パターンに合致する行だけ表示ma: 現在行をaでマーク (aは他の文字でも良い)'a:aでマークした行に移動 (aは他の文字でも良い)F:tail -fと同様の表示 (C-cで終了)-N: 行番号の表示-S: 行を折りたたまないで表示
topコマンドで予期せず実行中のプログラムがないかを確認する．- あれば
killコマンドで終了させる．
- あれば
/tmp/が溢れないように注意する．/tmp/sugar*の一時ファイルが大量に残っていれば削除する．