to_cnf: to CNF encoding of cardinality constraints

[sourdough-bread]

b, x, y, z = boolvar(4)
c1 = b.implies(x+y+z <=1)
c2 = ~b | (x+y+z <=1)

The implication c1 is translated to an OR constraint in to_cnf(c1):

[(~BV0) or (sum([BV1, BV2, BV3]) <= 1)]

and c2is decomposed in to_cnf(c2) as:

[(~BV0) or (BV4),
 (sum([BV1, BV2, BV3]) > 1) or (BV4),
 (~BV4) or (sum([BV1, BV2, BV3]) <= 1)]

potentially introducing a loop.

[JoD]

Where exactly do you see the potential loop?

[sourdough-bread]

Where exactly do you see the potential loop?

c2 = ~b | (x+y+z <=1)

is the same expression as

(~BV4) or (sum([BV1, BV2, BV3]) <= 1)]

Which means there is no decomposiiton of the c2 constraint. If it's already in CNF, it should return the c2 constraint instead of creating extra constraint:

(~BV0) or (BV4),
 (sum([BV1, BV2, BV3]) > 1) or (BV4)

[tias]

There might be something bigger at play.

bv0 = boolvar()
bvs = boolvar(3)
Model(bv0 | Xor(bvs)).solve("ortools")

does not work either. The 'Xor' global constraint is not flattened. For any solver.

Fixing that might also fix the c2 = ~b | (x+y+z <=1) case.

(note that the above was sidestepped in #204 by adding globalconstraint decomp in to_cnf, but so the problem is deeper)

[tias]

what I reported was a different issue I now realize, which is also resolved in the mean time.

@sourdough-bread the derivation of c2 follows the CNF rules:

~b | (x+y+z <=1) is translated into [~b | auxbv, auxbv == (x+y+z <=1)] with the double reification split into [~b | auxbv, auxbv -> (x+y+z <=1), auxbv <- (x+y+z <=1)] with the latter one flipped to a right-pointing implication [~b | auxbv, auxbv -> (x+y+z <=1), ~auxbv -> (x+y+z > 1)] and then both implications converted to a disjunction.

But in this last step, converting an implication to a disjuntion, it is indeed creating a new expression that is the same as the original one, so if that expression is supported why would it translate the original one in the first place...

I guess this shows that our 'to_cnf' is applying the last rule too aggressively. It should not translate implications to a global constraint to a disjunction, only implications to logical constraint?

Then the output would be [~b | auxbv, auxbv -> (x+y+z <=1), ~auxbv -> (x+y+z > 1)]

Is that OK for you?

(if you don't even want that, then there should be a rewrite rule that rewrites the original disjunction into an implication, but that is a different kind of request)

[tias]

fixed by #223