Markus Asks:
Encoding "all-except" constraints in CNF
I am looking for an efficient CNF encoding of the following situation: I have sets of boolean literals $A = \{ a_1, \ldots, a_m \}$, $B = \{ b_1,\ldots, b_n \}$ and subsets $B_1, \ldots, B_m$, where for all $i$ we have $B_i \subseteq B$ and $|B_i|\le 10$. I would like to encode the constraints $$ a_i \to \bigwedge_{b \in B \setminus B_i} b\qquad (i = 1, \ldots, m) $$ into CNF. The arrow is logical implication. In other words: Each $a_i$ should imply all elements of $B$ except those which are contained in the small set $B_i$.
The naive encoding $\{(\lnot a_i \lor b)\}_{i = 1, \ldots, m,\ b \in B\setminus B_i}$ requires $\mathcal{O}(n\cdot m)$ clauses. I am looking for an encoding that only requires $\mathcal{O}(n + m)$ clauses. I'm happy to introduce helper literals like in the Tseytin transformation.
Progress
I have encodings using $\mathcal{O}(n + m\log n)$ and $\mathcal{O}(n\log n + m)$ clauses. Both constructions are inspired by tree data structures for Range-Minimum Queries.
$\mathcal{O}(n + m\log n)$
Construct a binary tree of optimal height with $n$ leaves and assign one of the $a_i$ to each leaf of the tree. Introduce a helper variable for each inner node of the tree. If $n$ is a literal assigned to an inner node of the tree and its children are assigned the literals $n'$ and $n''$, we have clauses $(\lnot n\lor n')$ and $(\lnot n\lor n'')$. Then it is easy to see that each "all-except" can be encoded using a logarithmic (in $n$) number of clauses of the form $(\lnot a_i\lor n)$, where $n$ is the literal associated with a node in the tree.
$\mathcal{O}(n \log n + m)$
This encoding is reminiscient of the sparse table data structure for RMQ.
We introduce helper literals $h_{i, j}$ for $0\le j\le \log_2 n$, $1 \le i\le n - 2^j + 1$ and have clauses $\{(\lnot h_{i, 0}\lor b_i)\}_i$,$\{(\lnot h_{i, j + 1} \lor h_{i, j})\}_{i, j}$, $\{(\lnot h_{i, j + 1}\lor h_{i + 2^j, j})\}_{i, j}$. Using this, we can encode each constraint using at most 22 clauses, since it is possible to encode a rule of the form $a_i \to b_u \wedge b_{u+1}\wedge \cdots \wedge b_{v - 1} \wedge b_v$ using only two additional clauses.
Question
Is it possible to do it with $\mathcal{O}(n + m)$ clauses? I know that there are RMQ data structures with linear precomputation and constant queries, but it's not clear to me that their ideas are useful in my setting.
SolveForum.com may not be responsible for the answers or solutions given to any question asked by the users. All Answers or responses are user generated answers and we do not have proof of its validity or correctness. Please vote for the answer that helped you in order to help others find out which is the most helpful answer. Questions labeled as solved may be solved or may not be solved depending on the type of question and the date posted for some posts may be scheduled to be deleted periodically. Do not hesitate to share your thoughts here to help others.
