[Solved]: Reduce the following problem to SAT

Problem Detail: 

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?

Asked By : Aden Dong

Answered By : MGwynne

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/6521