operations_research::sat::SymmetryPropagator Class Reference

#include <symmetry.h>

Inheritance diagram for operations_research::sat::SymmetryPropagator:

Public Member Functions
	SymmetryPropagator ()
	SymmetryPropagator (const SymmetryPropagator &)=delete
	This type is neither copyable nor movable.
SymmetryPropagator &	operator= (const SymmetryPropagator &)=delete
	~SymmetryPropagator () override
bool	Propagate (Trail *trail) final
void	Untrail (const Trail &trail, int trail_index) final
absl::Span< const Literal >	Reason (const Trail &trail, int trail_index, int64_t conflict_id) const final
void	AddSymmetry (std::unique_ptr< SparsePermutation > permutation)
int	num_permutations () const
void	Permute (int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
Public Member Functions inherited from operations_research::sat::SatPropagator
	SatPropagator (const std::string &name)
	SatPropagator (const SatPropagator &)=delete
	This type is neither copyable nor movable.
SatPropagator &	operator= (const SatPropagator &)=delete
virtual	~SatPropagator ()=default
void	SetPropagatorId (int id)
	Sets/Gets this propagator unique id.
int	PropagatorId () const
bool	PropagatePreconditionsAreSatisfied (const Trail &trail) const
	######################## Implementations below ########################
bool	PropagationIsDone (const Trail &trail) const
	Returns true iff all the trail was inspected by this propagator.
virtual bool	IsEmpty () const

Additional Inherited Members
Protected Attributes inherited from operations_research::sat::SatPropagator
const std::string	name_
int	propagator_id_
int	propagation_trail_index_

Detailed Description

This class implements more or less the strategy described in the paper: Devriendt J., Bogaerts B., De Cat B., Denecker M., Mears C. "Symmetry propagation: Improved Dynamic Symmetry Breaking in SAT", 2012, IEEE 24th International Conference on Tools with Artificial Intelligence.

Basically, each time a literal is propagated, this class tries to detect if another literal could also be propagated by symmetry. Note that this uses a heuristic in order to be efficient and that it is not exhaustive in the sense that it doesn't detect all possible propagations.

Algorithm details:

Given the current solver trail (i.e. the assigned literals and their assignment order) the idea is to compute (as efficiently as possible) for each permutation added to this class what is called the first (under the trail assignment order) non-symmetric literal. A literal 'l' is said to be non-symmetric under a given assignment and for a given permutation 'p' if 'l' is assigned to true but not 'p(l)'.

If a first non-symmetric literal 'l' for a permutation 'p' is not a decision, then:

• Because it is not a decision, 'l' has been implied by a reason formed by literals assigned to true at lower trail indices.
• Because this is the first non-symmetric literal for 'p', the permuted reason only contains literal that are also assigned to true.
• Because of this, 'p(l)' is also implied by the current assignment. Of course, this assume that p is a symmetry of the full problem.

  Note

  if it is already assigned to false, then we have a conflict.

  Todo

  (user): Implement the optimizations mentioned in the paper?

  (user): Instrument and see if the code can be optimized.

Definition at line 60 of file symmetry.h.

Constructor & Destructor Documentation

SymmetryPropagator() [1/2]

operations_research::sat::SymmetryPropagator::SymmetryPropagator

(

)

Definition at line 31 of file symmetry.cc.

SymmetryPropagator() [2/2]

operations_research::sat::SymmetryPropagator::SymmetryPropagator ( const SymmetryPropagator & )

delete

This type is neither copyable nor movable.

~SymmetryPropagator()

operations_research::sat::SymmetryPropagator::~SymmetryPropagator ( )

override

Definition at line 37 of file symmetry.cc.

Member Function Documentation

AddSymmetry()

void operations_research::sat::SymmetryPropagator::AddSymmetry

(

std::unique_ptr< SparsePermutation >

permutation

)

Adds a new permutation to this symmetry propagator. The ownership is transferred. This must be an integer permutation such that:

• Its domain is [0, 2 * num_variables) and corresponds to the index representation of the literals over num_variables variables.
• It must be compatible with the negation, for any literal l; not(p(l)) must be the same as p(not(l)), where p(x) represents the image of x by the permutation.

Remark: Any permutation which is a symmetry of the main SAT problem can be added here. However, since the number of permutations is usually not manageable, a good alternative is to only add the generators of the permutation group. It is also important to add permutations with a support as small as possible.

Todo

(user): Currently this can only be called before PropagateNext() is called (DCHECKed). Not sure if we need more incrementality though.

Definition at line 45 of file symmetry.cc.

num_permutations()

int operations_research::sat::SymmetryPropagator::num_permutations ( ) const

inline

Definition at line 92 of file symmetry.h.

operator=()

SymmetryPropagator & operations_research::sat::SymmetryPropagator::operator= ( const SymmetryPropagator & )

delete

Permute()

void operations_research::sat::SymmetryPropagator::Permute	(	int	index,
		absl::Span< const Literal >	input,
		std::vector< Literal > *	output ) const

Visible for testing.

Permutes a list of literals from input into output using the permutation with given index. This uses tmp_literal_mapping_ and has a complexity in O(permutation_support + input_size).

Initialize tmp_literal_mapping_ (resize it if needed).

Permute the input into the output.

Clean up.

Definition at line 201 of file symmetry.cc.

Propagate()

bool operations_research::sat::SymmetryPropagator::Propagate ( Trail * trail )

finalvirtual

Inspects the trail from propagation_trail_index_ until at least one literal is propagated. Returns false iff a conflict is detected (in which case trail->SetFailingClause() must be called).

This must update propagation_trail_index_ so that all the literals before it have been propagated. In particular, if nothing was propagated, then PropagationIsDone() must return true.

Implements operations_research::sat::SatPropagator.

Definition at line 135 of file symmetry.cc.

Reason()

absl::Span< const Literal > operations_research::sat::SymmetryPropagator::Reason ( const Trail & , int , int64_t  ) const

finalvirtual

Explains why the literal at given trail_index was propagated by returning a reason for this propagation. This will only be called for literals that are on the trail and were propagated by this class.

The interpretation is that because all the literals of a reason were assigned to false, we could deduce the assignment of the given variable.

The returned Span has to be valid until the literal is untrailed. A client can use trail_.GetEmptyVectorToStoreReason() if it doesn't have a memory location that already contains the reason.

If conlict id is positive, then this is called during first UIP resolution and we will backtrack over this literal right away, so we don't need to have a span that survive more than once.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 156 of file symmetry.cc.

Untrail()

void operations_research::sat::SymmetryPropagator::Untrail ( const Trail & , int trail_index )

finalvirtual

Reverts the state so that all the literals with a trail index greater or equal to the given one are not processed for propagation. Note that the trail current decision level is already reverted before this is called.

Todo

(user): Currently this is called at each Backtrack(), but we could bundle the calls in case multiple conflict one after the other are detected even before the Propagate() call of a SatPropagator is called.

Todo

(user): It is not yet 100% the case, but this can be guaranteed to be called with a trail index that will always be the start of a new decision level.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 143 of file symmetry.cc.

---

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

• ortools/sat/symmetry.h
• ortools/sat/symmetry.cc