Additional constraint generated during transformation of choice rules

[rtaupe]

In addition to the two normal rules encoding a choice rule, ChoiceHeadToNormal now also generates a constraint that forbids the two complementary head literals to be true at the same time. The constraint helps propagation and thus potentially improves solving performance. It can be grounded at the same time as the choice rule itself if constraints are grounded permissively (with gtc >= 2 since the body of the constraint contains two literals more than the body of the choice rule).