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 |
Except as otherwise noted, the content of this page is licensed under the Creative Commons Attribution 4.0 License, and code samples are licensed under the Apache 2.0 License. For details, see the Google Developers Site Policies. Java is a registered trademark of Oracle and/or its affiliates.
Last updated 2024-08-06 UTC.
[null,null,["Last updated 2024-08-06 UTC."],[[["HittingSetOptimizer is a generalization of the max-HS algorithm, similar to MinimizeWithCoreAndLazyEncoding but uses a hybrid approach with a MIP solver."],["It's based on the research paper \"Solving MAXSAT by Solving a Sequence of Simpler SAT Instances\" by Jessica Davies and Fahiem Bacchus."],["This approach was successful in the 2016 max-SAT competition, specifically in the industrial category."],["Currently, it requires linking with the SCIP MIP solver, which is large and potentially needs optimization."]]],["The `HittingSetOptimizer` class implements a hybrid approach, generalizing the max-HS algorithm, using a MIP solver to manage infeasibility cores. It is similar to `MinimizeWithCoreAndLazyEncoding`. This approach won the 2016 max-SAT competition in the industrial category. Key methods include `HittingSetOptimizer`, which initializes with model data and an observer, and `Optimize`, which performs the optimization and returns the solver status. The implementation is noted to require linking with the SCIP MIP solver.\n"]]
