test.py

from __future__ import absolute_import
from __future__ import division
from __future__ import print_function

from ortools.sat.python import cp_model


def sat_test():
    # Creates the model
    model = cp_model.CpModel()

    # Creates the variables.
    num_vals = 4
    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 != 0)
    model.Add(y != 0)
    model.Add(x != y)
    aux_vars = [x, y]
    model.Add(cp_model.LinearExpr.Sum(aux_vars) == z)
    # Creates a solver and solves the model.
    solver = cp_model.CpSolver()
    status = solver.Solve(model)

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