UNSATコアの解析

 次は、drat-trimで生成したUNSATコアの出力です。

p cnf は、ヘッダで、最大変数、と節数(32)が出力されています。2行目からは、UNSATコアが指摘している矛盾に関係している節になります。

例えば、18864という変数名は、プラスの符号なので、アサート(true)という意味になっています。同様に、18870という変数名もtrueであることを指示しています。このCNFを見ると二つの変数群グループに大別できます。

一つは、6500近辺の変数群と、18870近辺の変数群です。6500近辺の変数は、スタッフ、Day,シフトに対応した変数になっています。

次は、解析で判明した変数の対応です。

UNSATコアが出力しているのは、全てperson38,shift Eに限定されているので、パターン関係のエラーであることが分かります。また、18870付近の変数は、Daily Cumulative Totalizer付近の変数でそれとの矛盾を示していることが分かります。

このような解析を行うことによって、バグの原因が判明することになります。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