Identify boolean function that satisfies some constrains The problem
I want to find a boolean function $f(x,y):\{0,1\}^n \rightarrow \{0,1\}$, where $x=\{x_i\}_{i=1}^{m}$ and $y=\{y_i\}_{i=1}^{k}$ are $m$ and $k$ boolean variables, such that:

*

*$m,k \ge 1$ (so at least one variable in each category)

*$f(x,y)=\begin{cases}
        1, & \text{for } \sum_{i=1}^{m} x_i \ge \sum_{i=1}^{k} y_i, \text{ with } \sum_{i=1}^{m} x_i \ne 0\\
        0, & \text{otherwise}
        \end{cases}$
So, $f$ get to be active only when the number of active $x$'s are equal or more than the active $y$'s, given that at least one of the $x$'s is active.
This covers also the trivial case of:
$\sum_{i=1}^{m} x_i = \sum_{i=1}^{k} y_i = 0 \rightarrow f(x,y)=0$ (when all variables are zero, result is zero)
I search for a parametric boolean formula, i.e. one that connects the various variables with any logical operators in some order, no matter the $m,k$.
Note that if the formula's condition is a strict equality $(\sum_{i=1}^{m} x_i \gt \sum_{i=1}^{k} y_i)$, and this is an easier problem, it's still acceptable.
And it makes more sense to me to include all variables in the formula of $f$.
What I've tried
No spotaneous idea came to my mind and so I thought to start with small examples and by computing the DNF forms from the truth tables, maybe I will start seeing some patterns.
I have some cases written here:

*

*$m=k=1$
x1 | y1 | f
-----------  
0  | 0  | 0  
0  | 1  | 0
1  | 0  | 1
1  | 1  | 1

$f=x1$. No $y1$ at all here!


*$m=1,k=2$
x1 | y1 | y2 | f  
----------------  
0  | 0  | 0  | 0  
0  | 0  | 1  | 0  
0  | 1  | 0  | 0  
0  | 1  | 1  | 0  
1  | 0  | 0  | 1  
1  | 0  | 1  | 1  
1  | 1  | 0  | 1  
1  | 1  | 1  | 0  

$f=(x1$ AND NOT $y1)$ OR $(x1$ AND NOT $y2)$. Nice. Seems like a pattern.


*$m=2,k=1$
x1 | x2 | y1 | f  
----------------  
0  | 0  | 0  | 0  
0  | 0  | 1  | 0  
0  | 1  | 0  | 1  
0  | 1  | 1  | 1  
1  | 0  | 0  | 1  
1  | 0  | 1  | 1  
1  | 1  | 0  | 1  
1  | 1  | 1  | 1  

$f=(x1$ OR $x2)$. No $y1$ again.

Maybe it can be proven that no such boolean function exists?
If that is the case, I believe there should be an approximation function, i.e. a boolean function whose results are as close as possible to the ideal one that I am asking for? How to find the best possible one in this case? Could it be the one I saw in the examples above, i.e. $f=\bigwedge\limits_{i,j=1}^{m,k} (x_i$ AND NOT $y_j)$? How would someone prove that?
 A: A boolean function is simply a function on boolean variables that produces a boolean result. There is no requirement that it must built in a certain way.
However, if you insist that you want some chain of logical operators, for any fixed $m,k$ we can build such an $f$. Suppose for now that $m \ge k$.
Note that $x$ has at least as many active values as $y$, if and only if there is a way to match up the elements of $x$ with $y$ so that every active element of $y$ is matched with an active element of $x$. That is, if $x_i$ and $y_j$ are matched, then either $y_j = 0$ or $x_i = 1$, or in symbols, $y_j \implies x_i$.
To formalize this, define a pairing to be a set $P \subset \{1, \ldots, m\} \times \{1, \ldots k\}$ such if $(i, j), (r,s) \in P$, then $i = r \iff j = s$, and for all $1 \le j \le k$, there exists some $i$ such that $(i,j) \in P$. Let $\scr P$ be the set of all such pairings. If $p \in P \in \mathscr P$, denote its coordinates by $p = (i_p, j_p)$.
So $x$ has at least as many active elements as $y$ if and only if there exists a $P\in \scr P$ such that
$$\bigwedge_{p\in P} (y_{j_p} \implies x_{i_p})$$
That is, when
$$\bigvee_{P \in \mathscr P}\bigwedge_{p\in P} (y_{j_p} \implies x_{i_p})$$
is true. So $$f(x,y) = \bigvee_{P \in \mathscr P}\bigwedge_{p\in P} (y_{j_p} \implies x_{i_p})$$
When $m < k$, there are no pairings. Instead define a partial pairing as a tuple $(P, Q)$ where $P$ is a pairing of some $m$ elements of $\{1,\ldots, k\}$ with $\{0,\ldots, m\}$, and $Q$ is the set of $k-m$ indices that were not paired. Let $\scr Q$ be the set of partial pairings.
Now we can express
$$f(x,y) = \bigvee_{(P,Q) \in \mathscr Q}\left(\bigwedge_{p\in P} (y_{j_p} \implies x_{i_p})\wedge \bigwedge_{j \in Q} (\lnot y_j)\right)$$
<Edit>
The above only encodes $x$ having as many active values as $y$. To also encode that at least one value must be active, we have
$$f(x,y) = \left(\bigvee_{i=1}^m x_i\right) \wedge \left(\bigvee_{(P,Q) \in \mathscr Q}\left(\bigwedge_{p\in P} (y_{j_p} \implies x_{i_p})\wedge \bigwedge_{j \in Q} (\lnot y_j)\right)\right)$$
</Edit>
All this bit about pairings is just a way of expressing the short-hand notation that holds for every $m,k$. For a particular $m,n$, it is just a matter of listing every every possible pairing. For example, when $m = k = 2$, this is
$$f(x, y) = \left(x_1 \vee x_2\right) \wedge \left(\left[ (y_1 \implies x_1) \wedge (y_2 \implies x_2) \right] \vee  \left[(y_1 \implies x_2) \wedge (y_2 \implies x_1) \right]\right)$$
but as $m, k$ get larger, this quickly grows into a ridiculously long expression. But despite that, it still accurately represents $f(x,y)$.
There are undoubtedly simpler expressions that are equivalent. But what this shows is that it is always possible to express $f(x,y)$ in terms of logical operators. Which is something that is true of any boolean function.
<Edit> Adding a few simple examples.
To simplify the functions, I'm just doing "$x$ has at least as many active elements as $y$". To get the actual condition of the question, "and" the functions with $(x_1 \vee x_2 \vee \ldots \vee x_m)$.
If we match a set $a$ of three variables with set $b$ of two, there are $6$ possible pairings between them, each with one member of $a$ left over:
$$\begin{array}{c|ccc}
 & a_1 & a_2 & a_3\\
\hline
p_1 & b_1 & b_2 & - \\
p_2 & b_2 & b_1 & - \\
p_3 & b_1 & - & b_2 \\
p_4 & b_2 & - & b_1 \\
p_5 & - & b_1 & b_2 \\
p_6 & - & b_2 & b_1
\end{array}$$
If $a = x$ and $b = y$, then each pairing is represented by the expressions
$$\begin{array}{c|c}
p_1 & (y_1 \implies x_1) \wedge (y_2 \implies x_2) \\
p_2 & (y_2 \implies x_1) \wedge (y_1 \implies x_2) \\
p_3 & (y_1 \implies x_1) \wedge (y_2 \implies x_3) \\
p_4 & (y_2 \implies x_1) \wedge (y_1 \implies x_3) \\
p_5 & (y_1 \implies x_2) \wedge (y_2 \implies x_3) \\
p_6 & (y_2 \implies x_2) \wedge (y_1 \implies x_3)
\end{array}$$
When $x$ has the extra elements, it doesn't matter if they are active or not, so nothing has to be added for them.
When $x$ has more or equal active elements, at least one of these statements will be true, and vice versa. So the total condition is
$$\begin{align}f(x,y) =\ &[(y_1 \implies x_1) \wedge (y_2 \implies x_2)]\ \vee \\
&[(y_2 \implies x_1) \wedge (y_1 \implies x_2)]\ \vee \\
&[(y_1 \implies x_1) \wedge (y_2 \implies x_3)]\ \vee \\
&[(y_2 \implies x_1) \wedge (y_1 \implies x_3)]\ \vee \\
&[(y_1 \implies x_2) \wedge (y_2 \implies x_3)]\ \vee \\
&[(y_2 \implies x_2) \wedge (y_1 \implies x_3)]\end{align}$$
If $a = y, b = x$, so it is $y$ that has the unmatched elements, then it is necessary to guarantee that the unmatched elements are not active:
$$\begin{array}{c|c}
p_1 & (y_1 \implies x_1) \wedge (y_2 \implies x_2) \wedge \lnot y_3 \\
p_2 & (y_1 \implies x_2) \wedge (y_2 \implies x_1) \wedge \lnot y_3 \\
p_3 & (y_1 \implies x_1) \wedge \lnot y_2 \wedge (y_3 \implies x_2) \\
p_4 & (y_1 \implies x_2) \wedge \lnot y_2 \wedge (y_3 \implies x_1) \\
p_5 & \lnot y_1 \wedge (y_2 \implies x_1) \wedge (y_3 \implies x_2) \\
p_6 & \lnot y_1 \wedge (y_2 \implies x_2) \wedge (y_3 \implies x_1)
\end{array}$$
And again, we "or" the various pairings together to get the full function:
$$\begin{align}f(x,y) =\ &[(y_1 \implies x_1) \wedge (y_2 \implies x_2) \wedge \lnot y_3]\ \vee \\
&[(y_1 \implies x_2) \wedge (y_2 \implies x_1) \wedge \lnot y_3]\ \vee \\
&[(y_1 \implies x_1) \wedge \lnot y_2 \wedge (y_3 \implies x_2)]\ \vee \\
&[(y_1 \implies x_2) \wedge \lnot y_2 \wedge (y_3 \implies x_1)]\ \vee \\
&[\lnot y_1 \wedge (y_2 \implies x_1) \wedge (y_3 \implies x_2)]\ \vee \\
&[\lnot y_1 \wedge (y_2 \implies x_2) \wedge (y_3 \implies x_1)]\end{align}$$
<\Edit>
