เครื่องมือแก้ปัญหา CP-SAT

OR-Tools มีเครื่องมือหลัก 2 อย่างสำหรับการแก้ปัญหาการเขียนโปรแกรมจำนวนเต็ม

• MPSolver ตามที่อธิบายไว้ในส่วนก่อนหน้า
• เครื่องมือแก้โจทย์ CP-SAT ซึ่งเราจะอธิบายในลำดับถัดไป

ตัวอย่างที่ช่วยแก้ปัญหาการเขียนโปรแกรมด้วยจำนวนเต็มโดยใช้ทั้ง CP-SAT เครื่องมือแก้โจทย์และ MPSolver Wrapper โปรดดู การแก้ปัญหาด้านงาน

หมายเหตุ: เครื่องมือแก้โจทย์ CP-SAT จะทำงานกับจำนวนเต็มเพื่อเพิ่มความเร็วในการประมวลผล ซึ่งหมายความว่าคุณต้องกำหนดปัญหาการเพิ่มประสิทธิภาพโดยใช้จำนวนเต็มเท่านั้น ถ้าคุณเริ่มต้นด้วยโจทย์ที่จำกัดด้วยพจน์ที่ไม่ใช่จำนวนเต็ม จะต้องคูณข้อจำกัดเหล่านั้นด้วยจำนวนเต็มที่ใหญ่เพียงพอก่อน ทุกคำเป็นจำนวนเต็ม โปรดดู ตัวอย่างการแก้ปัญหาเกี่ยวกับการเพิ่มประสิทธิภาพ

ส่วนต่อไปนี้จะแสดงตัวอย่างที่แสดงวิธีใช้เครื่องมือแก้โจทย์ CP-SAT

ตัวอย่าง: การค้นหาโซลูชันที่เป็นไปได้

เรามาเริ่มด้วยตัวอย่างปัญหาง่ายๆ ที่มี

• ตัวแปร 3 ตัว ได้แก่ x, y และ z แต่ละตัวจะมีค่าเป็น 0, 1 หรือ 2
• ข้อจำกัด 1 ข้อ: x != y

เราจะเริ่มต้นด้วยการแสดงวิธีใช้เครื่องมือแก้โจทย์ CP-SAT เพื่อหา ในทุกภาษาที่รองรับ การหาวิธีแก้ปัญหาที่เป็นไปได้คือ ในกรณีนี้ อาจมีความซับซ้อนสำหรับโจทย์โปรแกรมจำกัด เป็นเรื่องที่ยากมากที่จะพิจารณาว่ามีวิธีแก้ปัญหาที่เป็นไปได้หรือไม่

ดูตัวอย่างของการค้นหาวิธีการแก้ปัญหา CP ที่เหมาะสมที่สุด โปรดดู การแก้ไขปัญหาการเพิ่มประสิทธิภาพ

นำเข้าไลบรารี

โค้ดต่อไปนี้จะนำเข้าไลบรารีที่จำเป็น

Python

from ortools.sat.python import cp_model

C++

#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/util/sorted_interval_list.h"

Java

import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;

C#

using System;
using Google.OrTools.Sat;

ประกาศโมเดล

โค้ดต่อไปนี้แจ้งโมเดล CP-SAT

Python

model = cp_model.CpModel()

C++

CpModelBuilder cp_model;

Java

CpModel model = new CpModel();

C#

CpModel model = new CpModel();

สร้างตัวแปร

โค้ดต่อไปนี้จะสร้างตัวแปรของโจทย์

Python

num_vals = 3
x = model.new_int_var(0, num_vals - 1, "x")
y = model.new_int_var(0, num_vals - 1, "y")
z = model.new_int_var(0, num_vals - 1, "z")

C++

const Domain domain(0, 2);
const IntVar x = cp_model.NewIntVar(domain).WithName("x");
const IntVar y = cp_model.NewIntVar(domain).WithName("y");
const IntVar z = cp_model.NewIntVar(domain).WithName("z");

Java

int numVals = 3;

IntVar x = model.newIntVar(0, numVals - 1, "x");
IntVar y = model.newIntVar(0, numVals - 1, "y");
IntVar z = model.newIntVar(0, numVals - 1, "z");

C#

int num_vals = 3;

IntVar x = model.NewIntVar(0, num_vals - 1, "x");
IntVar y = model.NewIntVar(0, num_vals - 1, "y");
IntVar z = model.NewIntVar(0, num_vals - 1, "z");

เครื่องมือแก้โจทย์สร้างตัวแปร 3 ตัว ได้แก่ x, y และ z โดยตัวแปรแต่ละตัวจะรับค่า ค่า 0, 1 หรือ 2

สร้างข้อจำกัด

โค้ดต่อไปนี้สร้างข้อจำกัด x != y

Python

model.add(x != y)

C++

cp_model.AddNotEqual(x, y);

Java

model.addDifferent(x, y);

C#

model.Add(x != y);

โทรหาเครื่องมือแก้โจทย์

โค้ดต่อไปนี้เรียกใช้เครื่องมือแก้โจทย์

Python

solver = cp_model.CpSolver()
status = solver.solve(model)

C++

const CpSolverResponse response = Solve(cp_model.Build());

Java

CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);

C#

CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);

ค่าผลลัพธ์ CP-SAT

เครื่องมือแก้โจทย์ CP-SAT จะแสดงค่าสถานะค่าใดค่าหนึ่งที่แสดงในตารางด้านล่าง ใน ในตัวอย่างนี้ ค่าที่แสดงผลคือ OPTIMAL

สถานะ	คำอธิบาย
OPTIMAL	พบโซลูชันที่เหมาะสมแล้ว
FEASIBLE	พบวิธีแก้ปัญหาที่เป็นไปได้แล้ว แต่เราไม่ทราบว่าจะเหมาะสมที่สุดหรือไม่
INFEASIBLE	มีการพิสูจน์แล้วว่าปัญหานี้เป็นไปไม่ได้
MODEL_INVALID	CpModelProto ที่ระบุไม่ผ่านขั้นตอนการตรวจสอบ คุณสามารถ โดยละเอียดเมื่อโทรหา ValidateCpModel(model_proto)
UNKNOWN	ไม่ทราบสถานะของโมเดลเนื่องจากไม่พบวิธีแก้โจทย์ (หรือ ไม่ได้รับการพิสูจน์ว่า INFEASIBLE) ก่อนที่จะมีบางอย่างทำให้เครื่องมือแก้โจทย์ เช่น การจำกัดเวลา ขีดจำกัดหน่วยความจำ หรือขีดจำกัดที่กำหนดเองที่ผู้ใช้กำหนดไว้

ซึ่งมีคำจำกัดความใน cp_model.proto.

แสดงโซลูชันแรก

โค้ดต่อไปนี้แสดงโซลูชันแรกที่เป็นไปได้ซึ่งโปรแกรมแก้โจทย์พบ โปรดทราบว่าโค้ดจะตรวจสอบว่าค่าของ status เป็น FEASIBLE หรือ OPTIMAL

Python

if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print(f"x = {solver.value(x)}")
    print(f"y = {solver.value(y)}")
    print(f"z = {solver.value(z)}")
else:
    print("No solution found.")

C++

if (response.status() == CpSolverStatus::OPTIMAL ||
    response.status() == CpSolverStatus::FEASIBLE) {
  // Get the value of x in the solution.
  LOG(INFO) << "x = " << SolutionIntegerValue(response, x);
  LOG(INFO) << "y = " << SolutionIntegerValue(response, y);
  LOG(INFO) << "z = " << SolutionIntegerValue(response, z);
} else {
  LOG(INFO) << "No solution found.";
}

Java

if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
  System.out.println("x = " + solver.value(x));
  System.out.println("y = " + solver.value(y));
  System.out.println("z = " + solver.value(z));
} else {
  System.out.println("No solution found.");
}

C#

if (status == CpSolverStatus.Optimal || status == CpSolverStatus.Feasible)
{
    Console.WriteLine("x = " + solver.Value(x));
    Console.WriteLine("y = " + solver.Value(y));
    Console.WriteLine("z = " + solver.Value(z));
}
else
{
    Console.WriteLine("No solution found.");
}

เรียกใช้โปรแกรม

รายการที่สมบูรณ์จะแสดงในส่วนถัดไป เมื่อคุณเรียกใช้โปรแกรม ระบบจะแสดงคำตอบแรกที่โปรแกรมแก้โจทย์พบ ดังนี้

x = 1
y = 0
z = 0

จบโปรแกรม

โปรแกรมทั้งหมดจะแสดงอยู่ด้านล่าง

Python

"""Simple solve."""
from ortools.sat.python import cp_model


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

    # Creates the variables.
    num_vals = 3
    x = model.new_int_var(0, num_vals - 1, "x")
    y = model.new_int_var(0, num_vals - 1, "y")
    z = model.new_int_var(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.OPTIMAL or status == cp_model.FEASIBLE:
        print(f"x = {solver.value(x)}")
        print(f"y = {solver.value(y)}")
        print(f"z = {solver.value(z)}")
    else:
        print("No solution found.")


simple_sat_program()

C++

#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/util/sorted_interval_list.h"

namespace operations_research {
namespace sat {

void SimpleSatProgram() {
  CpModelBuilder cp_model;

  const Domain domain(0, 2);
  const IntVar x = cp_model.NewIntVar(domain).WithName("x");
  const IntVar y = cp_model.NewIntVar(domain).WithName("y");
  const IntVar z = cp_model.NewIntVar(domain).WithName("z");

  cp_model.AddNotEqual(x, y);

  // Solving part.
  const CpSolverResponse response = Solve(cp_model.Build());

  if (response.status() == CpSolverStatus::OPTIMAL ||
      response.status() == CpSolverStatus::FEASIBLE) {
    // Get the value of x in the solution.
    LOG(INFO) << "x = " << SolutionIntegerValue(response, x);
    LOG(INFO) << "y = " << SolutionIntegerValue(response, y);
    LOG(INFO) << "z = " << SolutionIntegerValue(response, z);
  } else {
    LOG(INFO) << "No solution found.";
  }
}

}  // namespace sat
}  // namespace operations_research

int main() {
  operations_research::sat::SimpleSatProgram();
  return EXIT_SUCCESS;
}

Java

package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;

/** Minimal CP-SAT example to showcase calling the solver. */
public final class SimpleSatProgram {
  public static void main(String[] args) throws Exception {
    Loader.loadNativeLibraries();
    // Create the model.
    CpModel model = new CpModel();

    // Create the variables.
    int numVals = 3;

    IntVar x = model.newIntVar(0, numVals - 1, "x");
    IntVar y = model.newIntVar(0, numVals - 1, "y");
    IntVar z = model.newIntVar(0, numVals - 1, "z");

    // Create the constraints.
    model.addDifferent(x, y);

    // Create a solver and solve the model.
    CpSolver solver = new CpSolver();
    CpSolverStatus status = solver.solve(model);

    if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
      System.out.println("x = " + solver.value(x));
      System.out.println("y = " + solver.value(y));
      System.out.println("z = " + solver.value(z));
    } else {
      System.out.println("No solution found.");
    }
  }

  private SimpleSatProgram() {}
}

C#

using System;
using Google.OrTools.Sat;

public class SimpleSatProgram
{
    static void Main()
    {
        // Creates the model.
        CpModel model = new CpModel();

        // Creates the variables.
        int num_vals = 3;

        IntVar x = model.NewIntVar(0, num_vals - 1, "x");
        IntVar y = model.NewIntVar(0, num_vals - 1, "y");
        IntVar z = model.NewIntVar(0, num_vals - 1, "z");

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

        // Creates a solver and solves the model.
        CpSolver solver = new CpSolver();
        CpSolverStatus status = solver.Solve(model);

        if (status == CpSolverStatus.Optimal || status == CpSolverStatus.Feasible)
        {
            Console.WriteLine("x = " + solver.Value(x));
            Console.WriteLine("y = " + solver.Value(y));
            Console.WriteLine("z = " + solver.Value(z));
        }
        else
        {
            Console.WriteLine("No solution found.");
        }
    }
}

กำลังค้นหาวิธีแก้โจทย์ทั้งหมด

ต่อไป เราจะแสดงวิธีแก้ไขโปรแกรมด้านบนเพื่อค้นหา โซลูชันที่เป็นไปได้ทั้งหมด

ส่วนเพิ่มเติมหลักของโปรแกรมคือเครื่องพิมพ์โซลูชัน Callback ที่คุณ ไปยังเครื่องมือแก้โจทย์ ซึ่งแสดงเฉลยแต่ละวิธีที่พบ

เพิ่มเครื่องพิมพ์โซลูชัน

โค้ดต่อไปนี้จะสร้างเครื่องพิมพ์โซลูชัน

Python

class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
    """Print intermediate solutions."""

    def __init__(self, variables: list[cp_model.IntVar]):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self.__variables = variables
        self.__solution_count = 0

    def on_solution_callback(self) -> None:
        self.__solution_count += 1
        for v in self.__variables:
            print(f"{v}={self.value(v)}", end=" ")
        print()

    @property
    def solution_count(self) -> int:
        return self.__solution_count

C++

Model model;

int num_solutions = 0;
model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
  LOG(INFO) << "Solution " << num_solutions;
  LOG(INFO) << "  x = " << SolutionIntegerValue(r, x);
  LOG(INFO) << "  y = " << SolutionIntegerValue(r, y);
  LOG(INFO) << "  z = " << SolutionIntegerValue(r, z);
  num_solutions++;
}));

Java

static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
  public VarArraySolutionPrinter(IntVar[] variables) {
    variableArray = variables;
  }

  @Override
  public void onSolutionCallback() {
    System.out.printf("Solution #%d: time = %.02f s%n", solutionCount, wallTime());
    for (IntVar v : variableArray) {
      System.out.printf("  %s = %d%n", v.getName(), value(v));
    }
    solutionCount++;
  }

  public int getSolutionCount() {
    return solutionCount;
  }

  private int solutionCount;
  private final IntVar[] variableArray;
}

C#

public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
    public VarArraySolutionPrinter(IntVar[] variables)
    {
        variables_ = variables;
    }

    public override void OnSolutionCallback()
    {
        {
            Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime()));
            foreach (IntVar v in variables_)
            {
                Console.WriteLine(String.Format("  {0} = {1}", v.ToString(), Value(v)));
            }
            solution_count_++;
        }
    }

    public int SolutionCount()
    {
        return solution_count_;
    }

    private int solution_count_;
    private IntVar[] variables_;
}

โทรหาเครื่องมือแก้โจทย์

โค้ดต่อไปนี้เรียกใช้ตัวแก้โจทย์ และส่งเครื่องพิมพ์ของโซลูชันไปให้

Python

solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter([x, y, z])
# Enumerate all solutions.
solver.parameters.enumerate_all_solutions = True
# Solve.
status = solver.solve(model, solution_printer)

C++

SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);

Java

CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z});
// Tell the solver to enumerate all solutions.
solver.getParameters().setEnumerateAllSolutions(true);
// And solve.
solver.solve(model, cb);

C#

CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z });
// Search for all solutions.
solver.StringParameters = "enumerate_all_solutions:true";
// And solve.
solver.Solve(model, cb);

เรียกใช้โปรแกรม

โปรแกรมฉบับเต็มจะแสดงในส่วนถัดไป เมื่อคุณเรียกใช้โปรแกรม โปรแกรมจะแสดงโซลูชันที่เป็นไปได้ทั้งหมด 18 วิธี

x=1 y=0 z=0
x=2 y=0 z=0
x=2 y=1 z=0
x=2 y=1 z=1
x=2 y=1 z=2
x=2 y=0 z=2
x=2 y=0 z=1
x=1 y=0 z=1
x=0 y=1 z=1
x=0 y=1 z=2
x=0 y=2 z=2
x=1 y=2 z=2
x=1 y=2 z=1
x=1 y=2 z=0
x=0 y=2 z=0
x=0 y=1 z=0
x=0 y=2 z=1
x=1 y=0 z=2
Status = FEASIBLE

จบโปรแกรม

โปรแกรมทั้งหมดจะแสดงอยู่ด้านล่าง

Python

from ortools.sat.python import cp_model


class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
    """Print intermediate solutions."""

    def __init__(self, variables: list[cp_model.IntVar]):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self.__variables = variables
        self.__solution_count = 0

    def on_solution_callback(self) -> None:
        self.__solution_count += 1
        for v in self.__variables:
            print(f"{v}={self.value(v)}", end=" ")
        print()

    @property
    def solution_count(self) -> int:
        return self.__solution_count


def search_for_all_solutions_sample_sat():
    """Showcases calling the solver to search for all solutions."""
    # Creates the model.
    model = cp_model.CpModel()

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

    # Create the constraints.
    model.add(x != y)

    # Create a solver and solve.
    solver = cp_model.CpSolver()
    solution_printer = VarArraySolutionPrinter([x, y, z])
    # Enumerate all solutions.
    solver.parameters.enumerate_all_solutions = True
    # Solve.
    status = solver.solve(model, solution_printer)

    print(f"Status = {solver.status_name(status)}")
    print(f"Number of solutions found: {solution_printer.solution_count}")


search_for_all_solutions_sample_sat()

C++

#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/sorted_interval_list.h"

namespace operations_research {
namespace sat {

void SearchAllSolutionsSampleSat() {
  CpModelBuilder cp_model;

  const Domain domain(0, 2);
  const IntVar x = cp_model.NewIntVar(domain).WithName("x");
  const IntVar y = cp_model.NewIntVar(domain).WithName("y");
  const IntVar z = cp_model.NewIntVar(domain).WithName("z");

  cp_model.AddNotEqual(x, y);

  Model model;

  int num_solutions = 0;
  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
    LOG(INFO) << "Solution " << num_solutions;
    LOG(INFO) << "  x = " << SolutionIntegerValue(r, x);
    LOG(INFO) << "  y = " << SolutionIntegerValue(r, y);
    LOG(INFO) << "  z = " << SolutionIntegerValue(r, z);
    num_solutions++;
  }));

  // Tell the solver to enumerate all solutions.
  SatParameters parameters;
  parameters.set_enumerate_all_solutions(true);
  model.Add(NewSatParameters(parameters));
  const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);

  LOG(INFO) << "Number of solutions found: " << num_solutions;
}

}  // namespace sat
}  // namespace operations_research

int main() {
  operations_research::sat::SearchAllSolutionsSampleSat();

  return EXIT_SUCCESS;
}

Java

package com.google.ortools.sat.samples;

import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
import com.google.ortools.sat.IntVar;

/** Code sample that solves a model and displays all solutions. */
public class SearchForAllSolutionsSampleSat {
  static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
    public VarArraySolutionPrinter(IntVar[] variables) {
      variableArray = variables;
    }

    @Override
    public void onSolutionCallback() {
      System.out.printf("Solution #%d: time = %.02f s%n", solutionCount, wallTime());
      for (IntVar v : variableArray) {
        System.out.printf("  %s = %d%n", v.getName(), value(v));
      }
      solutionCount++;
    }

    public int getSolutionCount() {
      return solutionCount;
    }

    private int solutionCount;
    private final IntVar[] variableArray;
  }

  public static void main(String[] args) throws Exception {
    Loader.loadNativeLibraries();
    // Create the model.
    CpModel model = new CpModel();

    // Create the variables.
    int numVals = 3;

    IntVar x = model.newIntVar(0, numVals - 1, "x");
    IntVar y = model.newIntVar(0, numVals - 1, "y");
    IntVar z = model.newIntVar(0, numVals - 1, "z");

    // Create the constraints.
    model.addDifferent(x, y);

    // Create a solver and solve the model.
    CpSolver solver = new CpSolver();
    VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z});
    // Tell the solver to enumerate all solutions.
    solver.getParameters().setEnumerateAllSolutions(true);
    // And solve.
    solver.solve(model, cb);

    System.out.println(cb.getSolutionCount() + " solutions found.");
  }
}

C#

using System;
using Google.OrTools.Sat;

public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
    public VarArraySolutionPrinter(IntVar[] variables)
    {
        variables_ = variables;
    }

    public override void OnSolutionCallback()
    {
        {
            Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime()));
            foreach (IntVar v in variables_)
            {
                Console.WriteLine(String.Format("  {0} = {1}", v.ToString(), Value(v)));
            }
            solution_count_++;
        }
    }

    public int SolutionCount()
    {
        return solution_count_;
    }

    private int solution_count_;
    private IntVar[] variables_;
}

public class SearchForAllSolutionsSampleSat
{
    static void Main()
    {
        // Creates the model.
        CpModel model = new CpModel();

        // Creates the variables.
        int num_vals = 3;

        IntVar x = model.NewIntVar(0, num_vals - 1, "x");
        IntVar y = model.NewIntVar(0, num_vals - 1, "y");
        IntVar z = model.NewIntVar(0, num_vals - 1, "z");

        // Adds a different constraint.
        model.Add(x != y);

        // Creates a solver and solves the model.
        CpSolver solver = new CpSolver();
        VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z });
        // Search for all solutions.
        solver.StringParameters = "enumerate_all_solutions:true";
        // And solve.
        solver.Solve(model, cb);

        Console.WriteLine($"Number of solutions found: {cb.SolutionCount()}");
    }
}