Encoding "all-except" constraints in CNF

Question

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.

Answer 1

Let $[b]$ to denote $1$ if $b$ is true, $0$ if $b$ is false. We have $$ \begin{align} & \bigwedge_{b \in B \setminus B_i} b \\ \iff & \sum_{b \in B \setminus B_i} [\neg b] = 0 \\ \iff & \sum_{b \in B} [\neg b] = \sum_{b \in B_i} [\neg b] \\ \end{align} $$

Therefore, an all-except constraint can be expressed in terms of sums of values $[\neg b]$. We can make variables of form $s_{i,j} \iff \sum_{b \in B_i} [\neg b] = j$ for $j \leq |B_i|$. Furthermore, variables for the LHS $t_j \iff \sum_{b \in B} b = j$ are needed only for $j \leq 10$. Therefore, the whole condition can be expressed using $O(n + m)$ auxiliary variables and clauses.