Based on earlier feedback, I'm creating this thread to advertise questions on CS.SE that would be interesting to this community and haven't received an answer.

Guidelines:

1. Each answer should link directly to a single question on CS.SE that has not been adequately answered and that would be of interest to this community. In particular, the question should be research-level and related to theoretical computer science. Also, make sure the question has remained open on CS.SE for a significant period of time with no answer (say, at least two weeks). Don't re-post a question that's an already well-known open problem or has already been re-posted on CSTheory.SE.

2. Each answer should include a short summary of the question asked. There's no need to repost the CS.SE question verbatim, but it should be fairly clear what the question is about without following the link.

3. Feel free to downvote and vote-to-delete suggestions that aren't "up to snuff".

4. Don't abuse this thread. Abusing this thread is an easy way to ensure it is closed/deleted. This thread will stay open only as long as the CSTheory community feels it serves a useful purpose. For instance, don't post links to CS.SE questions that are essentially homework exercises, not research level, or not within our scope.

The question can be seen as an assignment problem to SAT with only 2 literals for each variable, one negated and the other positive. The question asks what is the minimum subset of clauses that have $k$ or more satisfied literals in an assignment of the formula (not necessarily an assignment that satisfies the formula).