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

• A DNA strand is a sequence of amino acids, each of which can be Adenine (A), Cytosine (C), Guanine (G), or Thymine (T). Given two DNA strands, we have to insert gaps in the shortest sequence until both have the same length, in a way that most of the positions have the same amino acid in both sequences. In particular, we want to see if we can find one such alignment in which at least $k$ of the amino acids match.

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

• strand1: array of int
  strand2: array of int
  k: int
  

  The DNA strands are in strand1 and strand2, the second one being the (strictly) shortest sequence. Each position of the strands (starting at $0$) contains a number identifying an amino acid, according to the following table:

     A   0
     C   1
     G   2
     T   3
  

  Finally, the number k, with k${}\leq{}$strand2.size, is the least number of amino acids that must match.

• alignment: array of int
  

  The output consists of an array alignment of size strand2.size indicating, for each amino acid in the second strand, its index after adding the gaps. For instance, if the strands were:

     strand1 = ACGTACGT
     strand2 = ATAT
  

  and we added the following gaps:

     strand1  = ACGTACGT
     strand2' = A··TAT··
  

  Then the output should be:

     alignment = 0 3 4 5
  

Note: this problem can be solved in asymptotic polynomial time without reducing to SAT.