Module fr.univartois.cril.juniverse
Package fr.univartois.cril.juniverse.core

Interface IUniverseSolver

All Known Subinterfaces:
IUniverseConfigurableSolver, IUniverseCSPSolver, IUniverseOptimizationSolver, IUniversePseudoBooleanSolver, IUniverseSatSolver
public interface IUniverseSolver
The IUniverseSolver interface is the root interface defining the base contract for all solvers.

  • Method Details

    • reset

      void reset()
      Resets this solver in its original state.

    • nVariables

      int nVariables()
      Gives the number of variables defined in this solver.
      Returns:
      The number of variables.

    • getVariablesMapping

      Map<String,IUniverseVariable> getVariablesMapping()
      Gives the mapping of the variables in this solver.
      Returns:
      The mapping of the variables.

    • getAuxiliaryVariables

      List<String> getAuxiliaryVariables()
      Gives the list of the auxiliary variables used by the solver. These variables are those that the solver defines to help it represent the problem (for instance, to reify constraints).
      Returns:
      The list of the auxiliary variables, given by their name.

    • getConstraints

      List<IUniverseConstraint> getConstraints()
      Gives the list of the constraints in this solver.
      Returns:
      The list of the constraints.

    • decisionVariables

      void decisionVariables(List<String> variables)
      Advises this solver to focus on some variables to make decisions.
      Parameters:
      variables - The variables on which to make decisions.

    • valueHeuristicStatic

      void valueHeuristicStatic(List<String> variables, List<? extends Number> orderedValues)
      Forces a static order on the values to try for some variables.
      Parameters:
      variables - The variables for which a static order is set.
      orderedValues - The values to try for the specified variables, in the desired order.

    • nConstraints

      int nConstraints()
      Gives the number of constraints defined in this solver.
      Returns:
      The number of constraints.

    • isOptimization

      boolean isOptimization()
      Checks whether the associated problem is an optimization problem.
      Returns:
      Whether the problem is an optimization problem.

    • setTimeout

      void setTimeout(long seconds)
      Sets the time limit before interrupting the search.
      Parameters:
      seconds - The time limit to set (in seconds).

    • setTimeoutMs

      void setTimeoutMs(long mseconds)
      Sets the time limit before interrupting the search.
      Parameters:
      mseconds - The time limit to set (in milliseconds).

    • setVerbosity

      void setVerbosity(int level)
      Sets the verbosity level of the solver. Extreme values (outside the range expected by the underlying solver) should be handled silently as the minimum or maximum value supported by the solver.
      Parameters:
      level - The verbosity level to set.

    • addSearchListener

      default void addSearchListener(IUniverseSearchListener listener)
      Adds a listener to this solver, which listens to the events occurring in the solver during the search.
      Parameters:
      listener - The listener to add.
      Throws:
      UnsupportedOperationException - If this solver does not support search events.

    • removeSearchListener

      default void removeSearchListener(IUniverseSearchListener listener)
      Removes a listener from this solver, so that the listener does not listen to the events occurring in the solver during the search anymore.
      Parameters:
      listener - The listener to remove.
      Throws:
      UnsupportedOperationException - If this solver does not support search events.

    • setLogFile

      void setLogFile(String filename)
      Sets the log file to be used by the solver.
      Parameters:
      filename - The name of the log file.

    • setLogStream

      void setLogStream(OutputStream stream)
      Sets the output stream to be used by the solver for logging.
      Parameters:
      stream - The logging output stream.

    • loadInstance

      void loadInstance(String filename)
      Loads a problem stored in the given file. The solver is expected to parse the problem itself.
      Parameters:
      filename - The name of the file containing the problem to solve.

    • solve

      UniverseSolverResult solve()
      Solves the problem associated to this solver.
      Returns:
      The outcome of the search conducted by the solver.

    • solve

      UniverseSolverResult solve(String filename)
      Solves the problem stored in the given file. The solver is expected to parse the problem itself.
      Parameters:
      filename - The name of the file containing the problem to solve.
      Returns:
      The outcome of the search conducted by the solver.

    • solve

      UniverseSolverResult solve(List<UniverseAssumption<BigInteger>> assumptions)
      Solves the problem associated to this solver.
      Parameters:
      assumptions - The assumptions to consider when solving.
      Returns:
      The outcome of the search conducted by the solver.

    • interrupt

      void interrupt()
      Interrupts (asynchronously) the search currently performed by this solver.

    • solution

      List<BigInteger> solution()
      Gives the solution found by this solver (if any).
      Returns:
      The solution found by this solver.

    • mapSolution

      Map<String,BigInteger> mapSolution()
      Gives the mapping between the names of the variables and the assignment found by this solver (if any).
      Returns:
      The solution found by this solver.

    • mapSolution

      Map<String,BigInteger> mapSolution(boolean excludeAux)
      Gives the mapping between the names of the variables and the assignment found by this solver (if any).
      Parameters:
      excludeAux - Whether auxiliary variables should be excluded from the solution.
      Returns:
      The solution found by this solver.

    • checkSolution

      boolean checkSolution()
      Checks the last solution that has been computed by the solver. Said differently, this method ensures that the last solution satisfies all the constraints of the problem solved by the solver.
      Returns:
      Whether the last solution is correct.

    • checkSolution

      boolean checkSolution(Map<String,BigInteger> assignment)
      Checks whether the given assignment is a solution of the problem. Said differently, this method ensures that the given assignment satisfies all the constraints of the problem solved by the solver.
      Parameters:
      assignment - The assignment to check as a solution.
      Returns:
      Whether the given assignment is a solution of the problem.