Google OR-Tools v9.9
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
com.google.ortools.sat.CpSolver Class Reference

Public Member Functions

 CpSolver ()
 
CpSolverStatus solve (CpModel model)
 
CpSolverStatus solve (CpModel model, CpSolverSolutionCallback cb)
 
CpSolverStatus solveWithSolutionCallback (CpModel model, CpSolverSolutionCallback cb)
 
CpSolverStatus searchAllSolutions (CpModel model, CpSolverSolutionCallback cb)
 
synchronized void stopSearch ()
 
double objectiveValue ()
 
double bestObjectiveBound ()
 
long value (LinearArgument expr)
 
Boolean booleanValue (Literal var)
 
CpSolverResponse response ()
 
long numBranches ()
 
long numConflicts ()
 
double wallTime ()
 
double userTime ()
 
List< Integer > sufficientAssumptionsForInfeasibility ()
 
SatParameters.Builder getParameters ()
 
void setLogCallback (Consumer< String > cb)
 
String responseStats ()
 
String getSolutionInfo ()
 
 CpSolver ()
 
CpSolverStatus solve (CpModel model)
 
CpSolverStatus solve (CpModel model, CpSolverSolutionCallback cb)
 
CpSolverStatus solveWithSolutionCallback (CpModel model, CpSolverSolutionCallback cb)
 
CpSolverStatus searchAllSolutions (CpModel model, CpSolverSolutionCallback cb)
 
synchronized void stopSearch ()
 
double objectiveValue ()
 
double bestObjectiveBound ()
 
long value (LinearArgument expr)
 
Boolean booleanValue (Literal var)
 
CpSolverResponse response ()
 
long numBranches ()
 
long numConflicts ()
 
double wallTime ()
 
double userTime ()
 
List< Integer > sufficientAssumptionsForInfeasibility ()
 
SatParameters.Builder getParameters ()
 
void setLogCallback (Consumer< String > cb)
 
String responseStats ()
 
String getSolutionInfo ()
 

Detailed Description

Wrapper around the SAT solver.

This class proposes different solve() methods, as well as accessors to get the values of variables in the best solution, as well as general statistics of the search.

Definition at line 28 of file CpSolver.java.

Constructor & Destructor Documentation

◆ CpSolver() [1/2]

com.google.ortools.sat.CpSolver.CpSolver ( )

Main construction of the CpSolver class.

Definition at line 30 of file CpSolver.java.

◆ CpSolver() [2/2]

com.google.ortools.sat.CpSolver.CpSolver ( )

Main construction of the CpSolver class.

Definition at line 30 of file CpSolver.java.

Member Function Documentation

◆ bestObjectiveBound() [1/2]

double com.google.ortools.sat.CpSolver.bestObjectiveBound ( )

Returns the best lower bound found when minimizing, of the best upper bound found when maximizing.

Definition at line 125 of file CpSolver.java.

◆ bestObjectiveBound() [2/2]

double com.google.ortools.sat.CpSolver.bestObjectiveBound ( )

Returns the best lower bound found when minimizing, of the best upper bound found when maximizing.

Definition at line 125 of file CpSolver.java.

◆ booleanValue() [1/2]

Boolean com.google.ortools.sat.CpSolver.booleanValue ( Literal var)

Returns the Boolean value of a literal in the last solution found.

Definition at line 140 of file CpSolver.java.

◆ booleanValue() [2/2]

Boolean com.google.ortools.sat.CpSolver.booleanValue ( Literal var)

Returns the Boolean value of a literal in the last solution found.

Definition at line 140 of file CpSolver.java.

◆ getParameters() [1/2]

SatParameters.Builder com.google.ortools.sat.CpSolver.getParameters ( )

Returns the builder of the parameters of the SAT solver for modification.

Definition at line 179 of file CpSolver.java.

◆ getParameters() [2/2]

SatParameters.Builder com.google.ortools.sat.CpSolver.getParameters ( )

Returns the builder of the parameters of the SAT solver for modification.

Definition at line 179 of file CpSolver.java.

◆ getSolutionInfo() [1/2]

String com.google.ortools.sat.CpSolver.getSolutionInfo ( )

Returns some information on how the solution was found, or the reason why the model or the parameters are invalid.

Definition at line 197 of file CpSolver.java.

◆ getSolutionInfo() [2/2]

String com.google.ortools.sat.CpSolver.getSolutionInfo ( )

Returns some information on how the solution was found, or the reason why the model or the parameters are invalid.

Definition at line 197 of file CpSolver.java.

◆ numBranches() [1/2]

long com.google.ortools.sat.CpSolver.numBranches ( )

Returns the number of branches explored during search.

Definition at line 155 of file CpSolver.java.

◆ numBranches() [2/2]

long com.google.ortools.sat.CpSolver.numBranches ( )

Returns the number of branches explored during search.

Definition at line 155 of file CpSolver.java.

◆ numConflicts() [1/2]

long com.google.ortools.sat.CpSolver.numConflicts ( )

Returns the number of conflicts created during search.

Definition at line 160 of file CpSolver.java.

◆ numConflicts() [2/2]

long com.google.ortools.sat.CpSolver.numConflicts ( )

Returns the number of conflicts created during search.

Definition at line 160 of file CpSolver.java.

◆ objectiveValue() [1/2]

double com.google.ortools.sat.CpSolver.objectiveValue ( )

Returns the best objective value found during search.

Definition at line 117 of file CpSolver.java.

◆ objectiveValue() [2/2]

double com.google.ortools.sat.CpSolver.objectiveValue ( )

Returns the best objective value found during search.

Definition at line 117 of file CpSolver.java.

◆ response() [1/2]

CpSolverResponse com.google.ortools.sat.CpSolver.response ( )

Returns the internal response protobuf that is returned internally by the SAT solver.

Definition at line 150 of file CpSolver.java.

◆ response() [2/2]

CpSolverResponse com.google.ortools.sat.CpSolver.response ( )

Returns the internal response protobuf that is returned internally by the SAT solver.

Definition at line 150 of file CpSolver.java.

◆ responseStats() [1/2]

String com.google.ortools.sat.CpSolver.responseStats ( )

Returns some statistics on the solution found as a string.

Definition at line 189 of file CpSolver.java.

◆ responseStats() [2/2]

String com.google.ortools.sat.CpSolver.responseStats ( )

Returns some statistics on the solution found as a string.

Definition at line 189 of file CpSolver.java.

◆ searchAllSolutions() [1/2]

CpSolverStatus com.google.ortools.sat.CpSolver.searchAllSolutions ( CpModel model,
CpSolverSolutionCallback cb )

Searches for all solutions of a satisfiability problem.

This method searches for all feasible solutions of a given model. Then it feeds the solutions to the callback.

Note that the model cannot have an objective.

Parameters
modelthe model to solve
cbthe callback that will be called at each solution
Returns
the status of the solve (FEASIBLE, INFEASIBLE...)
Deprecated
Use the solve() method with the same signature, after setting the enumerate_all_solution parameter to true.

Definition at line 93 of file CpSolver.java.

◆ searchAllSolutions() [2/2]

CpSolverStatus com.google.ortools.sat.CpSolver.searchAllSolutions ( CpModel model,
CpSolverSolutionCallback cb )

Searches for all solutions of a satisfiability problem.

This method searches for all feasible solutions of a given model. Then it feeds the solutions to the callback.

Note that the model cannot have an objective.

Parameters
modelthe model to solve
cbthe callback that will be called at each solution
Returns
the status of the solve (FEASIBLE, INFEASIBLE...)
Deprecated
Use the solve() method with the same signature, after setting the enumerate_all_solution parameter to true.

Definition at line 93 of file CpSolver.java.

◆ setLogCallback() [1/2]

void com.google.ortools.sat.CpSolver.setLogCallback ( Consumer< String > cb)

Sets the log callback for the solver.

Definition at line 184 of file CpSolver.java.

◆ setLogCallback() [2/2]

void com.google.ortools.sat.CpSolver.setLogCallback ( Consumer< String > cb)

Sets the log callback for the solver.

Definition at line 184 of file CpSolver.java.

◆ solve() [1/4]

CpSolverStatus com.google.ortools.sat.CpSolver.solve ( CpModel model)

Solves the given model, and returns the solve status.

Definition at line 37 of file CpSolver.java.

◆ solve() [2/4]

CpSolverStatus com.google.ortools.sat.CpSolver.solve ( CpModel model)

Solves the given model, and returns the solve status.

Definition at line 37 of file CpSolver.java.

◆ solve() [3/4]

CpSolverStatus com.google.ortools.sat.CpSolver.solve ( CpModel model,
CpSolverSolutionCallback cb )

Solves the given model, calls the solution callback at each incumbent solution, and returns the solve status.

Setup search.

Cleanup search.

Definition at line 45 of file CpSolver.java.

◆ solve() [4/4]

CpSolverStatus com.google.ortools.sat.CpSolver.solve ( CpModel model,
CpSolverSolutionCallback cb )

Solves the given model, calls the solution callback at each incumbent solution, and returns the solve status.

Setup search.

Cleanup search.

Definition at line 45 of file CpSolver.java.

◆ solveWithSolutionCallback() [1/2]

CpSolverStatus com.google.ortools.sat.CpSolver.solveWithSolutionCallback ( CpModel model,
CpSolverSolutionCallback cb )

Solves the given model, passes each incumber solution to the solution callback if not null, and returns the solve status.

Deprecated
Use the solve() method with the same signature.

Definition at line 74 of file CpSolver.java.

◆ solveWithSolutionCallback() [2/2]

CpSolverStatus com.google.ortools.sat.CpSolver.solveWithSolutionCallback ( CpModel model,
CpSolverSolutionCallback cb )

Solves the given model, passes each incumber solution to the solution callback if not null, and returns the solve status.

Deprecated
Use the solve() method with the same signature.

Definition at line 74 of file CpSolver.java.

◆ stopSearch() [1/2]

synchronized void com.google.ortools.sat.CpSolver.stopSearch ( )

Stops the search asynchronously.

Definition at line 110 of file CpSolver.java.

◆ stopSearch() [2/2]

synchronized void com.google.ortools.sat.CpSolver.stopSearch ( )

Stops the search asynchronously.

Definition at line 110 of file CpSolver.java.

◆ sufficientAssumptionsForInfeasibility() [1/2]

List< Integer > com.google.ortools.sat.CpSolver.sufficientAssumptionsForInfeasibility ( )

Definition at line 174 of file CpSolver.java.

◆ sufficientAssumptionsForInfeasibility() [2/2]

List< Integer > com.google.ortools.sat.CpSolver.sufficientAssumptionsForInfeasibility ( )

Definition at line 174 of file CpSolver.java.

◆ userTime() [1/2]

double com.google.ortools.sat.CpSolver.userTime ( )

Returns the user time of the search.

Definition at line 170 of file CpSolver.java.

◆ userTime() [2/2]

double com.google.ortools.sat.CpSolver.userTime ( )

Returns the user time of the search.

Definition at line 170 of file CpSolver.java.

◆ value() [1/2]

long com.google.ortools.sat.CpSolver.value ( LinearArgument expr)

Returns the value of a linear expression in the last solution found.

Definition at line 130 of file CpSolver.java.

◆ value() [2/2]

long com.google.ortools.sat.CpSolver.value ( LinearArgument expr)

Returns the value of a linear expression in the last solution found.

Definition at line 130 of file CpSolver.java.

◆ wallTime() [1/2]

double com.google.ortools.sat.CpSolver.wallTime ( )

Returns the wall time of the search.

Definition at line 165 of file CpSolver.java.

◆ wallTime() [2/2]

double com.google.ortools.sat.CpSolver.wallTime ( )

Returns the wall time of the search.

Definition at line 165 of file CpSolver.java.


The documentation for this class was generated from the following files: