CP-SAT 솔버

OR-Tools는 정수 프로그래밍 문제를 해결하기 위한 두 가지 기본 도구를 제공합니다.

• MPSolver는 이전 섹션에서 설명한 것입니다.
• CP-SAT 솔버입니다. 다음에 설명하겠습니다.

CP-SAT 솔버와 MPSolver 래퍼를 모두 사용하여 정수 프로그래밍 문제를 해결하는 예는 할당 문제 해결을 참고하세요.

참고: 연산 속도를 높이기 위해 CP-SAT 솔버는 정수에 대해 작업을 수행합니다. 즉, 정수만 사용하여 최적화 문제를 정의해야 합니다. 정수가 아닌 항이 포함된 제약 조건이 있는 문제를 시작하는 경우 먼저 모든 항이 정수가 되도록 이 제약조건에 충분히 큰 정수를 곱해야 합니다. 예를 보려면 최적화 문제 해결을 참고하세요.

다음 섹션에는 CP-SAT 솔버를 사용하는 방법을 보여주는 예가 나와 있습니다.

예: 가능한 솔루션 찾기

간단한 문제 예시부터 시작해 보겠습니다.

• 0, 1, 2 값을 취할 수 있는 3개의 변수 x, y, z.
• 제약조건 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");

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

모든 솔루션을 찾는 중

이제 위의 프로그램을 수정하여 가능한 모든 솔루션을 찾는 방법을 보여줍니다.

프로그램의 주요 추가 사항은 솔루션 프린터입니다. 해결사에 전달하는 콜백은 발견된 각 솔루션을 표시합니다.

솔루션 프린터 추가

다음 코드는 솔루션 프린터를 만듭니다.

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