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."]]],[]]
