SATソルバーでPodの配置を決定する

## 問題

Kubernetesを使った設計していて、「どのワーカーノードにどのPodを配置すると、ノードのハードウェアリソースに収まる範囲で、冗長性を確保できるのか」という問題に直面しました。Kubernetesのスケジューラーが良きに計らってくれると嬉しいですが、諸般の事情により設計者が手作業でPod配置を決定する必要に迫られてしまったのでこの問題を解くためのコードを作ってみました。

### 条件

* それぞれのPodはCPU, メモリなどのリソースを要求する
* 配置したいPod数は既に決まっている
* ワーカーノードのリソース（CPUなど）は既に決まっており、その範囲内に収まるようにPodを配置する
* 1つのReplicaSetから作られるPodが1つのワーカーノードに偏ってしまうとそのノードの障害時に全滅してしまうので、冗長性を持たせて配置する

## 対応

Z3というソルバーを使ってみます。Z3はSMTソルバーというものの1つで上記のような条件を与えると、その条件を満たす解を求めてくれます。https://github.com/Z3Prover/z3

今回はCPUコア数をハードウェアリソースとして条件を与えることにします。以下はJupyterを用いたコードになっています（Python初心者のため変なところがたくさんあると思います）。Pod名は https://github.com/GoogleCloudPlatform/microservices-demo を真似ました。

```python
!pip install z3-solver tabulate

import numpy as np
from z3 import *
import functools
import tabulate
from IPython.display import HTML, display

# 問題設定
nodes = [{'name':'node001', 'cpu': 7}, {'name':'node002', 'cpu': 5}, {'name':'node003', 'cpu': 6}, {'name':'node004', 'cpu': 5}]
replica_sets = [{'name':'frontend', 'replicas':4, 'min_replicas': 2, 'cpu': 1.5}, {'name':'cart', 'replicas':4, 'min_replicas': 2, 'cpu': 1.3}, {'name':'email', 'replicas':4, 'min_replicas': 2, 'cpu': 0.5}, {'name':'ad', 'replicas':3, 'min_replicas': 1, 'cpu': 0.2}, {'name':'payment', 'replicas':4, 'min_replicas': 2, 'cpu': 0.2}, {'name':'currency', 'replicas':1, 'min_replicas': 0, 'cpu': 0.2}, {'name':'shipping', 'replicas':6, 'min_replicas': 3, 'cpu': 0.1}, {'name':'recommendation', 'replicas':2, 'min_replicas': 1, 'cpu': 2}]
config = np.array([Real(f'v{i}') for i in range(len(nodes)*len(replica_sets))]).reshape((len(nodes), len(replica_sets)))

solver = Solver()

# solverへ制約を入力
for i in range(len(nodes)):
    for j in range(len(replica_sets)):
        # 配置数は0以上
        solver.add(config[i][j] >= 0)
        # 配置数は整数(配置数をReal型ではなくIntで定義するとSumで小数点以下が切り落とされてしまうためReal型で宣言してこの制約で整数に絞る)
        solver.add(deployment[i][j] == ToInt(config[i][j]))
# それぞれのノードに配置したpodの合計がreplica_setのreplicasになっている
for j in range(len(replica_sets)):
    solver.add(Sum([deployment[i][j] for i in range(len(nodes))]) == replica_sets[j]['replicas'])
# それぞれのノードに配置したpodが使用するリソース合計がノードのリソースに収まっている
for i in range(len(nodes)):
    solver.add(Sum([replica_sets[j]['cpu'] * config[i][j] for j in range(len(replica_sets))]) <= nodes[i]['cpu'])
# N+1の冗長性を持つ(どれか1ノードが停止したとしてもmin_replicas以上の稼働数となる)
for k in range(len(nodes)):
    for j in range(len(replica_sets)):
        solver.add(Sum([config[i][j] for i in range(len(nodes))]) - config[k][j] >= replica_sets[j]['min_replicas'])

# 結果表示
if solver.check() == sat:
    model = solver.model()
    
    print('Pod配置')
    # ndarrayへ変更
    result = np.frompyfunc(lambda v: model[v].as_long(), 1, 1)(config)
    # ノード名の列を追加
    display_result = np.insert(result, 0, 'name', axis=1)    
    for i in range(len(nodes)):
        display_result[i][0] = nodes[i]['name']
    # 表示
    pod_headers = []
    for r in replica_sets:
        pod_headers.append(r['name'])
    pod_headers.insert(0, 'node')
    display(HTML(tabulate.tabulate(display_result, pod_headers, tablefmt='html')))

    print('各ノードのリソース使用状況')
    # 使用しているリソースを合計
    table = []
    for i in range(len(nodes)):
        sum = 0.0
        for j in range(len(replica_sets)):
            sum = sum + replica_sets[j]['cpu'] * result[i][j]
        table.append([nodes[i]['name'], sum, nodes[i]['cpu']])
    node_headers = ['name', 'used', 'total']
    display(HTML(tabulate.tabulate(table, node_headers, tablefmt='html')))

else:
    print('解なし')
```

## 計算結果

こんな感じでどのノードにどのPodをいくつ配置すると良いかが出力されます。
![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/376039/af16cda7-dce3-2d41-5ddc-c04f7415164e.png)

## 参考

* https://speakerdeck.com/ytaka23/cicd-conference-2021
* https://qiita.com/fuloru169/items/de8c53402f4998177dfd