Yes, any such pair can be separated by a formula of size $O(n)$. More generally, any disjoint pair $P,N\subseteq\{0,1\}^n$ of size $s=|P|+|N|$ can be separated by a decision tree of size $O(s)$, which can be implemented as an $O(s)$-size formula by replacing each query node with $(p\land\cdots)\lor(\neg p\land\cdots)$.
It suffices to observe that there exists a decision tree such that every path to a leaf is consistent with exactly one element of $P\cup N$ (which means that it has $s$ leaves and $s-1$ inner nodes). One way to show this is to consider the full binary tree of height $n$ that queries all variables along every path, take its subtree consisting of the union of paths to leaves in $P\cup N$, and eliminate inner nodes that do not branch.
Another way is to build it inductively. Start with the trivial one-element decision tree, and repeat: pick a leaf $x$ that is consistent with $\ge2$ elements of $P\cup N$, and make $x$ into a query node for some variable $p$ such that each of the $p$ and $\neg p$ branches is still consistent with an element of $P\cup N$. Notice that this actually gives a polynomial-time algorithm to construct the decision tree, given $P$ and $N$.
[The first version of this answer presented a different construction, using a linear hash function $h\colon\mathbb F_2^n\to\mathbb F_2^{O(\log s)}$ such that $h(P)\cap h(N)=\varnothing$. This only gives a separating circuit of size $O(n\log n)$, or $O((n+s_0)\log s)$ in the general case, where $s_0=\min\{|P|,|N|\}$.]
For $s\le n$, the $O(s)$ bound is optimal up to a multiplicative constant: it is easy to see that any circuit separating $P=\{0^n\}$ from $N=\{0^i10^{n-1-i}:i<s-1\}$ must
include all of the first $s-1$ variables, and as such it has size at least $s$.
For larger $s$, an optimal bound is given by Theorem 1.1 of Andreev, Clementi, and Rolim [1] (with $\varepsilon=1/2$): the maximum circuit size required to separate $P,N\subseteq\{0,1\}^n$ with $|P|+|N|=s$ is
$$\Theta\left(\frac s{\log s}\right)+O(n).$$
They do not seem to particularly care about the case of small $s$, but combined with the discussion above, we obtain the following complete characterization:
Theorem: The maximum circuit size required to separate disjoint pairs $P,N\subseteq\{0,1\}^n$ with $|P|+|N|=s$ is
$$\begin{cases}\Theta\left(\frac s{\log s}\right)&\text{if }n\log n\le s,\\
\Theta(n)&\text{if }n\le s\le n\log n,\\
\Theta(s)&\text{if }s\le n.\end{cases}$$
And while it does not yield improvement on any of the above, let me mention the following fun fact: for every nonempty $X\subseteq\{0,1\}^n$ of size $s=|X|$, there exists $I\subseteq[n]$ of size $|I|<s$ such that the restrictions $x\restriction I\in\{0,1\}^I$ of the elements $x\in X$ are pairwise distinct. To see this, fix $I$ of minimal size with this separation property. For each $i\in I$, the minimality of $I$ implies that there exist $x_i,y_i\in X$ such that $x_i\restriction I$ and $y_i\restriction I$ differ only at the $i$-th position. Put $E=\{\{x_i,y_i\}:i\in I\}$. Then $(X,E)$ is a graph with $s$ vertices and $|I|$ edges, and it is acyclic (if we start from a $\{0,1\}$ vector, and flip a sequence of distinct bits, we cannot arrive where we started from). Thus, $s>|I|$.
Reference:
[1] Alexander E. Andreev, Andrea E. F. Clementi, José D. P. Rolim: Optimal bounds for the approximation of boolean functions and some applications, Theoretical Computer Science 180 (1997), no. 1–2, pp. 243–268, doi: 10.1016/S0304-3975(96)00217-4.
