Prove NP-completeness of deciding satisfiability of monotone boolean formula I am trying to solve this problem and I am really struggling.

A monotone boolean formula is a formula in propositional logic where all the literals are positive. For example, 

$\qquad (x_1 \lor x_2) \land (x_1 \lor x_3) \land (x_3 \lor x_4 \lor x_5)$ 

is a monotone boolean function. On the other hand, something like

$\qquad (x_1 \lor x_2 \lor x_3) \land (\neg x_1 \lor x_3) \land (\neg x_1 \lor x_5)$ 

is not a monotone boolean function.

How can I prove NP-completeness for this problem: 


  Determine whether a monotone boolean function is satisfiable if $k$ variables or fewer are set to $1$? 


Clearly, all the variables could just be set to be positive, and that's trivial, so that is why there is the restraint of $k$ positively set variables.

I have tried a reduction from SAT to monotone boolean formula. One thing I have tried is to substitute a dummy variable in for every negative literal. For example, I tried replacing $\neg x_1$ with $z_1$, and then I tried forcing $x_1$ and $z_1$ to be different values. I haven't quite been able to get this to work though.
The "parent" of the problem you're looking at is sometimes called Weighted Satisfiability (WSAT, particularly in parameterized complexity) or Min-Ones (though this is normally an optimization version, but near enough). These problems have the "at most $k$ variables set to true" restriction as their defining feature.

The restriction to monotone formulae is actually surprisingly easy to show hardness for, you just need to thing outside satisfiability problems for a moment. Instead of trying to modify a SAT instance, we instead start with Dominating Set (DS).

See if you can get it from there. More is in the spoilers, broken into bits, but avoid them if you can. I won't show membership in NP, you should have no problem with that.


   Given an instance $(G, k)$ of DS (i.e. we want a dominating set of size at most $k$ for $G$), we can construct an instance $(\phi,k)$ of WSAT where the formula $\phi$ is a monotone CNF formula:


The basic construction:


   For each $v\in V(G)$ we have a variable $v' \in \text{var}(\phi)$, for each $v \in V(G)$ we have a clause $c_{v} = \bigvee_{u\in N(v)} u'$.


A sketch of the proof:


  Each vertex either has to be in the dominating set, or have a neighbour that is, so if we can find $k$ vertices that form a dominating set, the corresponding $k$ variables can be set to true in $\phi$, and each clause must contain at least one of them. Similarly if there is a weight $k$ satisfying assignment, the true variables correspond to the vertices we place in the dominating set - every clause $c_{v}$ must have at least one, so each $v$ is dominated (by itself or otherwise).