スケジュールナースのブログ

2026年11月12日木曜日

SATソルバの長所と短所、MIPソルバとの対照的観点から

Q.SATソルバの長所と短所について、特にMIPソルバとの比較しながら論じて

SATソルバ（充足可能性問題ソルバ）は、命題論理式を用いた高速な分岐探索と強力な制約伝播（単位伝播）を得意とする一方で、数値的な目的関数の最適化や複雑な線形計算の扱いを苦手とします。

組合せ最適化や検証の分野でよく比較されるMIPソルバ（混合整数計画ソルバ）とは、対象とする問題構造や内部アルゴリズムに明確な違いがあります。それぞれの特徴を比較しながら、SATソルバの長所と短所を整理します。

SATソルバとMIPソルバの比較表

比較項目	SATソルバ	MIPソルバ
基本モデル	命題論理式（CNF：連言標準形）	線形不等式・等式と線形目的関数
扱える変数	ブール変数（真・偽 / 0・1）のみ	連続変数および整数変数
主な用途	充足可能性の判定（実行可能解の有無）	最適解の探索（目的関数の最小化・最大化）
コア技術	CDCL（矛盾駆動節学習）、単位伝播	分枝限定法、線形計画緩和（LP緩和）、切除平面法
得意な制約	論理的条件（IF-THEN、排他的論理和など）	数値の総和、容量制限、比率などの線形制約

SATソルバの長所（MIPソルバに対する優位点）

論理的制約の表現力と処理速度:
「AならばBである」「XとYは同時に成立しない」といった論理ルールを直接扱えます。MIPソルバでこれらを表現するには「Big-M法」などの技巧が必要になり、計算効率が落ちることが多いのに対し、SATソルバはそのまま高速に処理できます。
矛盾駆動節学習（CDCL）による強力な枝刈り:
探索中に矛盾が生じた際、その原因を分析して新しい制約（学習節）を動的に追加します。これにより、同じ失敗パターンを含む広大な探索空間を一度にスキップでき、数百万変数規模の巨大な論理問題でも解けることがあります。
単位伝播（Unit Propagation）の圧倒的な高速性:
変数の値が決まった瞬間に連鎖的に他の変数の値を確定させる処理（単位伝播）が極めて高速です。MIPソルバが各ノードで線形計画問題（LP）を解くのに比べて、1ノードあたりの探索コストが非常に低く抑えられます。
決定問題（実行可能性の判定）での強さ:
「条件を満たす解が1つでも存在するか（あるいは絶対に存在しないか）」を証明するタスクにおいて非常に強力です。ハードウェア・ソフトウェアの形式検証や、パズル・スケジューリングの制約充足で真価を発揮します。

SATソルバの短所（MIPソルバに対する劣位点）

目的関数の最適化が直接できない:
SATソルバは基本的に「Yes（充足可能）」か「No（充足不能）」を判定するツールです。コスト最小化や利益最大化を行うには、目的関数の値を変えながらSATソルバを何度も呼び出す（MaxSATやPBソルバなどの拡張を使う）必要があり、MIPソルバのようにはスマートに扱えません。
数値演算・線形制約の表現が苦手:
「重さの合計が100kg以下」といった単純な足し算の制約であっても、SATソルバではすべてのビット演算や組み合わせを論理回路（CNF）に展開する必要があります。変数の数や節の数が爆発的に増え、パフォーマンスが著しく低下します。
連続変数を扱えない:
扱う変数はすべて「0か1（偽か真）」の離散値に限定されます。流量、時間、金額などの連続的な値を扱う問題には直接適用できません。
大域的な見通し（緩和解）を持てない:
MIPソルバは「整数条件を外した線形計画問題（LP緩和）」を解くことで、現在の探索枝から得られる最良の目的関数値の上界・下界を数学的に見積もることができます。SATソルバにはこのような大域的な指針がないため、数値的な最適化問題では無駄な探索が増えがちです。

使い分けの目安

SATソルバが適しているケース:
複雑なルールや論理的条件が絡み合う問題、実行可能なスケジュールや配置を1つ見つけたい場合、システムのバグや仕様の不整合を厳密に検証したい場合。
MIPソルバが適しているケース:
コストや利益などの明確な評価指標（目的関数）を最適化したい場合、資源配分・物流・生産計画など、数値の足し算や容量制約が中心となる場合。

2026年11月10日火曜日

c++　テンプレートとconst_expr

実装ステージに入っています。雑多なコードをテンプレート化により整理します。実装では、何が良い実装か未だ確定しないので、パラメータは、テンプレート化して、後で変えるだけで、実装の中身も変えます。テンプレートが決まると固定した定数が出てくるので、さらにconst_exprにより静的にコンパイルするようにします。if文であっても、静的に評価されるので、実行時は、if文にはなりません。

一にアルゴリズム、二にデータ構造、三に実装テクニックですが、最後の部分でも数％の効果が期待できます。

WRITE＿WIDTH＝４，６，８，１２，１６，２０，２４で最適化コードを。

WRITE_WIDTH が 4,6,8,12,16,20,24 の固定値しか来ないなら、memcpy() に任せるより専用化した方が速いです。

ポイントは、

16byteまでは a0 の計算結果だけで完結

20,24byteは次の128bitも加算して一部書く

SSE2のみ使用

ストア数最小

template<int WRITE_WIDTH>

static inline void add_u8_aligned16_X(

unsigned char* A,

const unsigned char* B)

{

__m128i a0 = _mm_load_si128((const __m128i*)(A + 0));

__m128i b0 = _mm_load_si128((const __m128i*)(B + 0));

a0 = _mm_add_epi8(a0, b0);

if constexpr (WRITE_WIDTH == 4)

{

*(uint32_t*)A = (uint32_t)_mm_cvtsi128_si32(a0);

}

else if constexpr (WRITE_WIDTH == 6)

{

uint32_t lo32 = (uint32_t)_mm_cvtsi128_si32(a0);

uint16_t hi16 = (uint16_t)(_mm_extract_epi16(a0, 2));

*(uint32_t*)(A + 0) = lo32;

*(uint16_t*)(A + 4) = hi16;

}

else if constexpr (WRITE_WIDTH == 8)

{

_mm_storel_epi64((__m128i*)A, a0);

}

else if constexpr (WRITE_WIDTH == 12)

{

_mm_storel_epi64((__m128i*)A, a0);

uint32_t x =

(uint32_t)_mm_extract_epi16(a0, 4)

| ((uint32_t)_mm_extract_epi16(a0, 5) << 16);

*(uint32_t*)(A + 8) = x;

}

else if constexpr (WRITE_WIDTH == 16)

{

_mm_store_si128((__m128i*)A, a0);

}

else if constexpr (WRITE_WIDTH == 20)

{

__m128i a1 = _mm_load_si128((const __m128i*)(A + 16));

__m128i b1 = _mm_load_si128((const __m128i*)(B + 16));

a1 = _mm_add_epi8(a1, b1);

_mm_store_si128((__m128i*)(A + 0), a0);

*(uint32_t*)(A + 16)

= (uint32_t)_mm_cvtsi128_si32(a1);

}

else if constexpr (WRITE_WIDTH == 24)

{