Here is the problem. Given $k, n, T_1, \ldots, T_m$, where each $T_i \subseteq \{1, \ldots, n\}$. Is there a subset $S \subseteq \{1, \ldots, n\}$ with size at most $k$ such that $S \cap T_i \neq \emptyset$ for all $i$? I am trying to reduce this problem to SAT. My idea of a solution would be to have a variable $x_i$ for each of 1 to $n$. For each $T_i$, create a clause $(x_{i_1} \vee \cdots \vee x_{i_k})$ if $T_i = \{i_1, \ldots, i_k\}$. Then and all these clauses together. But this clearly isn't a complete solution as it does not represent the constraint that $S$ must have at most $k$ elements. I know that I must create more variables, but I'm simply not sure how. So I have two questions:

  1. Is my idea of solution on the right track?
  2. How should the new variables be created so that they can be used to represent the cardinality $k$ constraint?
  • 5
    $\begingroup$ Just a remark: Your problem is known as HITTING SET, which is an equivalent formulation of the SET COVER problem. $\endgroup$
    – A.Schulz
    Nov 7 '12 at 8:22

It looks like you are trying to compute a hypergraph transversal of size $k$. That is, $\{T_1,\dots,T_m\}$ is your hypergraph, and $S$ is your transversal. A standard translation is to express the clauses as you have, and then translate the length restriction into a cardinality constraint.

So use your existing encoding, i.e., $\bigwedge_{1 \le j \le m} \bigvee_{i \in T_j} x_i$ and then add clauses encoding $\sum_{1 \le i \le n} x_i \le k$.

$\sum_{1 \le i \le n} x_i \le k$ is a cardinality constraint. There are various different cardinality constraint translations into SAT.

The simplest but rather large cardinality constraint translation is just $\bigwedge_{X \subseteq \{1,\dots,n\}, |X| = k+1} \bigvee_{i \in X} \neg x_i$. In this way each disjunction represents the constraint $\neg \bigwedge_{i \in X} x_i$ - for all subsets $X$ of $\{1,\dots,n\}$ of size k+1. That is, we ensure that there is no way that more than k variables can be set. Note that this is not polynomial size in $k$

Some links to papers on more space-efficient cardinality constraint translations which are polynomial size in $k$:

If you are actually interested in solving such problems, perhaps it is better to formulate them as pseudo-boolean problems (see wiki article on pseudo-boolean problems) and use pseudo-boolean solvers (see pseudo-boolean competition). That way the cardinality constraints are just pseudo-boolean constraints and are part of the language - hopefully the pseudo-boolean solver then handles them directly and therefore more efficiently.

  • 1
    $\begingroup$ Please describe all links shortly (at least author and title) so people can find the documents should the links break. It's probably best to use DOI if available. $\endgroup$
    – Raphael
    Nov 7 '12 at 10:29
  • 1
    $\begingroup$ @Raphael Good point! Apologies I should have done that to begin with. I've now updated all the links; I'm not sure if Springer provide DOIs but there should be enough information now to find them if the links break. Note: I don't link to the official PDFs from Springer to avoid access problems. $\endgroup$
    – MGwynne
    Nov 7 '12 at 12:53
  • $\begingroup$ But it seems that the reduction you gave is not in polynomial time, right? $\endgroup$
    – Aden Dong
    Nov 7 '12 at 15:58
  • $\begingroup$ @AdenDong You said nothing about polynomial ;). The simple cardinality constraint translation I mention is not polynomial in $k$ (but is for fixed $k$). The cardinality constraint translations given in the papers I list are polynomial in $k$ - using new variables. I've updated my answer to make this clearer. $\endgroup$
    – MGwynne
    Nov 7 '12 at 16:46
  • $\begingroup$ MGwynne, I tend to always link the official DOI even if it is paywalled in order to be future-proof, and free versions additionally. But as it is now, anybody shoul be able to find the papers, so it's completely fine. $\endgroup$
    – Raphael
    Nov 7 '12 at 17:28

If you're not absolutely set on the normal SAT, your idea is already a reduction to MIN-ONES (over positive CNF formulae), which is basically SAT, but where you can set at most $k$ variables to true (strictly it's the optimization version where we minimize on the number of true variables).

Similarly if you head in a Parameterized Complexity direction, then you've already basically got WSAT($\Gamma_{2,1}^{+}$), where $\Gamma_{2,1}^{+}$ is the class of all positive CNF formulae (same as before, the notation might help your investigations though). In this case you'd have to start looking at what parameterization would be useful in your case.

I assume you're looking for an explicit reduction, but if not, you can always just fall back to the Cook-Levin Theorem.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.