AE-Kissat-MABをWindowsにポート

AE-Kissat-MABは、SAT Competition 2025の優勝ソルバです。 

The Results of SAT Competition 2025

下のプロットを見ると他のソルバよりも明確な優位性が見られます。

このソルバは、生成AIでコードチューニングされています。

近年SAT Competitionの進歩は緩慢であり、これほどに大きなゲインは、Kissatの登場以来ではないかと思います。

しかし、この数か月後にNVIDA　SATLUTIONは、さらにこの上を行く発表しています。

https://schedule-nurse.blogspot.com/2026/02/saturation_9.html

が、コードは公開されていません。なので、現時点で、公開されている利用可能なSATソルバの頂点に位置するソルバと考えてよいです。

インスタンス24を解くには、やはりCardicalでは、メモリ使用量に難点があり、Kissatに頼らざるを得ない、ならば、最新ソルバを使用してみたい、という発想です。

で、疑似インクリメンタルな実装にしてみました。

https://schedule-nurse.blogspot.com/2026/02/kissatincremental.html

次が、作成したAPIです。胆は、

１）Phaseのセットができる

２）UnitClauseを含めた学習節のExport/Importが可能

３）簡略化で消されないようにするFreeze機能を装備

４）VSIDS/CHBのスコアをExport/Import

これにより、複数回Solveしても、問題なく求解できます。完全なシリアライズではありませんが、上記機能により主要な諸元は、リストアすることが出来ます。ほぼ、Warm Start機能を実現しました。問題なく機能が確認出来た後、Githubにアップします。

これでインスタンス24攻略に向けての最終部品が出来ました。今後，各ソルバ群（LPソルバ、SATソルバ、HIghsソルバ、数理ソルバ）の統合化作業を行い、再挑戦を行う予定です。

#ifndef KISSAT_WIN_API_H
#define KISSAT_WIN_API_H

#include "kissat.h"
#include 

// Windows特有の初期化（信号ハンドラやリソース制限のダミー設定）
kissat * kissat_win_init (void);

// 変数の保護（簡約化による消滅を防止）
void kissat_win_freeze_variables (kissat *solver, int first, int last);

// 外部から値をセットして求解し、学習内容を保存する一括処理
// 戻り値: 10 (SAT), 20 (UNSAT), 0 (UNKNOWN)
int kissat_win_solve_step (
    kissat *solver, 
    const int *phases,      // 変数1〜Nに対するTrue(1)/False(0)の配列
    int num_phases, 
    unsigned lbd_limit,     // 学習節の保存しきい値 (7等)
    const char *learned_path // 学習節の保存先 (NULLなら保存しない)
);

// 解（Model）の取得
int kissat_win_get_value (kissat *solver, int lit);

#endif