Symmetry breaking is broken
Issue #225
resolved
Commit [[https://bitbucket.org/broesdecat/idp/changeset/421f028bb801|421f028bb801]] inserted a bug. Now 6 symmetrybreaking tests find too many models!
Comments (3)
-
-
reporter It should be solved as follows:
- In case that the user asks only for one model, you can make the "smart" transformation where the tseitins are relaxed.
- In other cases, you should make the strict transformation
(use the boolean nbmodelsequivalent from the groundinginference to check for this)
-
- changed status to resolved
Made symmetry breaking aware of the _nbModelsEquivalent boolean. Fixes issue 225: symmetry-breaking-is-broken
- Log in to comment
The new symmetry breaking clauses relax the constraints on their tseitin variables. Each model may have multiple combinations of tseitin assignments which satisfy the symmetry breaking clauses. The returned models hence are often the exact same model, but with different tseitin assignments. Anyone got any pointers on how to fix this (aka: how to make the solver ignore tseitins when eliminating found models)?