Different satisfiability results for minicard and minicard_encodings (and minicard_simp_encodings)

[chivdan]

For the attached CNF+ variant.zip minicard reports UNSAT while minicard_encodings and minicard_simp_encodings (with all cardinality encodings) report SAT.

[liffiton]

Thanks for the report and the test case! I see you're using repeated literals in your cardinality constraints. I added support for that to the main solver, but I don't think I ever thought about the encodings when I did that, as they were mostly created for comparison purposes and not for end use. My guess is that the encodings are giving spurious results here.

When I look at the satisfying assignment produced by encoding 6 (pairwise, which doesn't produce extra variables and so its models are the easiest to inspect), I think I've found evidence of that. 1286 through 1294 are FALSE while 1385 is assigned TRUE, which violates the constraint

-1285 -1286 -1287 -1288 -1289 -1290 -1291 -1292 -1293 -1294 1385 1385 1385 1385 1385 1385 1385 1385 1385 1385 <= 10

Can you check my result and my thinking there?

If I'm right, and the encodings aren't able to handle repeated literals, then I will add a note to the README warning of that at least. I'm not sure I will have the time to add that ability to the encodings.

[And incidentally, I'm pleasantly surprised to learn that someone is using Minicard. If you wouldn't mind emailing me a bit about how you're using it, I'd really appreciate it!]