CP-SAT-Solver

OR-Tools bietet zwei Haupttools zur Lösung von Ganzzahlen-Programmierproblemen:

  • MPSolver in einem vorherigen Abschnitt beschrieben.
  • Der CP-SAT-Rechner, den wir als Nächstes beschreiben.

Ein Beispiel, das ein Ganzzahl-Programmierproblem mithilfe des CP-SAT-Resolvers und des MPsolver-Wrappers löst, finden Sie unter Zuweisungsproblem lösen.

In den folgenden Abschnitten finden Sie Beispiele für die Verwendung des CP-SAT-Behebers.

Beispiel: Suche nach einer praktikablen Lösung

Beginnen wir mit einem einfachen Beispielproblem, in dem es Folgendes gibt:

  • Die drei Variablen x, y und z, von denen jede die Werte annehmen kann: 0, 1 oder 2.
  • Eine Einschränkung: x != y

Zunächst zeigen wir, wie Sie mit dem CP-SAT-Rechner eine einzige durchführbare Lösung in allen unterstützten Sprachen finden. Während die Suche nach einer durchführbaren Lösung in diesem Fall trivial ist, kann es bei komplexeren Problemen mit der Programmierung von Einschränkungen schwierig sein zu bestimmen, ob es eine praktikable Lösung gibt.

Ein Beispiel für die Suche nach einer optimalen Lösung für ein CP-Problem finden Sie unter Optimierungsproblem lösen.

Bibliotheken importieren

Mit dem folgenden Code wird die erforderliche Bibliothek importiert.

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;

Modell deklarieren

Mit dem folgenden Code wird das CP-SAT-Modell deklariert.

Python

model = cp_model.CpModel()

C++

CpModelBuilder cp_model;

Java

CpModel model = new CpModel();

C#

CpModel model = new CpModel();

Variablen erstellen

Mit dem folgenden Code werden die Variablen für das Problem erstellt.

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

Der Matherechner erstellt drei Variablen, x, y und z, die jeweils die Werte 0, 1 und 2 annehmen können.

Einschränkung erstellen

Mit dem folgenden Code wird die Einschränkung x != y erstellt.

Python

model.add(x != y)

C++

cp_model.AddNotEqual(x, y);

Java

model.addDifferent(x, y);

C#

model.Add(x != y);

Matherechner aufrufen

Mit dem folgenden Code wird der Solver aufgerufen.

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-Rückgabewerte

Der CP-SAT-Beheber gibt einen der Statuswerte aus der folgenden Tabelle zurück. In diesem Beispiel wird OPTIMAL zurückgegeben.

Status Beschreibung
OPTIMAL Es wurde eine optimale praktikable Lösung gefunden.
FEASIBLE Es wurde eine praktikable Lösung gefunden, aber wir wissen nicht, ob sie optimal ist.
INFEASIBLE Das Problem hat sich als nicht umsetzbar erwiesen.
MODEL_INVALID Das angegebene CpModelProto hat den Validierungsschritt nicht bestanden. Wenn Sie ValidateCpModel(model_proto) aufrufen, erhalten Sie einen detaillierten Fehler.
UNKNOWN Der Status des Modells ist unbekannt, da keine Lösung gefunden wurde (oder das Problem nicht nachgewiesen wurde, bevor der Solver beendet wurde), z. B. durch ein Zeitlimit, ein Speicherlimit oder ein vom Nutzer festgelegtes benutzerdefiniertes Limit.

Diese sind in cp_model.proto definiert.

Erste Lösung anzeigen

Der folgende Code zeigt die erste durchführbare Lösung an, die vom Matherechner gefunden wurde. Mit dem Code wird geprüft, ob der Wert von status FEASIBLE oder OPTIMAL ist.

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

Programm ausführen

Die vollständigen Programme finden Sie im nächsten Abschnitt. Wenn Sie ein Programm ausführen, wird die erste vom Solver gefundene Lösung zurückgegeben:

x = 1
y = 0
z = 0

Abgeschlossene Programme

Die vollständigen Programme sind unten aufgeführt.

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

Alle Lösungen finden

Als Nächstes zeigen wir Ihnen, wie Sie das oben genannte Programm ändern, um alle praktikablen Lösungen zu finden.

Die wichtigste Ergänzung des Programms ist ein Lösungsdrucker, ein Callback, den Sie an den Matherechner übergeben, der jede gefundene Lösung anzeigt.

Lösungsdrucker hinzufügen

Mit dem folgenden Code wird der Lösungsdrucker erstellt.

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

Matherechner aufrufen

Mit dem folgenden Code wird der Solver aufgerufen und der Lösungsdrucker an ihn übergeben.

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

Programm ausführen

Das vollständige Programm sehen Sie im nächsten Abschnitt. Wenn Sie das Programm ausführen, werden alle 18 möglichen Lösungen angezeigt:

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

Abgeschlossene Programme

Die vollständigen Programme sind unten aufgeführt.

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