Package com.google.ortools.sat

Class CpSolver

java.lang.Object
com.google.ortools.sat.CpSolver
public final class CpSolver
extends java.lang.Object
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.

  • Constructor Details

    • CpSolver

      public CpSolver()
      Main construction of the CpSolver class.

  • Method Details

    • solve

      public CpSolverStatus solve​(CpModel model)
      Solves the given module, and returns the solve status.

    • solveWithSolutionCallback

      public CpSolverStatus solveWithSolutionCallback​(CpModel model, CpSolverSolutionCallback cb)
      Solves a problem and passes each solution found to the callback.

    • searchAllSolutions

      public 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...)

    • stopSearch

      public void stopSearch()
      Stops the search asynchronously.

    • objectiveValue

      public double objectiveValue()
      Returns the best objective value found during search.

    • bestObjectiveBound

      public double bestObjectiveBound()
      Returns the best lower bound found when minimizing, of the best upper bound found when maximizing.

    • value

      public long value​(IntVar var)
      Returns the value of a variable in the last solution found.

    • booleanValue

      public java.lang.Boolean booleanValue​(Literal var)
      Returns the Boolean value of a literal in the last solution found.

    • response

      public CpSolverResponse response()
      Returns the internal response protobuf that is returned internally by the SAT solver.

    • numBranches

      public long numBranches()
      Returns the number of branches explored during search.

    • numConflicts

      public long numConflicts()
      Returns the number of conflicts created during search.

    • wallTime

      public double wallTime()
      Returns the wall time of the search.

    • userTime

      public double userTime()
      Returns the user time of the search.

    • sufficientAssumptionsForInfeasibility

      public java.util.List<java.lang.Integer> sufficientAssumptionsForInfeasibility()

    • getParameters

      public SatParameters.Builder getParameters()
      Returns the builder of the parameters of the SAT solver for modification.

    • setLogCallback

      public void setLogCallback​(java.util.function.Consumer<java.lang.String> cb)
      Sets the log callback for the solver.

    • responseStats

      public java.lang.String responseStats()
      Returns some statistics on the solution found as a string.