Your problem is NP-complete.
I prove NP-hardness below by reduction from the clique problem (given a graph and a number, does the graph have a clique of that many vertices).
reduction
Suppose we are given a clique instance consisting of a graph $G = (V, E)$ with $m = |E|$ and $n = |V|$ and a number $k$. Then we will produce an instance of your problem consisting of a formula $\phi$ and a number $K$ as described below
First of all, we set $K = k + (n+1) \times {k \choose 2}$.
Next, lets describe the variables used in $\phi$. For each vertex $v \in V$, $\phi$ will include a variable $x_v$. For each edge $e \in E$, $\phi$ will include $n+1$ variables: $y_e^0, y_e^1, \ldots, y_e^n$.
Finally, lets describe the clauses included in $\phi$. Each clauses has the form $(a \vee \neg b)$, which is logically equivalent to $(b \to a)$, so I will write all clauses in implication form. For each edge $e \in E$, we include clauses $(y_e^n \to y_e^0)$, $(y_e^0 \to y_e^1)$, $(y_e^1 \to y_e^2)$, ..., and $(y_e^{n-1} \to y_e^n)$. The effect of these clauses is to enforce the equality of all the $y_e^i$s (for any fixed $e$) in any satisfying assignment. Next, for any edge $(u, v) \in E$, we also include clauses $(y_{(u,v)}^0 \to x_u)$ and $(y_{(u,v)}^0 \to x_v)$. The effect of these clauses is that in any satisfying assignment, if the variables $y_{(u,v)}^i$ associated with an edge are true then the variables $x_u$ and $x_v$ associated with the endpoints must also be true.
clique $\to$ satisfying assignment
Suppose that there is a clique $C$ of size $k$ in $G$. Then we can create a satisfying assignment for $\phi$ with exactly $K = k + (n+1) \times {k \choose 2}$ true variables.
In particular, for $v \in V$, set $x_v$ to true iff $v \in C$, and for $e \in E$, set $y_e^i$ to true iff both endpoints of $e$ are in $C$.
There are $n+1$ variables $y_e^i$ for each $e$, and there are exactly $k \choose 2$ edges in $G$ with both endpoints in $C$ (since $C$ is a clique). Thus there are $(n+1) \times {k \choose 2}$ variables of the form $y_e^i$ that are set to true under this assignment. Furthermore, $|C| = k$, so there are exactly $k$ variables of the form $x_v$ set to true under this assignment. As desired, this assignment has exactly $K = k + (n+1) \times {k \choose 2}$ true variables.
Notice that $y_e^i = y_e^j$ for every edge $e$ and pair of indices $i, j$. Thus, the clauses of the form $(y_e^i \to y_e^{(i+1)~\text{mod}~(n+1)})$ are satisfied under this variable assignment.
Next, consider any edge $(u, v)$. If $y_{(u, v)}^0$ is true, then both $u$ and $v$ are vertices in $C$, so therefore both $x_u$ and $x_v$ are also true. Thus, clauses $(y_{(u,v)}^0 \to x_u)$ and $(y_{(u,v)}^0 \to x_v)$ are also satisfied.
Since all clauses are satisfied, this is a satisfying assignment (which we already noted has exactly $K$ true variables).
satisfying assignment $\to$ clique
Next suppose we have a satisfying assignment of $\phi$ with exactly $K = k+ (n+1) \times {k \choose 2}$ true variables.
Any satisfying assignment has $y_e^0 = y_e^1 = \cdots = y_e^n$. Then let $y_e = y_e^0$. Define $n_y$ to be the number of true $y_e$s. Similarly, define $n_x$ to be the number of true $x_v$s. Notice that the number of true variables in the assignment is equal to $n_x + (n+1) \times n_y$. Furthermore, $0 \le n_x < n+1$ since there are only $n$ different $x_v$s. Thus, we can conclude that $n_x = K~\text{mod}~(n+1) = k$ and $n_y = \lfloor \frac{K}{n+1} \rfloor = {k \choose 2}$.
Let $C = \{v \in V~|~x_v~\text{is true}\}$ and let $E' = \{e \in E~|~y_e~\text{is true}\}$. Note that $|C| = n_x$ and $|E'| = n_y$ by definition. Then $E'$ is a set of ${k \choose 2}$ edges, and $C$ is a set of $k$ edges.
Notice that if $(u,v) \in E'$, then $y_{(u,v)}$ is true, and therefore $y_{(u,v)}^0$ is true; as a result, since clauses $(y_{(u,v)}^0 \to x_u)$ and $(y_{(u,v)}^0 \to x_v)$ must be satisfied, we can conclude that $x_u$ and $x_v$ are also true, and therefore that $u,v \in C$. Thus, if $e \in E'$ and $v$ is an endpoint of $e$ then $v \in C$.
Thus the set of endpoints of edges in $E'$ is a subset of $C$. Then $E'$ is a set of ${k \choose 2}$ edges whose set of endpoints numbers at most $|C| = k$. A set of ${k \choose 2}$ edges has only $k$ endpoints in total only in the case that the $k$ endpoints are a clique. In other words, it must be the case that $C$ is a clique and the edges in $E'$ are the edges in the clique.
Thus we have identified a clique of size $k$ in $G$.
