Specialized SAT solver (?)

Question

(Context)

Given two byte arrays of length 16, say $L$ and $H$, one can define a mapping $M$ from the set of all bytes to itself in the following way.

If $0 \le b \lt 256$ is a byte, let $\text{lo}(b)$ denote the lower 4 bits of $b$ and let $\text{hi}(b)$ denote the higher 4 bits of $b$.

Let $L_i$ (resp. $H_i$) denote the $i$-th byte of $L$ (resp. $H$). Also let $L_{i,j}$ (resp. $H_{i,j}$) denote the $j$-th bit of the $i$-th byte of $L$ (resp. $H$).

$$ M: \{0,\dots,255\} \to \{0,\dots,255\} \\ b \mapsto L_{\text{lo}(b)} \land H_{\text{hi}(b)} $$

Where $\land$ is bitwise logical conjunction.

If we want $M$ to satisfy $M(b_0) = m_0, \dots, M(b_p) = m_p$ for bytes $b_k$ and bytes $m_k$ with $0 \le k \lt p$. Then $L$ and $H$ have to be chosen accordingly (if possible). Note that while the $b_k$ bytes are known, the $m_k$ bytes are not. Hence why they persist as propositional variables in the following clauses.

A constraint of the form $M(b_k) = m_k$ can be translated to:

$$ L_{\text{lo}(b_k)} \land H_{\text{hi}(b_k)} = m_k $$

Or more precisely:

$$ L_{\text{lo}(b_k), j} \land H_{\text{hi}(b_k), j} = m_{k,j} $$

Where $m_{k,j}$ is the $j$-th bit of $m_k$.

In general, any equation of the form $X \land Y = Z$ where $X, Y, Z$ are bits (or booleans) is equivalent the following boolean clauses in propositional logic:

$$ \bar{X} \lor \bar{Y} \lor Z \\ X \lor \bar{Z} \\ Y \lor \bar{Z} \\ $$

Where $\bar{X}$ is the negation of $X$.

The last remaining piece of the problem is the fact that all $m_k$ bytes should be distinct. Two bits $X$ and $Y$ are non-equal iff the following clauses hold:

$$ X \lor Y \\ \bar{X} \lor \bar{Y} $$

Hence this problem can be solved using 3-SAT. I have three question with regards to this:

1. Is my problem equivalent to 3-SAT, i.e. can an arbitrary 3-SAT problem be reduced to it? Or is it further simplifiable into something less difficult?
2. If not, do you see an algorithm for solving it efficiently?
3. If yes, would a "simple" CDCL-based solver suffice? (We're dealing with around 3000 clauses and 300 variables).

I have already tried a basic backtracking solver and it failed to terminate even after multiple hours. I'm writing this after having spent multiple weeks thinking about this, and having failed to come up with a specialised algorithm. I could of course just use an off-the-shelf SAT solver but I'm interested in solving this as efficiently as possible.

Thank you in advance.

Answer 1

The best solution I know of is to use a SAT solver.

I don't know whether there is a better solution. I don't see any proof that an arbitrary 3SAT problem can be reduced to it. (OK, strictly speaking, this is impossible for the concrete problem you list with arrays of size 16, because that is a finite problem, and 3SAT involves problems of unlimited size; but we can generalize your problem to replace 16 with a parameter, and then there is no such barrier.)

I suspect the most promising approach might to represent this as a SAT instance and apply an off-the-shelf SAT solver, as SAT solvers implement many heuristics that are not likely to be part of your simple back-tracking solver.

I want to correct one detail in the post. I believe it requires a lot more than 300 variables to encode this as a SAT problem. Your post states a condition for two bits $X,Y$ to be non-equal, but you actually require that two bytes be non-equal, which is a different problem and requires many more clauses, or more variables and more clauses. So I will describe below several ways to represent "distinctness of a bunch of bytes" in SAT.

Distinctness of two bytes, with no new variables

If $x_0,\dots,x_7$ and $y_0,\dots,y_7$ are two bytes, you can represent the constraint that they are different via a conjunction of 256 clauses:

$$\bigwedge_{c_0,\dots,c_7} (x_0 \ne c_0 \lor \dots \lor x_7 \ne c_7 \lor y_0 \ne c_0 \lor \dots \lor y_7 \ne c_7),$$

where the "and" is taken over all bytes $c_0,\dots,c_7$. Notice that $x_i \ne c_i$ has either the form $x_i$ (if $c_i=0$) or $\neg x_i$ (if $c_i=1$), so each of the 256 conjuncts is itself a CNF clause.

Then, you can add constraints that $m_k,m_\ell$ are distinct for every pair of indices $k,\ell$ with $k<\ell$, representing each such constraint as above. This will add about ${p \choose 2} 256$ clauses, and no new variables.

Distinctness of two bytes, with eight new variables

If $x_0,\dots,x_7$ and $y_0,\dots,y_7$ are two bytes, you can represent the constraint that they are different via the clause $t_0 \lor \dots \lor t_7$ and the constraint $t_i \implies x_i \ne y_i$, where $t_0,\dots,t_7$ are fresh new variables (different for each pair of bytes to be compared). This can be represented with 3 clauses and 8 new variables. Doing this for all pairs of bytes requires $3 {p \choose 2}$ additional clauses and $8 {p \choose 2}$ additional variables.

Distinctness of two bytes, with three new variables

Let $u,v,w$ be three fresh new variables. Then to enforce distinctness, we enforce the constraint that $x_{4u+2v+w} \ne y_{4u+2v+w}$, or equivalently,

$$(u\ne a \lor v \ne b \lor w \ne c \lor x_{4a+2b+c} \lor y_{4a+2b+c}) \land (u\ne a \lor v \ne b \lor w \ne c \lor \neg x_{4a+2b+c} \lor \neg y_{4a+2b+c}).$$

This can be enforced with 16 clauses (two for each possible combination of $a,b,c$) and 3 new variables (for $u,v,w$). Doing this for all pairs of bytes requires $16 {p \choose 2}$ additional clauses and $3 {p \choose 2}$ additional variables.

Distinctness of $p$ bytes, with a batch sorting network

Build a bitonic sorting network that maps the bytes $0,1,\dots,255$ to 256 outputs, except you replace each byte-comparator with a unit that --- instead of sorting the two byte values -- either swaps or doesn't swap those two values, under the control of a fresh random boolean variable. Treat the first $p$ outputs from this sorting network as the values of $m_1,\dots,m_p$.

Then, use the Tseitin transform to convert this circuit to a SAT instance. If you use a bitonic sorting network, the sorting network uses about 4096 byte-comparators, and each byte-comparator requires 32 clauses and 1 additional variable. In all, this requires about 4096 additional variables and $2^{17}$ clauses. This might be a bit better when $p$ is large.

How to compare these alternatives

It's hard to know which formulation in SAT will work best with existing SAT solvers. A standard heuristic is that solutions that involve fewer variables often are easier to solve, and solutions that involve fewer clauses might be quicker to solve, but these heuristics are imperfect, and it's hard to predict which formulation might be most effective.