概要
ソルバー（Solver）は、数学的最適化問題や方程式系を計算で解くエンジンを指す。1947 年の George Dantzig による線形計画法（LP / Simplex 法）から始まり、現代では (1) 線形計画（LP）、(2) 整数計画（IP / MIP）、(3) 非線形計画（NLP）、(4) 制約充足（CSP / SAT / SMT）、(5) 微分方程式系等の幅広い問題を扱う。2026 年現在、Gurobi / CPLEX / Mosek 等の商用ソルバーが世界記録を更新し続けながら、SciPy / PuLP / CVXPY の OSS が個人 / 学術で広く使われ、Microsoft の Z3（SAT/SMT）は形式検証で業界標準となっている。
主要ソルバー（2026 年）
線形 / 整数計画（LP / MIP）
| ソルバー | 形態 | 価格 | 特徴 |
|---|
| Gurobi | 商用 | $10,000-/年 | 業界最速、世界記録保持 |
| IBM CPLEX | 商用 | $5,000-/年 | 老舗、業界標準 |
| Mosek | 商用 | $5,000-/年 | 円錐最適化に強い |
| FICO Xpress | 商用 | $7,000-/年 | 北米金融多用 |
| HiGHS | OSS | 無償 | 商用品質 OSS、急成長 |
| SCIP | OSS | 学術無償 | MIP 強力 |
| GLPK（GNU LP Kit） | OSS | 無償 | 軽量、教育用 |
| OR-Tools | OSS（Google） | 無償 | 統合フレームワーク |
非線形計画（NLP）
| ソルバー | 形態 |
|---|
| Ipopt | OSS、業界標準 |
| KNITRO | 商用 |
| SNOPT | 商用 |
| Bonmin | OSS |
SAT / SMT（制約充足）
| ソルバー | 形態 | 用途 |
|---|
| Z3 | OSS（Microsoft） | 形式検証、SMT 業界標準 |
| cvc5 | OSS、Stanford 由来 | 高機能 SMT |
| MiniSat | OSS | SAT 最古参 |
| Glucose | OSS | 競技 SAT 強い |
| CryptoMiniSat | OSS | 暗号系 SAT |
| Yices 2 | OSS | SMT |
微分方程式 / シミュレーション
| ソルバー | 形態 | 用途 |
|---|
| SciPy.integrate | Python OSS | ODE 一般 |
| Sundials | OSS | 工業用 ODE/DAE |
| SUNDIALS CVODE | OSS | 大規模 ODE |
| FEniCSx | OSS | FEM 微分方程式 |
統合フレームワーク（モデリング言語）
| フレームワーク | 言語 | 特徴 |
|---|
| PuLP | Python | LP / MIP 入門 |
| CVXPY | Python | 凸最適化、研究用 |
| JuMP | Julia | 高速 + 表現力 |
| Pyomo | Python | 大規模、AMS 互換 |
| AMPL | 独自言語 | 業務最適化定番 |
| GAMS | 独自言語 | 経済モデル |
用途別の典型問題
| 分野 | 問題例 |
|---|
| サプライチェーン | 配送経路最適化（TSP） |
| 金融 | ポートフォリオ最適化（Markowitz） |
| 製造 | 工場スケジューリング |
| エネルギー | 発電所運用計画 |
| 物流 | コンテナ配置 |
| 公共交通 | 時刻表最適化 |
| 通信 | ネットワーク帯域割当 |
| AI | ニューラルネット訓練（SGD） |
| ゲーム | 動的計画 |
| 検証 | プログラム正当性証明 |
Python での簡易例（PuLP + Gurobi）
import pulp
# 線形計画問題: max 3x + 5y subject to x + 2y <= 8, 3x + y <= 9
prob = pulp.LpProblem("Example", pulp.LpMaximize)
x = pulp.LpVariable("x", lowBound=0)
y = pulp.LpVariable("y", lowBound=0)
prob += 3 * x + 5 * y # 目的関数
prob += x + 2 * y <= 8 # 制約
prob += 3 * x + y <= 9
prob.solve(pulp.GUROBI()) # Gurobi 商用ソルバー
print(f"最適値: {pulp.value(prob.objective)}")
print(f"x = {x.varValue}, y = {y.varValue}")
Excel / Google Sheets
| 製品 | ソルバー |
|---|
| Microsoft Excel | Solver アドイン（Frontline 製、無償付属） |
| Google Sheets | Linear Optimization アドオン（OR-Tools 系） |
| LibreOffice Calc | 内蔵 SCIP / Coin-OR CBC |
非エンジニアでも GUI で線形計画問題を解ける。
Z3（SMT）の例
from z3 import *
x, y = Ints("x y")
solver = Solver()
solver.add(x + y == 10)
solver.add(x > 0)
solver.add(y > 0)
solver.add(x * y >= 21)
if solver.check() == sat:
print(solver.model())
# x = 7, y = 3 等の解を出力
形式検証 / プログラム検証 / 暗号解析で広く使われる。
PC スペック要件
- 小規模 LP（変数 < 1000）: 任意 PC で十分
- 中規模 MIP（変数 < 10K）: Ryzen 7 7700X / 32 GB RAM
- 大規模 LP/MIP（変数 100K+）: Ryzen 9 9950X / 128 GB RAM
- Gurobi 並列計算: コア数多いほど速い、Threadripper 推奨
- GPU 加速ソルバー（cuOpt 等）: NVIDIA GPU 専用
関連用語との違い
| 用語 | 違い |
|---|
| アルゴリズム | 解法手順、ソルバーは実装 |
| エンジン | より広い概念、ソルバーは数値最適化特化 |
| シミュレータ | 動的挙動、ソルバーは静的方程式 |
| AI モデル | 学習駆動、ソルバーは数学的厳密 |
よくある質問
Q1: Gurobi と CPLEX、どちらを選ぶ？
A: 速度なら Gurobi（多くのベンチで 2-5 倍）、機能の幅は同等。価格交渉次第。学術用途は両者無償ライセンス提供あり。OSS で十分なら HiGHS が急成長中。
Q2: SAT ソルバーは AI で使う？
A: 部分的に。LLM の論理推論は確率的、SAT/SMT は厳密証明。Microsoft の Z3 は Visual Studio / Slack の検証で使用。AI x 形式手法のハイブリッドは研究領域として活発。
Q3: Excel Solver で何ができる？
A: 中小規模の業務最適化（在庫配分 / シフトスケジュール / 投資配分）まで実用。変数 200 以下 / 制約 100 以下が目安。本格運用は Gurobi or HiGHS に移行。
まとめ
- 数学的最適化問題を 計算で解くエンジン
- 2026 年は Gurobi / CPLEX（商用）+ HiGHS / SciPy / Z3（OSS） が主流
- 用途別に LP / MIP / NLP / SAT / SMT で使い分け