Java Reference

Java Reference

CpSolver.java
Go to the documentation of this file.
1// Copyright 2010-2021 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
14package com.google.ortools.sat;
15
16import com.google.ortools.sat.CpSolverResponse;
17import com.google.ortools.sat.CpSolverStatus;
18import com.google.ortools.sat.SatParameters;
19import java.util.List;
20import java.util.function.Consumer;
21
28public final class CpSolver {
30 public CpSolver() {
31 this.solveParameters = SatParameters.newBuilder();
32 this.logCallback = null;
33 this.solveWrapper = null;
34 }
35
38 return solveWithSolutionCallback(model, null);
39 }
40
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
75 return solve(model, cb);
76 }
77
92 @Deprecated
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
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
176 }
177
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:43
static String solverResponseStats(com.google.ortools.sat.CpSolverResponse response)
com.google.ortools.sat.CpSolverStatus getStatus()
java.util.List< java.lang.Integer > getSufficientAssumptionsForInfeasibilityList()
long getNumBranches()
int64 num_branches = 12;
long getNumConflicts()
int64 num_conflicts = 11;
double getUserTime()
double user_time = 16;
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
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
List< Integer > sufficientAssumptionsForInfeasibility()
Definition: CpSolver.java:174
String responseStats()
Returns some statistics on the solution found as a string.
Definition: CpSolver.java:189
void addSolutionCallback(SolutionCallback callback)
void setParameters(com.google.ortools.sat.SatParameters parameters)
void addLogCallback(java.util.function.Consumer< String > log_callback)
void clearSolutionCallback(SolutionCallback callback)
com.google.ortools.sat.CpSolverResponse solve(com.google.ortools.sat.CpModelProto model_proto)
A object that can build a LinearExpr object.
LinearExpr build()
Builds a linear expression.
A linear expression (sum (ai * xi) + b).
Definition: LinearExpr.java:19
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