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

2026年11月14日土曜日

puedo boolean competitionとmaxsatの違い

どちらもSATソルバを内部で使うことは同じです。最近のPBソルバは、MIPソルバも併用する傾向があります。MIPモデリング形態であるMPSフォーマットを読めるソルバもあります。MIPにより近いのは、PBソルバということになります。何とかして、線形制約を解こうとする試みですが、ベースはSATソルバであり、前述の本質的な弱点をカバーするのは難しいと思います。

Pseudo-Boolean Competition（擬似ブール競技会）と MaxSAT（最大充足可能性問題）の最も大きな違いは、「対象とする問題の表現形式（制約の書き方）」と「競技会としての位置づけ」にあります。 [1, 2, 3]

MaxSATは「論理式（節）の充足数」を最適化する問題枠組みであるのに対し、Pseudo-Boolean（PB）は「0-1変数の線形不等式（整数係数付き）」を扱う問題枠組みです。なお、MaxSATを競う大会としては MaxSAT Evaluation が存在し、Pseudo-Boolean Competition と並んでSAT国際会議（SAT Conference）の併設競技会として開催されています。 [1, 2, 3]

問題形式・理論上の違い

両者ともブール変数（0または1）を扱いますが、制約の表現能力に明確な差があります。 [1, 2]

比較項目	Pseudo-Boolean (PB / PBO)	MaxSAT (最大充足可能性問題)
基本の制約形式	線形不等式（例: 3x₁ + 2x₂ - x₃ ≥ 4）	節（Clause / 論理和）（例: \(x_1 \lor \neg x_2 \lor x_3\)）
数学的な位置づけ	0-1整数線形計画問題（0-1 ILP）と等価	充足可能性問題（SAT）の最適化版
表現力（コンパクトさ）	重み付き和や「〜個以上選ぶ」制約を1本の式で直接書ける	数値の足し算や比較を論理式に展開するため式が膨大になりやすい
目的関数	線形関数（または非線形関数）の最小化・最大化	満たされるソフト節の重み合計の最大化（違反コストの最小化）

競技会としての違い

国際会議SATに合わせて毎年開催されるソルバー競技会としては、それぞれ独立したイベントとして運営されています。 [1]

Pseudo-Boolean Competition（PB Competition）
擬似ブール制約の充足判定（PBS）および最適化（PBO）ソルバーの性能を競う大会です。入力形式には専用の OPB 形式などが使われ、近年は VeriPB による証明検証トラックや、非線形制約（Non-linear）トラックなども設けられています。 [1, 2]
MaxSAT Evaluation
MaxSATソルバーの性能を競う国際評価イベントです。入力形式には重み付きCNF（WCNF形式）が用いられ、厳密解法（Complete）と局所探索などの近似解法（Incomplete）の両部門で評価が行われます。 [1, 2]

技術的な関係性と使い分け

両者は互いに変換可能であり、ソルバーの内部技術も深く結びついています。 [1, 2]

包含関係
MaxSATは「係数がすべて1の特殊な擬似ブール最適化（PBO）」とみなすことができます。逆に、PB制約を論理回路のようにCNFへ変換してMaxSATソルバーやSATソルバーで解く手法も一般的です。 [1, 2, 3]
推論手法の違い
MaxSATソルバーはSAT由来の節学習（CDCL）やUnsat-core抽出を軸に動作します。一方、ネイティブなPBソルバーは整数計画法に近い切除平面法（Cutting Planes）による強い推論を行えるため、組み合わせの個数制限や重み計算が複雑な問題で有利になります。 [1, 2, 3]

PBソルバは、MPSフォーマットが読めるのですか？

結論から言うと、一般的なPB（Pseudo-Boolean）ソルバの多くは、標準でMPSフォーマットを直接読み込むことはできません。

PBソルバは競技会（Pseudo-Boolean Competition）などで採用されている OPBフォーマット（.opb）を標準入力として設計されているためです。ただし、一部のソルバやツールを組み合わせることでMPS形式を扱うことは可能です。

1. なぜ直接読めないのか（フォーマットの背景の違い）

OPB形式（PBソルバの標準）
すべての変数が 0-1変数であることを前提としており、文法がシンプルでパース（読み込み）が高速です。
MPS形式（数理最適化・MIPの標準）
連続変数、一般整数変数、範囲制約、SOS（特殊順序集合）など、混合整数計画法（MIP）の複雑な要素をすべて記述できる歴史ある業界標準フォーマットです。

2. MPS形式のデータをPBソルバで解く方法

0-1整数線形計画問題（0-1 ILP）として記述されたMPSファイルであれば、以下のアプローチでPBソルバを利用できます。

フォーマット変換ツールを使う（最も一般的）
MPSファイルをOPB形式に変換してからPBソルバに渡す方法です。代表的な数理最適化ソルバや変換ツール（SCIPの変換機能や、専用のPythonスクリプト、pblib などの変換ユーティリティ）を使って .mps を .opb に書き出せます。
MPS対応のハイブリッド／MIPソルバを使う
たとえば SCIP は混合整数計画（MIP）ソルバですが、PB制約の処理やPBソルバ的な推論機能も内蔵しており、MPS形式を直接読み込んで解くことができます。また、RoundingSat などの一部PBソルバでも、コンパイルオプションやフロントエンドツール経由でMPSやLP形式の入力をサポートするケースがあります。

3. 変換時の注意点

MPSファイルをOPBに変換する場合、元のMPSファイルが純粋な0-1問題（Pure Binary）である必要があります。もし連続変数（実数）や、0と1以外の値をとる一般整数変数が含まれている場合、そのままではPBソルバでは扱えない（一般整数は二進展開などのエンコーディングが必要になる）点に注意してください。

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)

{