注：中文非直接翻译英文，而是理解加工后的笔记，记录英文仅仅是记其专业表述。

SP-SAT Solver

CP-SAT求解器技术上优于传统CP求解器。

The CP-SAT solver is technologically superior to the original CP solver and should be preferred in almost all situations.

为了增加运算速度，CP求解器处理的都是整数。

如果有非整数项约束，可以先将其乘一个整数，使其变成整数项。

If you begin with a problem that has constraints with non-integer terms, you need to first multiply those constraints by a sufficiently large integer so that all terms are integers

来看一个简单例子：寻找可行解。

• 变量x，y，z，每个只能取值0，1，2。
• 约束条件：x ≠ y

核心步骤：

• 声明模型
• 创建变量
• 创建约束条件
• 调用求解器
• 展示结果

from ortools.sat.python import cp_model


def SimpleSatProgram():
    """Minimal CP-SAT example to showcase calling the solver."""
    # Creates the model.
    model = cp_model.CpModel()

    # Creates the variables.
    num_vals = 3
    x = model.NewIntVar(0, num_vals - 1, 'x')
    y = model.NewIntVar(0, num_vals - 1, 'y')
    z = model.NewIntVar(0, num_vals - 1, 'z')

    # Creates the constraints.
    model.Add(x != y)

    # Creates a solver and solves the model.
    solver = cp_model.CpSolver()
    status = solver.Solve(model)

    if status == cp_model.FEASIBLE:
        print('x = %i' % solver.Value(x))
        print('y = %i' % solver.Value(y))
        print('z = %i' % solver.Value(z))

SimpleSatProgram()