SAT formula specifying that exactly $k$ of $N$ boolean variables are active using less than $N$-choose-$k$ terms Is there a way to express the condition that exactly $k$ of $N$ boolean variables are active without writing a disjunction of $N$-choose-$k$ terms, i.e., all possible configurations of the $N$ variables where exactly $k$ are active? Is the same true for specifying that at least $K$ of the $N$ boolean variables are active?

I'm aware that this is a problem dealt with in theoretical computer science but I couldn't find any references.
There are many ways.  See Encoding 1-out-of-n constraint for SAT solvers for a compendium of several ways and for a useful reference with more information.

From a practical perspective, the different schemes have different tradeoffs.  If you are trying to encode a $k$-out-of-$N$ constraint in something you are feeding to a SAT solver, you can try each of the different candidate encodings to see which makes the SAT solver run faster; they can have a significant impact on the efficiency of the SAT solver.