operations_research::sat::GreaterThanAtLeastOneOfDetector Class Reference

#include <precedences.h>

Public Member Functions
	GreaterThanAtLeastOneOfDetector (Model *model)
int	AddGreaterThanAtLeastOneOfConstraints (Model *model, bool auto_detect_clauses=false)

Detailed Description

Detects if at least one of a subset of linear of size 2 or 1, touching the same variable, must be true. When this is the case we add a new propagator to propagate that fact.

Todo

(user): Shall we do that on the main thread before the workers are spawned? note that the probing version need the model to be loaded though.

Definition at line 535 of file precedences.h.

Constructor & Destructor Documentation

GreaterThanAtLeastOneOfDetector()

operations_research::sat::GreaterThanAtLeastOneOfDetector::GreaterThanAtLeastOneOfDetector ( Model * model )

inlineexplicit

Definition at line 537 of file precedences.h.

Member Function Documentation

AddGreaterThanAtLeastOneOfConstraints()

int operations_research::sat::GreaterThanAtLeastOneOfDetector::AddGreaterThanAtLeastOneOfConstraints	(	Model *	model,
		bool	auto_detect_clauses = false )

Advanced usage. To be called once all the constraints have been added to the model. This will detect GreaterThanAtLeastOneOfConstraint(). Returns the number of added constraint.

Todo

(user): This can be quite slow, add some kind of deterministic limit so that we can use it all the time.

We have two possible approaches. For now, we prefer the first one except if there is too many clauses in the problem.

Todo

(user): Do more extensive experiment. Remove the second approach as it is more time consuming? or identify when it make sense. Note that the first approach also allows to use "incomplete" at least one between arcs.

Todo

(user): This does not take into account clause of size 2 since they are stored in the BinaryImplicationGraph instead. Some ideas specific to size 2:

• There can be a lot of such clauses, but it might be nice to consider them. we need to experiments.
• The automatic clause detection might be a better approach and it could be combined with probing.

It is common that there is only two alternatives to push a variable. In this case, our presolve most likely made sure that the two are controlled by a single Boolean. This allows to detect this and add the appropriate greater than at least one of.

Definition at line 1328 of file precedences.cc.

---

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

• ortools/sat/precedences.h
• ortools/sat/precedences.cc