ROOTで、SATソルバを使用して解を得る試みは、失敗しました。原因は
■探索空間が広すぎる
■FIXED litsが、想定していたより得られない
です。SATソルバを廻せば、FIXED Litsが得られれるであろうと、想定していたのが間違いでした。手がかりを与えれば、それに準じたFixedLitsが得られることを期待していたのですが、現実には、ほとんど得られないまま時間だけが過ぎていく状態となりました。
この試みの失敗から言えることは、NSPは、単純がFIXED Litsが得られるような関係ではない、もっと複雑な関係にあるので、Branchを行ってその結果生じる影響をその都度丹念に紐解いていくしかない、ということです。Branchしないと、つまり 「やってみないと」わからない、それがNSPである、ということであると思います。
そこで、方針を
■探索空間を最小にして
■Branch数を最小
にすることに方針転換します。
次は、drat-trimで生成したUNSATコアの出力です。
p cnf は、ヘッダで、最大変数、と節数(32)が出力されています。2行目からは、UNSATコアが指摘している矛盾に関係している節になります。
例えば、18864という変数名は、プラスの符号なので、アサート(true)という意味になっています。同様に、18870という変数名もtrueであることを指示しています。このCNFを見ると二つの変数群グループに大別できます。
一つは、6500近辺の変数群と、18870近辺の変数群です。6500近辺の変数は、スタッフ、Day,シフトに対応した変数になっています。
次は、解析で判明した変数の対応です。
このような解析を行うことによって、バグの原因が判明することになります。assumption方式では、assumptionビットに限定されていて、ハード制約であるDaily Cumulative Totalizerのビットまでは出てきません。
＜まとめ＞
■原因が判明しないときの王道は、地道にUNSATコアを出力して解析する
■UNSATコア出力は、assumption方式と、DRAT方式の2種類
■assumption方式は、UNSAT判明直後に取得可能だが、Kissatではサポートしていない。一方DRATは、解析ツールが必要で、時間がかかる場合もあるが、assumption方式では対応不能な真のCoflictに近い出力が可能
■DRATは、SAT Competitionで使用されKissatを含む最新ソルバで対応している
p cnf 34747 32
18864 0
18870 0
18872 -6493 -6487 0
18876 -18872 0
18882 -18876 -18870 0
18884 -6517 0
18887 -18884 -6511 0
18891 -6541 0
18892 -6547 -6541 0
18893 -18891 0
18894 -18892 0
18899 -18893 -18887 0
18900 -18894 -18887 0
18910 -18899 -18882 0
18911 -18900 -18882 0
18927 -18910 -18864 0
18928 -18911 -18864 0
-18930 -18927 0
-18931 -18928 0
-18941 18930 0
-18936 18941 0
-18942 18931 0
-18937 18942 0
-18943 18930 0
-18938 18943 0
18937 18936 18938 0
6487 0
6493 0
6511 0
6517 0
6541 0
6547 0
次の手順で、CNFファイルをKissatに読み込ませDRATファイルを出力します。それをdrat-trimツールで読み込ませて、UNSATコアを出力させることができます。
kissat [オプション] <入力DIMACSファイル> <出力証明ファイル>
kissat input.cnf proof.drat
proof.drat）を指定した場合、デフォルトでは効率的な バイナリDRATフォーマット で出力されます。--no-binary オプションを付けて実行してください。 [1]- を指定すると、証明を標準出力に流すことができます。この場合は自動的に ASCIIフォーマット になります。 [1]-f オプションを付与してください。 [1]proof.drat は、ソルバーが行った推論ステップの生ログです。ここから人間の読める最小限の矛盾原因（UNSAT Core）や証明検証を行うために、SATコミュニティの標準ツールである drat-trim を使用します。 [1]problem.cnf）と、上記コードで得られた proof.drat を指定して以下のように実行します。# 1. 証明の正当性を検証し、同時にUNSATの原因となった節のコア（core.cnf）を抽出する
drat-trim problem.cnf proof.drat -c core.cnf
仕方なく、CNFを生成して他のソルバで、DRATを出力させようと思いました。
void write_cnf(string filename) {
solver->open_file_and_dump_irred_clauses(filename);
}
ところが、UNSATの場合、CNFは、UNSATを意味する1行しか出力されておらず、元のCNF構成は、忘れてしまって出力できないようです。
仕方なく、自前でCNFを出力させました。
solver.open_file_and_dump_irred_clauses()）などは、高速化の都合上 p cnf ... のヘッダーを自動で出力してくれない仕様になっています。#include <iostream>
#include <fstream>
#include <vector>
#include <cmath>
#include <algorithm>
int main() {
// 追加したい節のデータ
std::vector<std::vector<int>> clauses = {
{1, 2, 3},
{-1, -2},
{-1, -3}
};
// 変数の最大数と節の数をカウント
int max_var = 0;
for (const auto& clause : clauses) {
for (int lit : clause) {
max_var = std::max(max_var, std::abs(lit));
}
}
int num_clauses = clauses.size();
// ファイル書き出し
std::ofstream outfile("problem.cnf");
if (outfile.is_open()) {
// ヘッダーを最初に出力
outfile << "p cnf " << max_var << " " << num_clauses << "\n";
// 各節と末尾の0を出力
for (const auto& clause : clauses) {
for (int lit : clause) {
outfile << lit << " ";
}
outfile << "0\n";
}
outfile.close();
}
return 0;
}
しかし、上のコードは、Kissat等で用いられる形式で、CryptiminisatのMinisat伝統のLit形式ではありません。
そこで、仕方なく、自前で書きました。
void write_cnf(string filename) {
// solver->open_file_and_dump_irred_clauses(filename);
int max_var = 0;
for (const auto& clause : lits_vec) {
for (auto lit : clause) {
if (max_var < (lit.var() + 1)) {
max_var = lit.var() + 1;// std::max(max_var, std::abs(lit.var()));
}
}
}
int num_clauses = lits_vec.size();
// ファイル書き出し
std::ofstream outfile(filename);
if (outfile.is_open()) {
// ヘッダーを最初に出力
outfile << "p cnf " << max_var << " " << num_clauses << "\n";
// 各節と末尾の0を出力
for (const auto& clause : lits_vec) {
for (auto lit : clause) {
if (lit.sign()) {
int v = -(int)(lit.var() + 1);
outfile <<v<< " ";
}
else {
int v = (lit.var() + 1);
outfile << v<<" ";
}
}
outfile << " 0\n";
}
outfile.close();
}
}