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<storm::settings::modules::CoreSettings>().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..cd556c936 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<storm::settings::modules::GurobiSettings>().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<storm::settings::modules::GurobiSettings>().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<storm::settings::modules::GurobiSettings>().getNumberOfConcurrentMipThreads());
+ 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<storm::settings::modules::GurobiSettings>().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<typename ValueType>
void GurobiLpSolver<ValueType>::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<typename ValueType>
+ void GurobiLpSolver<ValueType>::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<typename ValueType>
+ uint64_t GurobiLpSolver<ValueType>::getSolutionCount() const {
+ STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to GurobiLpSolver<ValueType>::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<typename ValueType>
+ ValueType GurobiLpSolver<ValueType>::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<ValueType>(value);
+ }
+
+ template<typename ValueType>
+ int_fast64_t GurobiLpSolver<ValueType>::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<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
+
+ return static_cast<int_fast64_t>(value);
+ }
+
+ template<typename ValueType>
+ bool GurobiLpSolver<ValueType>::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<int>(value) - 1) <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
+ } else {
+ STORM_LOG_THROW(value <= storm::settings::getModule<storm::settings::modules::GurobiSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
+ }
+
+ return static_cast<bool>(value);
+ }
+
+ template<typename ValueType>
+ ValueType GurobiLpSolver<ValueType>::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<ValueType>(value);
+ }
+
+ template<typename ValueType>
+ void GurobiLpSolver<ValueType>::setMaximalMILPGap(ValueType const& gap, bool relative) {
+ int error = -1;
+ if (relative) {
+ error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAP, storm::utility::convertNumber<double>(gap));
+ } else {
+ error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAPABS, storm::utility::convertNumber<double>(gap));
+ }
+ STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi MILP GAP (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ }
+
+ template<typename ValueType>
+ ValueType GurobiLpSolver<ValueType>::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<ValueType>(relativeGap);
+ if (relative) {
+ return result;
+ } else {
+ return result * getObjectiveValue();
+ }
+ }
#else
template<typename ValueType>
@@ -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<typename ValueType>
+ void GurobiLpSolver<ValueType>::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<typename ValueType>
+ uint64_t GurobiLpSolver<ValueType>::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<typename ValueType>
+ ValueType GurobiLpSolver<ValueType>::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<typename ValueType>
+ int_fast64_t GurobiLpSolver<ValueType>::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<typename ValueType>
+ bool GurobiLpSolver<ValueType>::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<typename ValueType>
+ ValueType GurobiLpSolver<ValueType>::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<typename ValueType>
+ void GurobiLpSolver<ValueType>::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<typename ValueType>
+ ValueType GurobiLpSolver<ValueType>::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<double>;
template class GurobiLpSolver<storm::RationalNumber>;
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.