Java Reference

Java Reference

CpSolver.java
Go to the documentation of this file.
1// Copyright 2010-2018 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;
20
27public final class CpSolver {
29 public CpSolver() {
30 this.solveParameters = SatParameters.newBuilder();
31 }
32
34 public CpSolverStatus solve(CpModel model) {
35 solveResponse = SatHelper.solveWithParameters(model.model(), solveParameters.build());
36 return solveResponse.getStatus();
37 }
38
41 solveResponse = SatHelper.solveWithParametersAndSolutionCallback(
42 model.model(), solveParameters.build(), cb);
43 return solveResponse.getStatus();
44 }
45
58 public CpSolverStatus searchAllSolutions(CpModel model, CpSolverSolutionCallback cb) {
59 solveParameters.setEnumerateAllSolutions(true);
60 solveResponse = SatHelper.solveWithParametersAndSolutionCallback(
61 model.model(), solveParameters.build(), cb);
62 solveParameters.setEnumerateAllSolutions(true);
63 return solveResponse.getStatus();
64 }
65
67 public double objectiveValue() {
68 return solveResponse.getObjectiveValue();
69 }
70
75 public double bestObjectiveBound() {
76 return solveResponse.getBestObjectiveBound();
77 }
78
80 public long value(IntVar var) {
81 return solveResponse.getSolution(var.getIndex());
82 }
83
85 public Boolean booleanValue(Literal var) {
86 int index = var.getIndex();
87 if (index >= 0) {
88 return solveResponse.getSolution(index) != 0;
89 } else {
90 return solveResponse.getSolution(-index - 1) == 0;
91 }
92 }
93
95 public CpSolverResponse response() {
96 return solveResponse;
97 }
98
100 public long numBranches() {
101 return solveResponse.getNumBranches();
102 }
103
105 public long numConflicts() {
106 return solveResponse.getNumConflicts();
107 }
108
110 public double wallTime() {
111 return solveResponse.getWallTime();
112 }
113
115 public double userTime() {
116 return solveResponse.getUserTime();
117 }
118
120 return solveResponse.getSufficientAssumptionsForInfeasibilityList();
121 }
122
124 public SatParameters.Builder getParameters() {
125 return solveParameters;
126 }
127
129 public String responseStats() {
130 return SatHelper.solverResponseStats(solveResponse);
131 }
132
133 private CpSolverResponse solveResponse;
134 private final SatParameters.Builder solveParameters;
135}
Main modeling class.
Definition: CpModel.java:41
Parent class to create a callback called at each solution.
Wrapper around the SAT solver.
Definition: CpSolver.java:27
CpSolver()
Main construction of the CpSolver class.
Definition: CpSolver.java:29
double objectiveValue()
Returns the best objective value found during search.
Definition: CpSolver.java:67
double userTime()
Returns the user time of the search.
Definition: CpSolver.java:115
double wallTime()
Returns the wall time of the search.
Definition: CpSolver.java:110
double bestObjectiveBound()
Returns the best lower bound found when minimizing, of the best upper bound found when maximizing.
Definition: CpSolver.java:75
CpSolverResponse response()
Returns the internal response protobuf that is returned internally by the SAT solver.
Definition: CpSolver.java:95
CpSolverStatus solveWithSolutionCallback(CpModel model, CpSolverSolutionCallback cb)
Solves a problem and passes each solution found to the callback.
Definition: CpSolver.java:40
long value(IntVar var)
Returns the value of a variable in the last solution found.
Definition: CpSolver.java:80
long numBranches()
Returns the number of branches explored during search.
Definition: CpSolver.java:100
CpSolverStatus searchAllSolutions(CpModel model, CpSolverSolutionCallback cb)
Searches for all solutions of a satisfiability problem.
Definition: CpSolver.java:58
CpSolverStatus solve(CpModel model)
Solves the given module, and returns the solve status.
Definition: CpSolver.java:34
long numConflicts()
Returns the number of conflicts created during search.
Definition: CpSolver.java:105
SatParameters.Builder getParameters()
Returns the builder of the parameters of the SAT solver for modification.
Definition: CpSolver.java:124
Boolean booleanValue(Literal var)
Returns the Boolean value of a literal in the last solution found.
Definition: CpSolver.java:85
List< Integer > sufficientAssumptionsForInfeasibility()
Definition: CpSolver.java:119
String responseStats()
Returns some statistics on the solution found as a string.
Definition: CpSolver.java:129
An integer variable.
Definition: IntVar.java:21
int getIndex()
Internal, returns the index of the variable in the underlying CpModelProto.
Definition: IntVar.java:45
Interface to describe a boolean variable or its negation.
Definition: Literal.java:17