diff --git a/src/storm/settings/modules/GurobiSettings.cpp b/src/storm/settings/modules/GurobiSettings.cpp index 4f35e085a..094382d27 100644 --- a/src/storm/settings/modules/GurobiSettings.cpp +++ b/src/storm/settings/modules/GurobiSettings.cpp @@ -15,6 +15,8 @@ namespace storm { const std::string GurobiSettings::integerToleranceOption = "inttol"; const std::string GurobiSettings::threadsOption = "threads"; const std::string GurobiSettings::outputOption = "output"; + const std::string GurobiSettings::mipFocusOption = "mipfocus"; + const std::string GurobiSettings::concurrentMipThreadsOption = "concurrentmip"; GurobiSettings::GurobiSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build()); @@ -22,6 +24,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, mipFocusOption, true, "The high level solution strategy used to solve MILPs.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of the strategy.").setDefaultValueUnsignedInteger(0).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorIncluding(0, 3)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, concurrentMipThreadsOption, true, "The number of MIP solvers Gurobi spawns in parallel. Shall not be larger then the number of threads.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of parallel solvers.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedGreaterEqualValidator(1)).build()).build()); } bool GurobiSettings::isIntegerToleranceSet() const { @@ -44,11 +50,19 @@ namespace storm { return this->getOption(outputOption).getHasOptionBeenSet(); } + uint_fast64_t GurobiSettings::getMIPFocus() const { + return this->getOption(mipFocusOption).getArgumentByName("value").getValueAsUnsignedInteger(); + } + + uint_fast64_t GurobiSettings::getNumberOfConcurrentMipThreads() const { + return this->getOption(concurrentMipThreadsOption).getArgumentByName("value").getValueAsUnsignedInteger(); + } + bool GurobiSettings::check() const { if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) { STORM_LOG_WARN_COND(storm::settings::getModule().getLpSolver() == storm::solver::LpSolverType::Gurobi, "Gurobi is not selected as the preferred LP solver, so setting options for Gurobi might have no effect."); } - + STORM_LOG_WARN_COND(getNumberOfConcurrentMipThreads() <= getNumberOfThreads(), "Requested more concurrent MILP solvers then the available threads for Gurobi." ); return true; } diff --git a/src/storm/settings/modules/GurobiSettings.h b/src/storm/settings/modules/GurobiSettings.h index c91cf96f3..0151f6714 100644 --- a/src/storm/settings/modules/GurobiSettings.h +++ b/src/storm/settings/modules/GurobiSettings.h @@ -45,6 +45,21 @@ namespace storm { */ uint_fast64_t getNumberOfThreads() const; + /*! + * Retrieves the selected high-level solution strategy for MILPs. + * + * @return The high-level solution strategy. + */ + uint_fast64_t getMIPFocus() const; + + + /*! + * Retrieves the number of MIP solvers, Gurobi spawns in parallel. + * + * @return The number of MIP solvers Gurobi spawns in parallel.. + */ + uint_fast64_t getNumberOfConcurrentMipThreads() const; + /*! * Retrieves whether the output option was set. * @@ -62,6 +77,8 @@ namespace storm { static const std::string integerToleranceOption; static const std::string threadsOption; static const std::string outputOption; + static const std::string mipFocusOption; + static const std::string concurrentMipThreadsOption; }; } // namespace modules diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 3e0db5333..233427744 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -76,7 +76,13 @@ namespace storm { // Enable the following line to restrict Gurobi to one thread only. error = GRBsetintparam(env, "Threads", storm::settings::getModule().getNumberOfThreads()); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ")."); - + + error = GRBsetintparam(env, "MIPFocus", storm::settings::getModule().getMIPFocus()); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter MIPFocus (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + error = GRBsetintparam(env, "ConcurrentMIP", storm::settings::getModule().getMIPFocus()); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter ConcurrentMIP (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + // Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option. error = GRBsetdblparam(env, "IntFeasTol", storm::settings::getModule().getIntegerTolerance()); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ")."); @@ -175,6 +181,7 @@ namespace storm { template void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + STORM_LOG_TRACE("Adding constraint " << name << " to GurobiLpSolver:" << std::endl << "\t" << constraint); STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); @@ -436,6 +443,132 @@ namespace storm { } } + template + void GurobiLpSolver::setMaximalSolutionCount(uint64_t value) { + int error = GRBsetintparam(GRBgetenv(model), "PoolSolutions", value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter PoolSolutions (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + } + + template + uint64_t GurobiLpSolver::getSolutionCount() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to GurobiLpSolver::getSolutionCount: model has not been optimized."); + int result = -1; + int error = GRBgetintattr(model, "SolCount", &result); + STORM_LOG_THROW(error == 0 && result >= 0, storm::exceptions::InvalidStateException, "Unable to get solution count or invalid number of solutions."); + return result; + } + + template + ValueType GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable, uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + auto variableIndexPair = this->variableToIndexMap.find(variable); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + return storm::utility::convertNumber(value); + } + + template + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable, uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + auto variableIndexPair = this->variableToIndexMap.find(variable); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + STORM_LOG_THROW(std::abs(static_cast(value) - value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + + return static_cast(value); + } + + template + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable, uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + auto variableIndexPair = this->variableToIndexMap.find(variable); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + if (value > 0.5) { + STORM_LOG_THROW(std::abs(static_cast(value) - 1) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + } else { + STORM_LOG_THROW(value <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + } + + return static_cast(value); + } + + template + ValueType GurobiLpSolver::getObjectiveValue(uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattr(model, GRB_DBL_ATTR_POOLOBJVAL, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + return storm::utility::convertNumber(value); + } + + template + void GurobiLpSolver::setMaximalMILPGap(ValueType const& gap, bool relative) { + int error = -1; + if (relative) { + error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAP, storm::utility::convertNumber(gap)); + } else { + error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAPABS, storm::utility::convertNumber(gap)); + } + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi MILP GAP (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + } + + template + ValueType GurobiLpSolver::getMILPGap(bool relative) const { + double relativeGap; + int error = GRBgetdblattr(model, GRB_DBL_ATTR_MIPGAP, &relativeGap); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi MILP GAP (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + auto result = storm::utility::convertNumber(relativeGap); + if (relative) { + return result; + } else { + return result * getObjectiveValue(); + } + } #else template @@ -577,6 +710,49 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } + template + void GurobiLpSolver::setMaximalSolutionCount(uint64_t) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + uint64_t GurobiLpSolver::getSolutionCount() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getContinuousValue(storm::expressions::Variable const&, uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const&, uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const&, uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getObjectiveValue(uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + + template + void GurobiLpSolver::setMaximalMILPGap(ValueType const&, bool) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getMILPGap(bool) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + + #endif template class GurobiLpSolver; template class GurobiLpSolver; diff --git a/src/storm/solver/GurobiLpSolver.h b/src/storm/solver/GurobiLpSolver.h index 955e4c5ff..5947ad600 100644 --- a/src/storm/solver/GurobiLpSolver.h +++ b/src/storm/solver/GurobiLpSolver.h @@ -99,7 +99,6 @@ namespace storm { virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override; virtual bool getBinaryValue(storm::expressions::Variable const& name) const override; virtual ValueType getObjectiveValue() const override; - // Methods to print the LP problem to a file. virtual void writeModelToFile(std::string const& filename) const override; @@ -107,6 +106,28 @@ namespace storm { virtual void push() override; virtual void pop() override; + + // Methods to retrieve values of sub-optimal solutions found along the way. + void setMaximalSolutionCount(uint64_t value); // How many solutions will be stored (at max) + uint64_t getSolutionCount() const; // How many solutions have been found + ValueType getContinuousValue(storm::expressions::Variable const& name, uint64_t const& solutionIndex) const; + int_fast64_t getIntegerValue(storm::expressions::Variable const& name, uint64_t const& solutionIndex) const; + bool getBinaryValue(storm::expressions::Variable const& name, uint64_t const& solutionIndex) const; + ValueType getObjectiveValue(uint64_t const& solutionIndex) const; + + /*! + * Specifies the maximum difference between lower- and upper objective bounds that triggers termination. + * That means a solution is considered optimal if + * upperBound - lowerBound < gap * (relative ? |upperBound| : 1). + * Only relevant for programs with integer/boolean variables. + */ + void setMaximalMILPGap(ValueType const& gap, bool relative); + + /*! + * Returns the obtained gap after a call to optimize() + */ + ValueType getMILPGap(bool relative) const; + private: /*! * Sets some properties of the Gurobi environment according to parameters given by the options.