# CP ソルバー — Google OR-Tools CP-SAT(PyQBPP のみ)
:::{container} prog-cpp
このページは **制約プログラミング (CP)** のバックエンドを扱います.これは
QUBO/HUBO を直接扱うサンプラ([QUBO/HUBO ソルバー](../solver/experimental-solvers.md))でも
MILP ソルバー([MILP ソルバー](../solver/experimental-solvers.md))でもありません.CP エンジンは
Boolean/整数変数を制約のもとで SAT 風のコアで探索し,**証明付きの最適解**
を返します.
現在の CP バックエンドは **Google OR-Tools CP-SAT** のみです.Python
パッケージとしてのみ提供されるため,**PyQBPP (Python) からのみ** 利用可能で,
C++ エントリーポイントはありません.
→ PyQBPP のドキュメントを参照してください:
[**CP ソルバー — Google OR-Tools CP-SAT**](../solver/cp-solvers.md)
OR-Tools CP-SAT は各非線形単項を新しい Boolean AND としてエンコードするため,
**任意次数の HUBO** と **否定リテラル (`~x`) をネイティブに** 扱いながら証明
付きの最適解を返します — この組み合わせを満たす Hi-QUBO の外部ソルバーは
これだけです.
:::
:::{container} prog-python
このページは **制約プログラミング (CP)** のバックエンドを扱います.これは
QUBO/HUBO を直接扱うサンプラ([QUBO/HUBO ソルバー](../solver/experimental-solvers.md))でも
MILP ソルバー([MILP ソルバー](../solver/experimental-solvers.md))でもありません.CP エンジンは
Boolean/整数変数を制約のもとで SAT 風のコアで探索し,**証明付きの最適解**
を返します.
> **⚠️ Experimental — PyQBPP のみ.** OR-Tools ライブラリ本体は実用に供されて
> いる製品ですが,**PyQBPP 連携は実験的** で,ラッパ API は予告なく変更される
> 可能性があります.OR-Tools は Python パッケージとしてのみ提供される
> (`pip install ortools`) ため,このソルバーに C++ エントリーポイントは
> ありません.ソルバー生成時に遅延 import されます.
## OrToolsCpSatSolver
[Google OR-Tools CP-SAT](https://developers.google.com/optimization/cp/cp_solver)
は 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 倍に
膨らませずに済みます):
```{include} /../programFiles/markDown/solver/cp-solvers.md
:start-after:
:end-before:
```
これにより `OrToolsCpSatSolver` は,任意次数の HUBO **かつ** 否定リテラルを
ネイティブに受け付けながら証明付きの最適解を返せる,PyQBPP 唯一の外部
ソルバーになっています.
`search()` でよく使う kwargs:
`time_limit`(秒,`parameters.max_time_in_seconds`),
`thread_count`(`num_search_workers`),`log`(真偽値).
## 戻り値の型
`OrToolsCpSatSolver` は PyQBPP 標準の `SolverSol`
(`EasySolverSol`/`ABS3SolverSol` と同じ型) を返すため,プログラムの後段は
ソルバー非依存に保てます:
```{include} /../programFiles/markDown/solver/cp-solvers.md
:start-after:
:end-before:
```
:::