Convert sum of $N$ bits, $k$ shift right, to propositional formula. This problem is somehow related to multiplication circuits
Input: $N$ bits, integer $K$

*

*Output: a propositional formula that is satisfiable if and only if the sum of the bits, K shift right mode 2 equals 1

Example:

*

*N = {1,0,1,1}, K = 1 -> output = 1

*N = {1,1,1,1}, K = 1 -> output = 0

*N = {1,1,1,1}, K = 2 -> output = 1


I found an exponential solution for it, I hope that other answers will come out with something more efficient or prove that it is hard to find a better answer.
I will start with the example of N = {1,0,1,1}, K = 1. It's easy to solve it on the paper by summing those numbers and deleting the last digit. $1+0+1+1 = 11$, and deleting the last digit gives $1$.
Since it is a sum, the order of the digits is not important, the only thing that matters is the number of $1$`s, so we can look at the truth table of all the possibilities and concatenate it with $\lor$:
$$(i_1 \land i_2 ...\land i_n) \lor (i_1 \land i_2 ...\land i_n) \lor (i_1 \land i_2 ...\land i_n)...$$
All the $i$ that represent zeroes should also be prefixed with $\lnot$
For example N = 3, K = 1

*

*000 -> false

*001 -> false

*010 -> false

*011 -> true

*100 -> false

*101 -> true

*110 -> true

*111 -> true

Taking all the truth results gives:
$$(\lnot i_1 \land i_2 \land i3) \lor (i_1 \land \lnot  i_2 \land i3) \lor (i_1 \land i_2 \land \lnot i3) \lor (i_1 \land i_2 \land i3)$$
We can quickly calculate how many different counts of 1 we can have with $N$ bits that will yield a satisfactory result, there are a total of $N$ possibilities. For each possibility with $P$ $1$ bits, there are $\frac{N!}{P!(N-P)!}$ combinations. We can make a small optimization and instead of count $1$ combinations count $0$ combinations and negate the final result, but still, the final result is exponentially large.
