operations_research::sat::HittingSetOptimizer Class Reference

#include <max_hs.h>

Public Member Functions
	HittingSetOptimizer (const CpModelProto &model_proto, const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
SatSolver::Status	Optimize ()

Detailed Description

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

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.

Definition at line 59 of file max_hs.h.

Constructor & Destructor Documentation

HittingSetOptimizer()

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

Definition at line 66 of file max_hs.cc.

Member Function Documentation

Optimize()

SatSolver::Status operations_research::sat::HittingSetOptimizer::Optimize

(

)

This is the "generalized" hitting set problem we will solve. Each time we find a core, a new constraint will be added to this problem.

Todo

(user): remove code duplication with MinimizeWithCoreAndLazyEncoding();

This is used by the "stratified" approach. We will only consider terms with a weight not lower than this threshold. The threshold will decrease as the algorithm progress.

Start the algorithm.

Todo

(user): Even though we keep the same solver, currently the solve is not really done incrementally. It might be hard to improve though.

Todo

(user): deal with time limit.

Get the best external bound and constraint the objective of the MPModel.

Todo

(user): C^c is broken when using SCIP.

We currently abort if we have a non-optimal result. This is correct if we had a limit reached, but not in the other cases.

Todo

(user): It is actually easy to use a FEASIBLE result. If when passing it to SAT it is no feasbile, we can still create cores. If it is feasible, we have a solution, but we cannot increase the lower bound.

Update the objective lower bound with our current bound.

Note(user): This is not needed for correctness, but it might cause more propagation and is nice to have for reporting/logging purpose.

No assumptions with the current stratified_threshold? use the new one.

Todo

(user): Use the real weights and exploit the extra cores.

Todo

Todo

(user): If we extract more than the objective variables, we could use the solution values from the MPModel as hints to the SAT model.

If not all assumptions were taken, continue with a lower stratified bound. Otherwise we have an optimal solution.

Hack: we use a local limit internally that we restore at the end. However we still return LIMIT_REACHED in this case...

Definition at line 553 of file max_hs.cc.

---

The documentation for this class was generated from the following files:

• ortools/sat/max_hs.h
• ortools/sat/max_hs.cc