CNFする場合の、cnfの簡単化について
-cnfオプションにより生成されたcnfでは、既に値が確定している変数がファイルの最初に書き込まれている。
p cnf 518374 1386970
6469 0
6472 0
-6473 0
6474 0
以下省略
ここで、例えば 6473以上の変数には興味がない場合に、それら対象のの変数を出力cnfファイルから(意味を変更せずに)取り除かれているとが望ましい。
プリプロセッサの作成は難しくないが、実際にcnfファイルを生成するglueminisat->toDimacs(filename);
で呼ばれる toDimacs 中で処理できると嬉しい。
容易な変更で拡張可能であれば、toDimacsの第2引数に興味のある変数の最大値が入れられた場合にそれより大きい変数でかつ値が確定している変数はcnfから除きたい。