search

zkFold / zkfold-base

ZkFold's Base library
https://zkfold.io
MIT License
17 stars 7 forks source link

Deeper boolean optimization #271

Open TurtlePU opened 2 months ago

TurtlePU commented 2 months ago

A special case of #270 is the case of variables which are evidently boolean.

For example, if we know that x && y == 1, this means that x == 1 and y == 1.

The problem with boolean optimization is that we should somehow mark variables as boolean. Sure, some of them can be found by looking for constraints of a kind x * (x - 1) == 0, but, for example, the isZero bit from runInvert algorithm is constrained in a more roundabout fashion.

So is there an algorithm which would detect boolean variables? Or do we introduce a separate function markBoolean :: MonadCircuit var a m => var -> m () to mark them by hand?

vlasin commented 2 months ago

Hmm, in the example, x :: Bool c, I assume.

If so, then x && y == 1 requires just one constraint, while x == 1 and y == 1 means you are adding two. The latter is basically an application of forceOne to x and to y. The former is how it currently works: it already assumes the booleanness of the variables.

TurtlePU commented 2 months ago

x && y == 1 is actually two constraints and a variable:

$$\begin{cases} x y - z = 0 \ z - 1 = 0 \end{cases}$$

While x == 1 and y == 1 are two constraints which can be optimized further.

vlasin commented 2 months ago

Yeah, you are right!