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

2026年11月13日金曜日

スラックの扱いに違いがある

最適値を求めるという目的は同じです。だから、最適値を速く正確に求められるならSATとMIPのどちらの方法を取ってもよいのです。

で、スケジュールナース上で、何が違うかというとスラックの実装の違いにあります。

新しいバージョンでは、許容エラーという言い方を止めて、「スラック」にしようと思っています。

スラックとは何か、というとソフト制約の幅になります。ソフト制約領域に入ると1ソフトエラーに対して、重みを乗算した値がコストとして発生します。例えば、夜勤回数が４回、スラックが３(旧許容エラー）のときを考えます。夜勤が５回の解の場合、重み２のとき、２ｘ１のコストが発生します。

しかし、どこまでもソフト領域が広がっていることはありません。この場合スラックは、３ですから、必ずハード制約でクリップされて、それ以上は、コストが発生しないように制約されます。この場合、４＋３＝７回までは、ハード制約に違反しないので解は存在し得ます。もしどうしてもハード制約を上回ることなしに解が存在しえないときは、「解がない」状態となります。逆に言うと、解が存在するならば、その解は、必ず夜勤回数７回以下になるということです。

SATでも、MIPでも上記スラックの挙動は同じです。違うのは、スラックの実装にあります。SATは、ブール値「０」か「１」しか変数として持てません。なのでスラックもバイナリ変数で持ちます。スラックが３のとき、最大－最小制約では、上側３個、下側３個のバイナリ変数を要します。SATの場合、スラックの幅が大きければ大きい程、必要な変数数が大きくなります。

これに対してMIPは、リニアソルバをベースとするので、スラックを１個の連続変数に割り当てることが出来ます。つまりどれだけ多くのスラックを確保したとしてもスラックは１個で済みます。(上下に１個のスラックを配置した場合でも２個で済みます）

つまり、SATでは、スラックが大きければ大きい程、メモリコストがかかるのに対して、MIPでは、スラックの大きさに不感です。

スケジュールナースAL1は、SATベースなので、上記SATの短所がそのまま当てはまります。一方AL3では、内部深層においては、リニアソルバベースにしています。整数化の最後だけは、SATソルバの表皮となる予定です。概念的にスラック∞という発想も可能ですが、そこまで行うかは、未だ決定していません。

いずれにせよ、真の最適値は、スラック範囲のどこかにあります。AL3が、何故ソフト制約だらけの規模の大きな勤務表で優位となるかを、なんとなくでも分かっていただけたら幸いです。

最初から「スラック」という言葉で実装すればよかったのですが、スケジュールナースⅠの時代は、未だ私がOR（オペレーションズリサーチ）を勉強する前だったので、知らなかったのが実相です。しかし、その知らなかった時代から、ソフト制約の必然概念を実装していた私は偉かった、ということでしょう。

いずれせよ、ユーザが、スラックを直接に弄れる勤務表ソフトは、スケジュールナース以外ないのでは？と思います。実は、それが、学術ベンチマークで??の、私の答えです。

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)

{