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","

Note that an implementation of this approach won the 2016 max-SAT competition on the industrial category, see

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.

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


Return type: SatSolver::Status