CP ソルバー — Google OR-Tools CP-SAT（PyQBPP のみ）

このページは 制約プログラミング (CP) のバックエンドを扱います.これは QUBO/HUBO を直接扱うサンプラ（QUBO/HUBO ソルバー）でも MILP ソルバー（MILP ソルバー）でもありません.CP エンジンは Boolean／整数変数を制約のもとで SAT 風のコアで探索し,証明付きの最適解 を返します.

現在の CP バックエンドは Google OR-Tools CP-SAT のみです.Python パッケージとしてのみ提供されるため,PyQBPP (Python) からのみ 利用可能で, C++ エントリーポイントはありません.

→ PyQBPP のドキュメントを参照してください: CP ソルバー — Google OR-Tools CP-SAT

OR-Tools CP-SAT は各非線形単項を新しい Boolean AND としてエンコードするため, 任意次数の HUBO と 否定リテラル (~x) をネイティブに 扱いながら証明 付きの最適解を返します — この組み合わせを満たす Hi-QUBO の外部ソルバーは これだけです.

このページは 制約プログラミング (CP) のバックエンドを扱います.これは QUBO/HUBO を直接扱うサンプラ（QUBO/HUBO ソルバー）でも MILP ソルバー（MILP ソルバー）でもありません.CP エンジンは Boolean／整数変数を制約のもとで SAT 風のコアで探索し,証明付きの最適解 を返します.

⚠️ Experimental — PyQBPP のみ. OR-Tools ライブラリ本体は実用に供されて いる製品ですが,PyQBPP 連携は実験的 で,ラッパ API は予告なく変更される 可能性があります.OR-Tools は Python パッケージとしてのみ提供される (pip install ortools) ため,このソルバーに C++ エントリーポイントは ありません.ソルバー生成時に遅延 import されます.

OrToolsCpSatSolver

Google OR-Tools CP-SAT は SAT ベースの制約プログラミングエンジン.CP-SAT は二次目的関数を ネイティブには受け付けないため,PyQBPP は各非線形単項 ℓ_a ℓ_b ... ℓ_k（各 ℓ は x_i または ~x_i）を新しい Boolean z として z = ℓ_a ∧ ... ∧ ℓ_k で制約し,結果として線形 目的関数を最小化します.HUBO は任意次数で同じエンコーディングが 効き,否定リテラルも CP-SAT の BoolVar.Not() でネイティブに扱われます （all_positive 展開は不要 — m 個の否定リテラルを含む単項を 2^m 倍に 膨らませずに済みます）：

sol = qbpp.OrToolsCpSatSolver(e).search(time_limit=5.0)

これにより OrToolsCpSatSolver は,任意次数の HUBO かつ 否定リテラルを ネイティブに受け付けながら証明付きの最適解を返せる,PyQBPP 唯一の外部 ソルバーになっています.

search() でよく使う kwargs: time_limit（秒,parameters.max_time_in_seconds）, thread_count（num_search_workers）,log（真偽値）.

戻り値の型

OrToolsCpSatSolver は PyQBPP 標準の SolverSol (EasySolverSol/ABS3SolverSol と同じ型) を返すため,プログラムの後段は ソルバー非依存に保てます:

print(sol.energy)            # 最良目的関数値
print(sol.tts)               # time-to-best-solution (秒)
print(sol.info["solver"])    # "OrToolsCpSatSolver"
for s in sol.sols:           # 追加で得られた解
    print(s.energy, s.tts)