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 
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 
27 public 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 
40  public CpSolverStatus solveWithSolutionCallback(CpModel model, CpSolverSolutionCallback cb) {
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 
119  public List<Integer> sufficientAssumptionsForInfeasibility() {
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
List< Integer > sufficientAssumptionsForInfeasibility()
Definition: CpSolver.java:119
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
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