#include <disjunctive.h>

Inheritance diagram for operations_research::sat::DisjunctiveOverloadChecker:

Public Member Functions
	DisjunctiveOverloadChecker (SchedulingConstraintHelper helper, Model model=nullptr)

bool	Propagate () final

int	RegisterWith (GenericLiteralWatcher *watcher)

Public Member Functions inherited from operations_research::sat::PropagatorInterface
	PropagatorInterface ()=default

virtual	~PropagatorInterface ()=default

virtual bool	IncrementalPropagate (const std::vector< int > &)

Detailed Description

Below are many of the known propagation techniques for the disjunctive, each implemented in only one time direction and in its own propagator class. The Disjunctive() model function above will instantiate the used ones (according to the solver parameters) in both time directions.

See Petr Vilim PhD "Global Constraints in Scheduling" for a description of some of the algorithm.

Definition at line 178 of file disjunctive.h.

Constructor & Destructor Documentation

◆ DisjunctiveOverloadChecker()

operations_research::sat::DisjunctiveOverloadChecker::DisjunctiveOverloadChecker	(	SchedulingConstraintHelper *	helper,
		Model *	model = nullptr )

inlineexplicit

Definition at line 180 of file disjunctive.h.

Member Function Documentation

◆ Propagate()

bool operations_research::sat::DisjunctiveOverloadChecker::Propagate ( )

finalvirtual

This will be called after one or more literals that are watched by this propagator changed. It will also always be called on the first propagation cycle after registration.

We use this to detect precedence between task that must cause a push.

Split problem into independent part.

Many propagators in this file use the same approach, we start by processing the task by increasing start-min, packing everything to the left. We then process each "independent" set of task separately. A task is independent from the one before it, if its start-min wasn't pushed.

This way, we get one or more window [window_start, window_end] so that for all task in the window, [start_min, end_min] is inside the window, and the end min of any set of task to the left is <= window_start, and the start_min of any task to the right is >= end_min.

Nothing to do with overload checking, but almost free to do that here.

We have a detectable precedence that must cause a push.

Remarks: If we added all precedence literals + linear relation, this propagation would have been done by the linear propagator, but if we didn't add such relations yet, it is beneficial to detect that here!

Todo: (user): Actually, we just infered a "not last" so we could check for relevant_size > 2 potential propagation?

Todo: (user): Can we detect and propagate all such relations easily and do a pass before this maybe? On a related note, because this propagator is not instantiated in both direction, we might miss some easy propag.

Todo: (user): Shall we keep propagating? we know the prefix didn't change, so we could be faster here. On another hand, it might be better to propagate all the linear constraints before returning here.

Note: we need to do that AFTER the block above.

Extend window.

Process current window. We don't need to process the end of the window (after relevant_size) because these interval can be greedily assembled in a feasible solution.

Start of the next window.

Process last window.

Implements operations_research::sat::PropagatorInterface.

Definition at line 462 of file disjunctive.cc.

◆ RegisterWith()

int operations_research::sat::DisjunctiveOverloadChecker::RegisterWith ( GenericLiteralWatcher * watcher )

This propagator reach the fix point in one pass.

Definition at line 700 of file disjunctive.cc.

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