Name this satisfiability problem? I've got a specific problem, but I'm not sure where to look to solve it:

In the context of my application, there are critical services, non-critical services, and agents which provide exactly one critical service and one or more non-critical services. I must choose from the collection of all agents (with replacement) a finite number of agents, such that each critical service is provided by a certain number of agents. This is straightforward. However, I have the secondary objective that I would like the set I choose to also provide as many different non-critical services as possible.

I'm sure this can be done via SAT, but I don't really want to mess around with NP-complete solvers. The goal for either kind (critical or not) of the services could be constructed as a network flow problem and solved in a straightforward way, but I can't seem to merge them, even as a multi-commodity network flow.

Has anyone seen this problem before, or something embarrassingly similar? I'd really appreciate a pointer to where I could start looking for solutions.

-- David
Let $k$ be the finite number of agents you're allowed to choose. If there are no critical services, finding the set of $k$ agents that maximize the number of non-critical services provided is equivalent to Max-$k$-Cover, which can't be approximated better than $1-1/e$ unless P=NP. So for an exact solution, you'll have to use something capable of solving NP-hard problems.

If you'd be happy with an approximation, you're in luck. The constraint that you have to choose $k$ agents such that there are sufficiently many of them providing each service is a matroid constraint. This paper shows how to achieve a $1-1/e$ approximation on set cover problems under a matroid constraint.

If you want something simpler to implement, the matroid greedy algorithm gives a $1/2$ approximation on submodular set functions. So you just need to repeatedly choose the agent that provides the most new non-critical services, after at each step removing from consideration any agent whose choice would prevent you from providing enough of each critical service before reaching $k$ agents. If each agent provides unique non-critical services, you're just maximizing a weight function over a matroid, so the greedy algorithm gives an exact solution.