satsumaとは？

 2026SAT competition2026結果をよく見ると、大きく向上していることが分かります。特にUNSATの伸びは、近年では一番と言ってよいのではないでしょうか？この秘密を探りました。

satsumaとは？

CNF式の「対称性」を検出して壊す、独立した前処理ツールです(Markus Anders (RPTU Kaiserslautern-Landau) と Cayden Codel (CMU) 開発、SAT 2024で発表・SAT'26 Best Paper受賞)。

入力/出力: DIMACS CNF → 等充足(equisatisfiable)な、対称性を壊したCNFを出力するだけ。ソルバーには一切依存しない、パイプラインの前段に挟むだけのツールです

仕組み: dejavuというグラフ同型判定ソルバーを使い、CNFを(変数・節の関係を表す)グラフとして扱って自動的にグラフ同型群(=論理式の対称性)を検出。そのうえで対称な解を除外する制約を追加します

2つのモード:

satsuma fix — 検出した対称性を使って変数を直接固定・消去(場合によっては変数自体を消せる)

satsuma lex — 「辞書順で最小の解だけを許す」制約(lex-leader constraint)を追加

大会結果に出てきた satsuma-iter+kissat(優勝)・satsuma-lex+kissat はこの手法の異なる設定と見られます(iterは対称性検出→固定を繰り返し適用する版と推測されますが、READMEには明記が薄く未検証です)

使い方: satsuma fix formula.cnf > output.cnf としてCNFを加工し、その結果を好きなソルバー(例: kissat output.cnf)に渡すだけ。ソルバー本体には一切手を入れません

なぜ効くのか(前回の回答の補足)

多くの実問題(ハードウェア検証、組合せ問題など)のCNFには「変数を入れ替えても論理的に同じ」という対称性が大量に潜んでいます。CDCLソルバーは対称な解候補を何度も別々に探索してしまいがちで、これを事前に1つの代表解だけに絞ることで探索空間そのものを縮小できます。これがkissatのコア(CDCL探索)を一切変えずに +38問(238→276、前回表参照)もの差を生んだ理由です。

解互換性について

いいえ、単純にはそのまま互換ではありません。「SAT/UNSATの判定結果(充足可能かどうか)」は保証されますが、「見つかった解(モデル)」がそのまま使えるかはモード次第です。

SAT/UNSAT判定: 常に保証(equisatisfiable)

satsumaが返すのは常に元のCNFと等充足(equisatisfiable)な式です。つまり「SATかUNSATか」という結果自体は変換前後で完全に一致します。UNSATの場合はさらに証明(fixモードはSR/バイナリSR形式が安定版、VeriPBは実験段階。lexモードはVeriPBのみ)を出力でき、これをkissat自身が出す証明と繋いで大会が要求する完全な証明チェーンを作れます。

モデル(具体的な変数割り当て)の互換性: モードで挙動が違う

satsuma fix(変数を固定・消去するモード): 公式ドキュメントに明記されている通り、「対称性を利用して変数そのものを式から取り除くことがある」ため、縮小後の式で見つかった充足割り当ては、元の式の全変数に対する割り当てにはなっていない場合がある、と明言されています。

デフォルトではモデルの互換性は保証されません。互換性が欲しい場合は --add-reduced-as-unit オプションを付ける必要があります(「これを付ければ縮小後の式のどんな充足割り当ても、元の式の妥当な充足割り当てになる」との記載)

このオプションなしだと、消去された変数の値を復元する「reconstruction/witness」的な後処理が別途必要になりますが、そこを自動でやってくれる仕組みはドキュメント上見当たりませんでした

satsuma lex(辞書順最小解に絞る制約を追加するモード): こちらは新しい制約(節)を追加するだけで、変数自体は消していないと読めます。追加された制約は「元の解集合の部分集合だけを許す」ものなので、見つかった解はそのまま元のCNFの妥当な解になるはずです(ただしREADMEに「新規変数を一切導入しない」と明示的に断言されているわけではなく、そこは断定できません)

kissat-cppへの実装インパクト

SAT/UNSATの判定結果だけ欲しいなら、どちらのモードでも問題なく使えます

solver.value(lit) で実際の変数割り当て(モデル)を取りたいなら、

lex モードを使うか、

fix モードなら --add-reduced-as-unit を付けて使う

のどちらかが安全です。付けずに fix を使うと、kissatxxの units()/value() で返ってくる値が元の変数番号と食い違う(あるいは一部の変数が消えていて値を取れない)可能性があります

Sources: markusa4/satsuma (GitHub), satsuma: Structure-based Symmetry Breaking in SAT (arXiv)

fixとlexでは、どちらが解きやすいと考えられますか？

閲覧済み ウェブ

実際の大会データと理論的な違いの両面から見ると、fix(特にその発展形であるiter)の方が明確に「解きやすい式」を作ります。

大会での実測(前回計算したCSVより)

構成 解けた数/400 PAR-2

satsuma-iter+kissat(優勝、Anders/Codel) 276 3647.02

satsuma-lex+kissat(Oertelチーム) 249 4279.58

kissat単体(前処理なし) 238 4611.54

iterはkissat単体比+38問(+16%)、lexは+11問(+4.6%)。同じkissatバックエンドで、iterはlexの3倍以上の伸びしろを引き出しています。

なぜ差が出るのか(手法上の理由)

fix系(iterもこの系統): 検出した対称性を使って変数そのものを固定・消去します。つまり式を物理的に縮小してからソルバーに渡す。しかもiterの元になっている2026年の新論文 "Simplify, Order, Break, Repeat" によれば、対称性破壊を「単なる探索空間の制限」ではなく「簡約化(simplification)手段」と位置づけ、unit/binary節だけを追加する軽い変換に留めることで、その簡約が新たな対称性を露出させ、さらにもう一段対称性を壊せる——というのを繰り返す(Repeat)設計です。この論文はCaDiCaLの前処理としてPAR-2を2025年大会で22%、Anniversary trackで12%改善したと報告しており、fix系アプローチの優位性は他の実験でも裏付けられています

lex: 変数は一切消さず、「対称性のある解のうち辞書順最小のものだけ許す」という制約(lex-leader constraint)を追加するだけです。式は縮小されず、むしろ制約節が増える分だけ形式的には大きくなります。対称群が大きいとlex-leader制約自体が長大・複雑になりやすいことも知られており、追加した制約の処理コストが枝刈り効果を目減りさせがちです

トレードオフも存在する

ただし前回お伝えした通り、fixは変数を消してしまうぶんモデル(具体的な解の値)をそのまま元の式に使えない場合がある(--add-reduced-as-unitか別途reconstructionが必要)のに対し、lexは変数を消さないのでモデルの互換性は素直に保たれます。

→ 「解けるかどうか・どれだけ速く解けるか」だけを重視するならfix/iterが有利、「モデルをそのまま使いたい/実装をシンプルに保ちたい」ならlexが安全、という住み分けです。kissat-cppに組み込むなら、SAT/UNSAT判定だけでなくsolver.value()で解の中身も使う設計なので、fixを使うなら--add-reduced-as-unit必須、という前回の結論と合わせて検討する必要があります。

Sources: Simplify, Order, Break, Repeat (SAT 2026), satsuma: Structure-based Symmetry Breaking in SAT (arXiv), markusa4/satsuma (GitHub), SAT Competition 2026 raw scores