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

 A: If your formula can contain additional helper propositional variables, it can be reduced to a polynomial length relatively easily.
In addition to the inputs $i_1,i_2,\ldots, i_n$ we are going to use $(n+1)^2$ helper variables named $\Sigma_{f,t}$ with $f$ and $t$ ranging between $0$ and $n$ (inclusive). Our formula will be a long conjunction of four types of expressions (where $\bar{x}$ denotes negation):

*

*$\left(\Sigma_{0,0} \land \bar\Sigma_{0,1} \land\ \ldots \land \bar\Sigma_{0,n}\right)$ where all terms apart from the first one are negated,

*$\left(\Sigma_{f,0} \iff \Sigma_{f-1,0} \land \bar{i_f}\right)$ for $1\leq f\leq n$,

*$\left(\Sigma_{f,t} \iff \left(\Sigma_{f-1,t} \land \bar{i_f}\right)\lor \left(\Sigma_{f-1,t-1} \land i_f\right)\right)$ for $1\leq f\leq n$ and $1\leq t\leq n$,

*Disjunction of all $\Sigma_{n,t}$ such that $K$-th right-most bit of $t$ is $1$.

The variables $\Sigma_{f,t}$ represent the statements: $\sum\limits_{k=1}^f i_k = t$ and the first three bullet-points determine their truth-values  completely based on the assignment of $\{i_k\}$. The fourth point then makes the formula satisfiable if and only if the sum of all $n$ values satisfies the shift-right-by-k-modulo-2-equals-1 condition.
Of course, some of the variables are completely useless (such as those with $t>f$, since the sum of first $f$ terms cannot exceed $f$). Also, if $k$ was small enough, we could avoid computing the full sum but only get its value modulo $2^{k+1}$; instead of $0\leq t\leq n$, we would only have $0\leq t<2^{k+1}$ (which would actually make the expressions a little more uniform).
A: 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.
