KISSATでDRAT生成

 次の手順で、CNFファイルをKissatに読み込ませDRATファイルを出力します。それをdrat-trimツールで読み込ませて、UNSATコアを出力させることができます。

SATソルバの Kissat でDRAT形式の証明（Proof）を生成するには、コマンドの引数（オプション）として 入力のDIMACSファイルの後に、出力したい証明ファイルのパスを指定 します。 [1, 2]

基本的なコマンド構文

bash

kissat [オプション] <入力DIMACSファイル> <出力証明ファイル>

コードは注意してご使用ください。

具体的な使用例

たとえば、input.cnf という問題ファイルから、proof.drat という証明ファイルを生成する場合は、以下のように実行します。 [1]

bash

kissat input.cnf proof.drat

コードは注意してご使用ください。

重要な仕様と注意点

• フォーマットの自動判定:
  • 実際のファイル名（例: proof.drat）を指定した場合、デフォルトでは効率的な バイナリDRATフォーマット で出力されます。
  • テキスト（ASCII）形式で出力したい場合は、--no-binary オプションを付けて実行してください。 [1]
• 標準出力への出力:
  • 出力ファイル名に - を指定すると、証明を標準出力に流すことができます。この場合は自動的に ASCIIフォーマット になります。 [1]
• ファイルの圧縮:
  • 出力ファイルの拡張子を .gz や .bz2、.xz などにすると、Kissatが自動的にバックエンドツール（gzipなど）を呼び出し、圧縮しながら証明を書き出します。DRATファイルは非常に肥大化しやすいため、圧縮出力が推奨されます。 [1, 2, 3]
• 上書きの強制:
  • 既存のファイルを強制的に上書きして証明を書き出す場合は、-f オプションを付与してください。 [1]
• UNSAT時のみ有効:
  • DRATは「充足不能（UNSAT）」であることの証明を出力する仕組みです。問題が「充足可能（SAT）」な場合は、空の証明、または実質的な中身のないファイルになります。 

生成されたDRAT証明ファイルは、後から drat-trim などの検証ツール（Checker）を用いて、正当性をチェックすることができます。

 出力されたDRATから矛盾原因（UNSAT Core）を抽出する [1]

C++ APIから直接得られる proof.drat は、ソルバーが行った推論ステップの生ログです。ここから人間の読める最小限の矛盾原因（UNSAT Core）や証明検証を行うために、SATコミュニティの標準ツールである drat-trim を使用します。 [1]

drat-trimは、Windows版はないので、Win11のUbuntsu上でコンパイルし作成します。

実行コマンド（ターミナル）

元の問題ファイル（problem.cnf）と、上記コードで得られた proof.drat を指定して以下のように実行します。

bash

# 1. 証明の正当性を検証し、同時にUNSATの原因となった節のコア（core.cnf）を抽出する
drat-trim problem.cnf proof.drat -c core.cnf