Implementation of AllDifferentAC(). More...

#include <all_different.h>

Inheritance diagram for operations_research::sat::AllDifferentConstraint:

Public Member Functions
	AllDifferentConstraint (std::vector< IntegerVariable > variables, IntegerEncoder encoder, Trail trail, IntegerTrail *integer_trail)

bool	Propagate () final

void	RegisterWith (GenericLiteralWatcher *watcher)

Detailed Description

Implementation of AllDifferentAC().

Definition at line 68 of file all_different.h.

Constructor & Destructor Documentation

◆ AllDifferentConstraint()

operations_research::sat::AllDifferentConstraint::AllDifferentConstraint	(	std::vector< IntegerVariable >	variables,
		IntegerEncoder *	encoder,
		Trail *	trail,
		IntegerTrail *	integer_trail )

Initialize literals cache.

Compute value range of all variables.

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.

Can happen because of initial propagation!

Definition at line 112 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.

Because we currently propagates all clauses before entering this propagator, we known that this can't happen.

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 == offset_value, then find another assignment for the variable matched to offset_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 -> offset_value.

Implements operations_research::sat::PropagatorInterface.

Definition at line 260 of file all_different.cc.

◆ RegisterWith()

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

Watch only unbound literals.

Definition at line 171 of file all_different.cc.

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