How would i write constraints for this, given variables a and b, put 1 in variable c if a != b else put 0. a and b are not boolean. I need this proving that only n variables in 2 lists (of equal length) of variables are different where n is a public value.

(1 - c) Ă (c) = 0 // c is boolean
(a - b) Ă (Î») = (c) // a = b â c = 0
(ÎŒ) Ă (c) = (a - b) // a â b â c â 0

If you only need to prove that at most n pairs of variables are different, then itâs only 2 constraints per pair because you only need the first and third constraints above.

Similarly, for at least n different, you only need the first and second constraints.

Thanks @daira. How would the prover set Î» and ÎŒ? Î» = (a - b)^{-1} (0 when a == b) and ÎŒ = Î»^{-1} which is (a - b)?
You can do this with 2 constraints as i found this in the Pinocchio paper on page 7, under Zero-Equality Gate. The constraints for Y = (X! = 0)?1 : 0 are:

X Ă M â Y = 0
(1 â Y) Ă X = 0

Now Y cannot be anything other than 0 or 1. We set X to a - b, M to be (a - b)^{-1}, then Y is c.

Regarding âat least n pairs of variables are differentâ, for the r pairs that are equal with r >= n, the prover sets Î» = (a - b)^{-1} for n equal pairs and for the remaining r - n pairs, sets Î» = 0.
Donât follow the " at most n pairs" argument

Ah ok, yes that looks correct. The first constraint enforces X = 0 â Y = 0, and the second enforces X â 0 â Y = 1.

Never mind what I said about the âat leastâ and âat mostâ optimizations; they canât be combined with the two-constraint zero-equality gate, and so they donât help. (The reason they canât be combined is that each of the two zero-equality gate constraints alone doesnât enforce booleanity of Y.)

Are the âat leastâ and âat mostâ optimizations possible in the 3 constraint case? Or do we need a different approach where we do a range check on n?

Yes, the former. For example, for âat most n are differentâ, if we do this for each pair:

(1 - c) Ă (c) = 0 // c is boolean
(ÎŒ) Ă (c) = (a - b) // a â b â c â 0

then for pairs that are different we must have c = 1, and for pairs that are the same we can choose either c = 0 or c = 1. So we can arbitrarily pick m - n of the pairs that are the same and set c = 0 for those; then set c = 1 for all the other (n) pairs. Then the sum of the câs will be n.

Similarly for âat least n are differentâ, we do this for each pair:

(1 - c) Ă (c) = 0 // c is boolean
(a - b) Ă (Î») = (c) // a = b â c = 0

then for pairs that are the same we must have c = 0, and for pairs that are different we can choose either c = 0 or c = 1. So we can arbitrarily pick n of the pairs that are different and set c = 1 for those; then set c = 0 for all the other (m - n) pairs. Then the sum of the câs will be n.

Incidentally, thereâs no need for a separate constraint to prove that the sum is n (in any of the three cases). Just substitute n - âc_{1âŠm-1} for all occurrences of c_{0}.