CP-SAT সমাধানকারী

OR-Tools পূর্ণসংখ্যা প্রোগ্রামিং সমস্যা সমাধানের জন্য দুটি প্রধান টুল অফার করে:

• MPSolver , পূর্ববর্তী বিভাগে বর্ণিত।
• CP-SAT সমাধানকারী, যা আমরা পরবর্তী বর্ণনা করব।

একটি উদাহরণের জন্য যা CP-SAT সমাধানকারী এবং MPSolver র‍্যাপার উভয় ব্যবহার করে একটি পূর্ণসংখ্যা প্রোগ্রামিং সমস্যা সমাধান করে, একটি অ্যাসাইনমেন্ট সমস্যা সমাধান দেখুন।

দ্রষ্টব্য: গণনাগত গতি বাড়াতে, CP-SAT সমাধানকারী পূর্ণসংখ্যার উপর কাজ করে। এর মানে হল আপনি শুধুমাত্র পূর্ণসংখ্যা ব্যবহার করে আপনার অপ্টিমাইজেশন সমস্যা সংজ্ঞায়িত করতে হবে। আপনি যদি অ-পূর্ণসংখ্যা পদগুলির সাথে সীমাবদ্ধতা আছে এমন একটি সমস্যা দিয়ে শুরু করেন, তাহলে আপনাকে প্রথমে সেই সীমাবদ্ধতাগুলিকে যথেষ্ট বড় পূর্ণসংখ্যা দ্বারা গুণ করতে হবে যাতে সমস্ত পদ পূর্ণসংখ্যা হয়। একটি উদাহরণের জন্য একটি অপ্টিমাইজেশন সমস্যা সমাধান দেখুন।

নিম্নলিখিত বিভাগগুলি উদাহরণ উপস্থাপন করে যা দেখায় কিভাবে CP-SAT সমাধানকারী ব্যবহার করতে হয়।

উদাহরণ: একটি সম্ভাব্য সমাধান খোঁজা

আসুন একটি সাধারণ উদাহরণ দিয়ে শুরু করা যাক সমস্যা যেখানে আছে:

• তিনটি ভেরিয়েবল, x, y, এবং z, যার প্রতিটি মান নিতে পারে: 0, 1, বা 2।
• একটি সীমাবদ্ধতা: x != y

সমস্ত সমর্থিত ভাষায় একটি একক সম্ভাব্য সমাধান খুঁজতে CP-SAT সমাধানকারী কীভাবে ব্যবহার করবেন তা দেখানোর মাধ্যমে আমরা শুরু করব। যদিও এই ক্ষেত্রে একটি সম্ভাব্য সমাধান খুঁজে পাওয়া তুচ্ছ, আরও জটিল সীমাবদ্ধতা প্রোগ্রামিং সমস্যায় একটি সম্ভাব্য সমাধান আছে কিনা তা নির্ধারণ করা খুব কঠিন হতে পারে।

একটি CP সমস্যার একটি সর্বোত্তম সমাধান খোঁজার উদাহরণের জন্য, একটি অপ্টিমাইজেশান সমস্যা সমাধান দেখুন।

লাইব্রেরি আমদানি করুন

নিম্নলিখিত কোড প্রয়োজনীয় লাইব্রেরি আমদানি করে।

পাইথন

from ortools.sat.python import cp_model

সি++

#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"

জাভা

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;

সি#

using System;
using Google.OrTools.Sat;

মডেল ঘোষণা করুন

নিম্নলিখিত কোডটি CP-SAT মডেল ঘোষণা করে।

পাইথন

model = cp_model.CpModel()

সি++

CpModelBuilder cp_model;

জাভা

CpModel model = new CpModel();

সি#

CpModel model = new CpModel();

ভেরিয়েবল তৈরি করুন

নিম্নলিখিত কোডটি সমস্যার জন্য ভেরিয়েবল তৈরি করে।

পাইথন

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")

সি++

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");

জাভা

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");

সি#

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");

সমাধানকারী তিনটি ভেরিয়েবল তৈরি করে, x, y, এবং z, যার প্রতিটি মান 0, 1, বা 2 নিতে পারে।

সীমাবদ্ধতা তৈরি করুন

নিচের কোডটি x != y সীমাবদ্ধতা তৈরি করে।

পাইথন

model.add(x != y)

সি++

cp_model.AddNotEqual(x, y);

জাভা

model.addDifferent(x, y);

সি#

model.Add(x != y);

সমাধানকারীকে কল করুন

নিম্নলিখিত কোড সমাধানকারী কল.

পাইথন

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

সি++

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

জাভা

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

সি#

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

CP-SAT রিটার্ন মান

CP-SAT সমাধানকারী নীচের টেবিলে দেখানো স্ট্যাটাস মানগুলির একটি প্রদান করে। এই উদাহরণে, প্রত্যাবর্তিত মানটি হল OPTIMAL ।

স্ট্যাটাস	বর্ণনা
OPTIMAL	একটি সর্বোত্তম সম্ভাব্য সমাধান পাওয়া গেছে।
FEASIBLE	একটি সম্ভাব্য সমাধান পাওয়া গেছে, কিন্তু আমরা জানি না এটি সর্বোত্তম কিনা।
INFEASIBLE	সমস্যাটি অসম্ভাব্য প্রমাণিত হয়েছিল।
MODEL_INVALID	প্রদত্ত CpModelProto যাচাইকরণের ধাপটি পাস করেনি। আপনি ValidateCpModel(model_proto) এ কল করে একটি বিস্তারিত ত্রুটি পেতে পারেন।
UNKNOWN	মডেলটির স্থিতি অজানা কারণ কোনো সমাধান খুঁজে পাওয়া যায়নি (বা সমস্যাটি অসম্ভব বলে প্রমাণিত হয়নি) কোনো কিছুর আগে সমাধানকারীকে থামিয়ে দেয়, যেমন একটি সময়সীমা , একটি মেমরি সীমা বা ব্যবহারকারীর দ্বারা সেট করা একটি কাস্টম সীমা।

এগুলি cp_model.proto এ সংজ্ঞায়িত করা হয়েছে।

প্রথম সমাধান প্রদর্শন করুন

নিম্নলিখিত কোডটি সমাধানকারীর দ্বারা পাওয়া প্রথম সম্ভাব্য সমাধান প্রদর্শন করে। নোট করুন যে কোডটি status মানটি FEASIBLE বা OPTIMAL কিনা তা পরীক্ষা করে।

পাইথন

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.")

সি++

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.";
}

জাভা

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.");
}

সি#

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

সম্পূর্ণ প্রোগ্রাম

সম্পূর্ণ প্রোগ্রাম নীচে দেখানো হয়.

পাইথন

"""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()

সি++

#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;
}

জাভা

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() {}
}

সি#

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.");
        }
    }
}

সব সমাধান খোঁজা

এর পরে, আমরা সমস্ত সম্ভাব্য সমাধান খুঁজে পেতে উপরের প্রোগ্রামটিকে কীভাবে পরিবর্তন করতে হয় তা দেখাব।

প্রোগ্রামের প্রধান সংযোজন হল একটি সমাধান প্রিন্টার একটি কলব্যাক যা আপনি সমাধানকারীর কাছে পাস করেন, যা প্রতিটি সমাধান যেমন পাওয়া যায় তা প্রদর্শন করে।

সমাধান প্রিন্টার যোগ করুন

নিম্নলিখিত কোড সমাধান প্রিন্টার তৈরি করে।

পাইথন

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

সি++

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++;
}));

জাভা

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 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_;
}

সমাধানকারীকে কল করুন

নিম্নলিখিত কোডটি সমাধানকারীকে কল করে এবং এটিতে সমাধান প্রিন্টারটি পাস করে।

পাইথন

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)

সি++

SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &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);

সি#

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

সম্পূর্ণ প্রোগ্রাম

সম্পূর্ণ প্রোগ্রাম নীচে দেখানো হয়.

পাইথন

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()

সি++

#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;
}

জাভা

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.");
  }
}

সি#

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()}");
    }
}