operations_research::sat::GreaterThanAtLeastOneOfDetector Class Reference

#include <precedences.h>

Public Member Functions
void	Add (Literal lit, LinearTerm a, LinearTerm b, IntegerValue lhs, IntegerValue rhs)
	Adds a relation lit => a + b \in [lhs, rhs].
int	AddGreaterThanAtLeastOneOfConstraints (Model *model, bool auto_detect_clauses=false)

Detailed Description

This collect all enforced linear of size 2 or 1 and detect if at least one of a subset 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 475 of file precedences.h.

Member Function Documentation

Add()

void operations_research::sat::GreaterThanAtLeastOneOfDetector::Add	(	Literal	lit,
		LinearTerm	a,
		LinearTerm	b,
		IntegerValue	lhs,
		IntegerValue	rhs )

Adds a relation lit => a + b \in [lhs, rhs].

We shall only consider positive variable here.

Definition at line 1102 of file precedences.cc.

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.

Initialize lit_to_relations_.

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.

Release the memory, it is not longer needed.

Definition at line 1312 of file precedences.cc.

---

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

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