Implementation of AllDifferentAC(). More...

#include <all_different.h>

Inheritance diagram for operations_research::sat::AllDifferentConstraint:

Public Member Functions
	AllDifferentConstraint (absl::Span< const IntegerVariable > variables, Model *model)

	AllDifferentConstraint (int num_nodes, absl::Span< const int > tails, absl::Span< const int > heads, absl::Span< const Literal > literals, Model *model)

bool	Propagate () final

void	RegisterWith (GenericLiteralWatcher *watcher)

Detailed Description

Implementation of AllDifferentAC().

Definition at line 66 of file all_different.h.

Constructor & Destructor Documentation

◆ AllDifferentConstraint() [1/2]

operations_research::sat::AllDifferentConstraint::AllDifferentConstraint	(	absl::Span< const IntegerVariable >	variables,
		Model *	model )

Initialize literals cache.

Note: remap all values appearing here with a dense_index.

FullyEncode does not like 1-value domains, handle this case first.

Todo: (user): Prune now, ignore these variables during solving.

Force full encoding if not already done.

Fill cache with literals, default value is kFalseLiteralIndex.

Not sure it is needed, but lets sort.

Definition at line 116 of file all_different.cc.

◆ AllDifferentConstraint() [2/2]

operations_research::sat::AllDifferentConstraint::AllDifferentConstraint	(	int	num_nodes,
		absl::Span< const int >	tails,
		absl::Span< const int >	heads,
		absl::Span< const Literal >	literals,
		Model *	model )

In a circuit, the successor of all node must be "different". Thus this propagator can also be used in this context.

We assume everything is already dense.

Definition at line 169 of file all_different.cc.

Member Function Documentation

◆ Propagate()

bool operations_research::sat::AllDifferentConstraint::Propagate ( )

finalvirtual

The algorithm copies the solver state to successor_, which is used to compute a matching. If all variables can be matched, it generates the residual graph in separate vectors, computes its SCCs, and filters variable -> value if variable is not in the same SCC as value. Explanations for failure and filtering are fine-grained: failure is explained by a Hall set, i.e. dom(variables) \subseteq {values}, with variables < values; filtering is explained by the Hall set that would happen if the variable was assigned to the value.

Todo: (user): If needed, there are several ways performance could be improved. If copying the variable state is too costly, it could be maintained instead. If the propagator has too many fruitless calls (without failing/pruning), we can remember the O(n) arcs used in the matching and the SCC decomposition, and guard calls to Propagate() if these arcs are still valid.

Copy variable state to graph state.

Forward-checking should propagate x != value.

Seed with previous matching.

Compute max matching.

Fail if covering variables impossible. Explain with the forbidden parts of the graph that prevent MakeAugmentingPath from increasing the matching size.

For now explain all forbidden arcs.

The current matching is a valid solution, now try to filter values. Build residual graph, compute its SCCs.

Compute SCCs, make node -> component map.

Remove arcs var -> val where SCC(var) -/->* SCC(val).

We can deduce that x != value. To explain, force x == value, then find another assignment for the variable matched to value. It will fail: explaining why is the same as explaining failure as above, and it is an explanation of x != value.

Undo x -> old_value and old_variable -> value.

Implements operations_research::sat::PropagatorInterface.

Definition at line 262 of file all_different.cc.

◆ RegisterWith()

void operations_research::sat::AllDifferentConstraint::RegisterWith ( GenericLiteralWatcher * watcher )

Watch only unbound literals.

Definition at line 190 of file all_different.cc.

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

ortools/sat/all_different.h
ortools/sat/all_different.cc