C++ Reference: class SymmetryPropagator
Note: This documentation is automatically generated.
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 that if it is already assigned to false, then we have a conflict.
TODO(user): Implement the optimizations mentioned in the paper? TODO(user): Instrument and see if the code can be optimized.
| Method | |
|---|---|
AddSymmetry | Return type: Arguments: 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. |
num_permutations | Return type: |
Permute | Return type: Arguments: 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). |
Propagate | Return type: Arguments: |
Reason | Return type: Arguments: |
SymmetryPropagator | |
~SymmetryPropagator | |
Untrail | Return type: Arguments: |