CpSolver.java

Go to the documentation of this file.

// Copyright 2010-2021 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
 
package com.google.ortools.sat;
 
import com.google.ortools.sat.CpSolverResponse;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.SatParameters;
import java.util.List;
import java.util.function.Consumer;
 
public final class CpSolver {
  public CpSolver() {
    this.solveParameters = SatParameters.newBuilder();
    this.logCallback = null;
    this.solveWrapper = null;
  }
 
  public CpSolverStatus solve(CpModel model) {
    return solveWithSolutionCallback(model, null);
  }
 
  public CpSolverStatus solveWithSolutionCallback(CpModel model, CpSolverSolutionCallback cb) {
    // Setup search.
    createSolveWrapper(); // Synchronized.
    solveWrapper.setParameters(solveParameters.build());
    if (cb != null) {
      solveWrapper.addSolutionCallback(cb);
    }
    if (logCallback != null) {
      solveWrapper.addLogCallback(logCallback);
    }
 
    solveResponse = solveWrapper.solve(model.model());
 
    // Cleanup search.
    if (cb != null) {
      solveWrapper.clearSolutionCallback(cb);
    }
    releaseSolveWrapper(); // Synchronized.
 
    return solveResponse.getStatus();
  }
 
  public CpSolverStatus searchAllSolutions(CpModel model, CpSolverSolutionCallback cb) {
    boolean oldValue = solveParameters.getEnumerateAllSolutions();
    solveParameters.setEnumerateAllSolutions(true);
    solveWithSolutionCallback(model, cb);
    solveParameters.setEnumerateAllSolutions(oldValue);
    return solveResponse.getStatus();
  }
 
  private synchronized void createSolveWrapper() {
    solveWrapper = new SolveWrapper();
  }
 
  private synchronized void releaseSolveWrapper() {
    solveWrapper = null;
  }
 
  public synchronized void stopSearch() {
    if (solveWrapper != null) {
      solveWrapper.stopSearch();
    }
  }
 
  public double objectiveValue() {
    return solveResponse.getObjectiveValue();
  }
 
  public double bestObjectiveBound() {
    return solveResponse.getBestObjectiveBound();
  }
 
  public long value(IntVar var) {
    return solveResponse.getSolution(var.getIndex());
  }
 
  public Boolean booleanValue(Literal var) {
    int index = var.getIndex();
    if (index >= 0) {
      return solveResponse.getSolution(index) != 0;
    } else {
      return solveResponse.getSolution(-index - 1) == 0;
    }
  }
 
  public CpSolverResponse response() {
    return solveResponse;
  }
 
  public long numBranches() {
    return solveResponse.getNumBranches();
  }
 
  public long numConflicts() {
    return solveResponse.getNumConflicts();
  }
 
  public double wallTime() {
    return solveResponse.getWallTime();
  }
 
  public double userTime() {
    return solveResponse.getUserTime();
  }
 
  public List<Integer> sufficientAssumptionsForInfeasibility() {
    return solveResponse.getSufficientAssumptionsForInfeasibilityList();
  }
 
  public SatParameters.Builder getParameters() {
    return solveParameters;
  }
 
  public void setLogCallback(Consumer<String> cb) {
    this.logCallback = cb;
  }
 
  public String responseStats() {
    return CpSatHelper.solverResponseStats(solveResponse);
  }
 
  private CpSolverResponse solveResponse;
  private final SatParameters.Builder solveParameters;
  private Consumer<String> logCallback;
  private SolveWrapper solveWrapper;
}