1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Are you sure that reducing the number of clauses with fancy constructions will improve the performance of the SAT solver? Your basic $O(nm)$ encoding seems likely to interact well with the core operations of SAT solvers (unit propagation, conflict-driven clause learning). It might be worthwhile to test some sample SAT instances, where you try both the basic $O(nm)$ encoding and your fancier encodings, and see if the fancier encodings lead the SAT solver to find a solution faster. $\endgroup$
    – D.W.
    Feb 4, 2023 at 22:29
  • $\begingroup$ @D.W. Yes, the $\mathcal{O}(nm)$ encoding works fine from a SAT performance perspective. The problem is simply that I can't fit the entire clause set in RAM with the naive encoding. For my real-world use case, the two encodings I described work very well. I'm asking this question simply because I'm interested from a theoretical standpoint in whether it's possible to do better than the given encodings. $\endgroup$
    – Markus
    Feb 5, 2023 at 8:48

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.