Solve the following exercise by means of a reduction to SAT:

• Given a network (an undirected graph) $G_1$ and a larger network $G_2$, determine if we can find an injective mapping from the nodes of $G_1$ to the nodes of $G_2$ such that at least $k$ edges of $G_1$ are aligned to edges in $G_2$. We say that an edge is aligned if the image of its adjacent nodes are adjacent in $G2$.

The input of the exercise and the output with the solution (when the input is solvable) are as follows:

• n1: int
  n2: int
  E1: array of array [2] of int
  E2: array of array [2] of int
  k: int
  

  The input contains the numbers $n_1,n_2$ of nodes and the lists $E_1,E_2$ of edges of the graphs $G_1$ and $G_2$, respectively, with $n_1\leq n_2$, and the number $k$ of edges that must be aligned. Each edge of the graph $G_i$ appears in the list $E_i$ exactly once, with the nodes in no particular order, nodes being identified with a number in $\{0,\ldots,n_i-1\}$.

• mapping: array of int
  

  The output is an array mapping where its $i$’th position denotes the node of $G_2$ assigned to the node $i$ of $G_1$. The array should contain $n_1$ elements, each with a value in $\{0,\ldots,n_2-1\}$, without repeated entries.