Symmetry breaking is broken

[Bart Bogaerts]

Commit [[https://bitbucket.org/broesdecat/idp/changeset/421f028bb801|421f028bb801]] inserted a bug. Now 6 symmetrybreaking tests find too many models!

[JoD]

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)?

[Bart Bogaerts]

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)

[JoD]

Made symmetry breaking aware of the _nbModelsEquivalent boolean. Fixes issue 225: symmetry-breaking-is-broken

→ 2c05b0ff62f0