Stay organized with collections Save and categorize content based on your preferences.

C++ Reference: class HittingSetOptimizer

Note: This documentation is automatically generated.

Generalization of the max-HS algorithm (HS stands for Hitting Set). This is similar to MinimizeWithCoreAndLazyEncoding() but it uses a hybrid approach with a MIP solver to handle the discovered infeasibility cores.

See, Jessica Davies and Fahiem Bacchus, "Solving MAXSAT by Solving a Sequence of Simpler SAT Instances", http://www.cs.toronto.edu/~jdavies/daviesCP11.pdf"

Note that an implementation of this approach won the 2016 max-SAT competition on the industrial category, see http://maxsat.ia.udl.cat/results/#wpms-industrial

TODO(user): This class requires linking with the SCIP MIP solver which is quite big, maybe we should find a way not to do that.
Method
HittingSetOptimizer

Arguments: const CpModelProto& model_proto, const ObjectiveDefinition& objective_definition, const std::function<void()>& feasible_solution_observer, Model* model

Optimize

Return type: SatSolver::Status