Reduce the following problem to SAT

Question

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?

Answer 1

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$:

• Translating Pseudo-Boolean Constraints into SAT - Niklas Eén and Niklas Sörensson, JSAT vol 2 (2006), pg 1-26 (a good survey).
• Efficient CNF encoding of Boolean cardinality constraints - Olivier Bailleux and Yacine Boufkhad, Proceedings of Principles and Practice of Constraint Programming 2003, LNCS vol 2833, pg 108-122 (a nice, fairly easy to implement translation).
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints - Carsten Sinz - Proceedings of Principles and Practice of Constraint Programming 2005, LNCS 3709, pg 827-831.
• Towards Robust CNF Encodings of Cardinality Constraints - Joao Marques-Silva and Inês Lynce, Proceedings of Principles and Practice of Constraint Programming 2007, LNCS 4741, pg 483-497.

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.

Answer 2

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.