Java Reference

Java Reference

CpSolver.java
Go to the documentation of this file.
1 // Copyright 2010-2022 Google LLC
2 // Licensed under the Apache License, Version 2.0 (the "License");
3 // you may not use this file except in compliance with the License.
4 // You may obtain a copy of the License at
5 //
6 // http://www.apache.org/licenses/LICENSE-2.0
7 //
8 // Unless required by applicable law or agreed to in writing, software
9 // distributed under the License is distributed on an "AS IS" BASIS,
10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11 // See the License for the specific language governing permissions and
12 // limitations under the License.
13 
14 package com.google.ortools.sat;
15 
16 import com.google.ortools.sat.CpSolverResponse;
17 import com.google.ortools.sat.CpSolverStatus;
18 import com.google.ortools.sat.SatParameters;
19 import java.util.List;
20 import java.util.function.Consumer;
21 
28 public final class CpSolver {
30  public CpSolver() {
31  this.solveParameters = SatParameters.newBuilder();
32  this.logCallback = null;
33  this.solveWrapper = null;
34  }
35 
37  public CpSolverStatus solve(CpModel model) {
38  return solveWithSolutionCallback(model, null);
39  }
40 
45  public CpSolverStatus solve(CpModel model, CpSolverSolutionCallback cb) {
46  // Setup search.
47  createSolveWrapper(); // Synchronized.
48  solveWrapper.setParameters(solveParameters.build());
49  if (cb != null) {
50  solveWrapper.addSolutionCallback(cb);
51  }
52  if (logCallback != null) {
53  solveWrapper.addLogCallback(logCallback);
54  }
55 
56  solveResponse = solveWrapper.solve(model.model());
57 
58  // Cleanup search.
59  if (cb != null) {
60  solveWrapper.clearSolutionCallback(cb);
61  }
62  releaseSolveWrapper(); // Synchronized.
63 
64  return solveResponse.getStatus();
65  }
66 
73  @Deprecated
74  public CpSolverStatus solveWithSolutionCallback(CpModel model, CpSolverSolutionCallback cb) {
75  return solve(model, cb);
76  }
77 
92  @Deprecated
93  public CpSolverStatus searchAllSolutions(CpModel model, CpSolverSolutionCallback cb) {
94  boolean oldValue = solveParameters.getEnumerateAllSolutions();
95  solveParameters.setEnumerateAllSolutions(true);
96  solve(model, cb);
97  solveParameters.setEnumerateAllSolutions(oldValue);
98  return solveResponse.getStatus();
99  }
100 
101  private synchronized void createSolveWrapper() {
102  solveWrapper = new SolveWrapper();
103  }
104 
105  private synchronized void releaseSolveWrapper() {
106  solveWrapper = null;
107  }
108 
110  public synchronized void stopSearch() {
111  if (solveWrapper != null) {
112  solveWrapper.stopSearch();
113  }
114  }
115 
117  public double objectiveValue() {
118  return solveResponse.getObjectiveValue();
119  }
120 
125  public double bestObjectiveBound() {
126  return solveResponse.getBestObjectiveBound();
127  }
128 
130  public long value(LinearArgument expr) {
131  final LinearExpr e = expr.build();
132  long result = e.getOffset();
133  for (int i = 0; i < e.numElements(); ++i) {
134  result += solveResponse.getSolution(e.getVariableIndex(i)) * e.getCoefficient(i);
135  }
136  return result;
137  }
138 
140  public Boolean booleanValue(Literal var) {
141  int index = var.getIndex();
142  if (index >= 0) {
143  return solveResponse.getSolution(index) != 0;
144  } else {
145  return solveResponse.getSolution(-index - 1) == 0;
146  }
147  }
148 
150  public CpSolverResponse response() {
151  return solveResponse;
152  }
153 
155  public long numBranches() {
156  return solveResponse.getNumBranches();
157  }
158 
160  public long numConflicts() {
161  return solveResponse.getNumConflicts();
162  }
163 
165  public double wallTime() {
166  return solveResponse.getWallTime();
167  }
168 
170  public double userTime() {
171  return solveResponse.getUserTime();
172  }
173 
174  public List<Integer> sufficientAssumptionsForInfeasibility() {
175  return solveResponse.getSufficientAssumptionsForInfeasibilityList();
176  }
177 
179  public SatParameters.Builder getParameters() {
180  return solveParameters;
181  }
182 
184  public void setLogCallback(Consumer<String> cb) {
185  this.logCallback = cb;
186  }
187 
189  public String responseStats() {
190  return CpSatHelper.solverResponseStats(solveResponse);
191  }
192 
197  public String getSolutionInfo() {
198  return solveResponse.getSolutionInfo();
199  }
200 
201  private CpSolverResponse solveResponse;
202  private final SatParameters.Builder solveParameters;
203  private Consumer<String> logCallback;
204  private SolveWrapper solveWrapper;
205 }
Main modeling class.
Definition: CpModel.java:42
Parent class to create a callback called at each solution.
Wrapper around the SAT solver.
Definition: CpSolver.java:28
CpSolver()
Main construction of the CpSolver class.
Definition: CpSolver.java:30
double objectiveValue()
Returns the best objective value found during search.
Definition: CpSolver.java:117
double userTime()
Returns the user time of the search.
Definition: CpSolver.java:170
long value(LinearArgument expr)
Returns the value of a linear expression in the last solution found.
Definition: CpSolver.java:130
double wallTime()
Returns the wall time of the search.
Definition: CpSolver.java:165
CpSolverStatus solve(CpModel model, CpSolverSolutionCallback cb)
Solves the given model, calls the solution callback at each incumbent solution, and returns the solve...
Definition: CpSolver.java:45
double bestObjectiveBound()
Returns the best lower bound found when minimizing, of the best upper bound found when maximizing.
Definition: CpSolver.java:125
CpSolverResponse response()
Returns the internal response protobuf that is returned internally by the SAT solver.
Definition: CpSolver.java:150
CpSolverStatus solveWithSolutionCallback(CpModel model, CpSolverSolutionCallback cb)
Solves the given model, passes each incumber solution to the solution callback if not null,...
Definition: CpSolver.java:74
long numBranches()
Returns the number of branches explored during search.
Definition: CpSolver.java:155
List< Integer > sufficientAssumptionsForInfeasibility()
Definition: CpSolver.java:174
CpSolverStatus searchAllSolutions(CpModel model, CpSolverSolutionCallback cb)
Searches for all solutions of a satisfiability problem.
Definition: CpSolver.java:93
CpSolverStatus solve(CpModel model)
Solves the given model, and returns the solve status.
Definition: CpSolver.java:37
long numConflicts()
Returns the number of conflicts created during search.
Definition: CpSolver.java:160
String getSolutionInfo()
Returns some information on how the solution was found, or the reason why the model or the parameters...
Definition: CpSolver.java:197
SatParameters.Builder getParameters()
Returns the builder of the parameters of the SAT solver for modification.
Definition: CpSolver.java:179
void setLogCallback(Consumer< String > cb)
Sets the log callback for the solver.
Definition: CpSolver.java:184
synchronized void stopSearch()
Stops the search asynchronously.
Definition: CpSolver.java:110
Boolean booleanValue(Literal var)
Returns the Boolean value of a literal in the last solution found.
Definition: CpSolver.java:140
String responseStats()
Returns some statistics on the solution found as a string.
Definition: CpSolver.java:189
A object that can build a LinearExpr object.
LinearExpr build()
Builds a linear expression.
A linear expression (sum (ai * xi) + b).
long getCoefficient(int index)
Returns the ith coefficient.
int numElements()
Returns the number of terms (excluding the constant one) in this expression.
long getOffset()
Returns the constant part of the expression.
int getVariableIndex(int index)
Returns the index of the ith variable.
Interface to describe a boolean variable or its negation.
Definition: Literal.java:17