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:
- Is my idea of solution on the right track?
- 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
