Application of SAT solvers to the problem of finding vector Boolean functions with required cryptographic properties

We propose a method for finding an almost perfect nonlinear (APN) function. It is based on translation into SAT-problem and using SAT-solvers. We construct several formulas defining the conditions for finding an APN-function and introduce two representations of the function: Sparse and dense, which are used to describe the problem of finding one-to-one vectorial Boolean functions and APN-functions. We also propose a new method for finding a vectorial APN-function with additional properties. It is based on the idea of representing an unknown vectorial Boolean function as a sum of known APN-functions and two unknown Boolean functions: $\mathbf{G} = \mathbf{F}\oplus \mathbf{c}\cdot g_1 \oplus \mathbf{d}\cdot g_2$, where $\mathbf{F}$ is a known APN-function. It is shown that this method is more efficient than the direct construction of APN-function using SAT for dimensions 6 and 7. As a result, the method described in the work can prove the absence of cubic APN-functions in dimension 7 representable in the form of the sum described above. Tab. 3, bibliogr. 21.