Java Reference
Java Reference
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 27 of file CpSolver.java.
Public Member Functions  
CpSolver ()  
Main construction of the CpSolver class. More...  
CpSolverStatus  solve (CpModel model) 
Solves the given module, and returns the solve status. More...  
CpSolverStatus  solveWithSolutionCallback (CpModel model, CpSolverSolutionCallback cb) 
Solves a problem and passes each solution found to the callback. More...  
CpSolverStatus  searchAllSolutions (CpModel model, CpSolverSolutionCallback cb) 
Searches for all solutions of a satisfiability problem. More...  
double  objectiveValue () 
Returns the best objective value found during search. More...  
double  bestObjectiveBound () 
Returns the best lower bound found when minimizing, of the best upper bound found when maximizing. More...  
long  value (IntVar var) 
Returns the value of a variable in the last solution found. More...  
Boolean  booleanValue (Literal var) 
Returns the Boolean value of a literal in the last solution found. More...  
CpSolverResponse  response () 
Returns the internal response protobuf that is returned internally by the SAT solver. More...  
long  numBranches () 
Returns the number of branches explored during search. More...  
long  numConflicts () 
Returns the number of conflicts created during search. More...  
double  wallTime () 
Returns the wall time of the search. More...  
double  userTime () 
Returns the user time of the search. More...  
List< Integer >  sufficientAssumptionsForInfeasibility () 
SatParameters.Builder  getParameters () 
Returns the builder of the parameters of the SAT solver for modification. More...  
String  responseStats () 
Returns some statistics on the solution found as a string. More...  
Constructor & Destructor Documentation
◆ CpSolver()
CpSolver  (  ) 
Main construction of the CpSolver class.
Definition at line 29 of file CpSolver.java.
Member Function Documentation
◆ bestObjectiveBound()
double bestObjectiveBound  (  ) 
Returns the best lower bound found when minimizing, of the best upper bound found when maximizing.
Definition at line 75 of file CpSolver.java.
◆ booleanValue()
Boolean booleanValue  (  Literal  var  ) 
Returns the Boolean value of a literal in the last solution found.
Definition at line 85 of file CpSolver.java.
◆ getParameters()
SatParameters.Builder getParameters  (  ) 
Returns the builder of the parameters of the SAT solver for modification.
Definition at line 124 of file CpSolver.java.
◆ numBranches()
long numBranches  (  ) 
Returns the number of branches explored during search.
Definition at line 100 of file CpSolver.java.
◆ numConflicts()
long numConflicts  (  ) 
Returns the number of conflicts created during search.
Definition at line 105 of file CpSolver.java.
◆ objectiveValue()
double objectiveValue  (  ) 
Returns the best objective value found during search.
Definition at line 67 of file CpSolver.java.
◆ response()
CpSolverResponse response  (  ) 
Returns the internal response protobuf that is returned internally by the SAT solver.
Definition at line 95 of file CpSolver.java.
◆ responseStats()
String responseStats  (  ) 
Returns some statistics on the solution found as a string.
Definition at line 129 of file CpSolver.java.
◆ searchAllSolutions()
CpSolverStatus 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

model the model to solve cb the callback that will be called at each solution
 Returns
 the status of the solve (FEASIBLE, INFEASIBLE...)
Definition at line 58 of file CpSolver.java.
◆ solve()
CpSolverStatus solve  (  CpModel  model  ) 
Solves the given module, and returns the solve status.
Definition at line 34 of file CpSolver.java.
◆ solveWithSolutionCallback()
CpSolverStatus solveWithSolutionCallback  (  CpModel  model, 
CpSolverSolutionCallback  cb  
) 
Solves a problem and passes each solution found to the callback.
Definition at line 40 of file CpSolver.java.
◆ sufficientAssumptionsForInfeasibility()
List<Integer> sufficientAssumptionsForInfeasibility  (  ) 
Definition at line 119 of file CpSolver.java.
◆ userTime()
double userTime  (  ) 
Returns the user time of the search.
Definition at line 115 of file CpSolver.java.
◆ value()
long value  (  IntVar  var  ) 
Returns the value of a variable in the last solution found.
Definition at line 80 of file CpSolver.java.
◆ wallTime()
double wallTime  (  ) 
Returns the wall time of the search.
Definition at line 110 of file CpSolver.java.
The documentation for this class was generated from the following file: