Split-and-list: a CNF formula is satisfiable iff its OV instance has an orthogonal pair

Statement. For every CNF formula $f$ (no hypotheses at all: no bound on clause width, number of clauses, or number of variables), $f$ is satisfiable if and only if the explicitly constructed Orthogonal Vectors instance $\mathrm{toOV}(f)$ has an orthogonal pair.

The formula $f$. $f$ consists of a number of variables $n \in \mathbb{N}$ (possibly $n = 0$) and a finite ordered list of clauses $C_0, \dots, C_{m-1}$ ($m \ge 0$; the list may be empty). Each clause is a finite list of literals (it may be empty, and may repeat literals). A literal $\ell$ is a pair consisting of a variable index $\mathrm{idx}(\ell) \in \{0, \dots, n-1\}$ and a polarity (positive or negative). Under an assignment $\sigma : \{0,\dots,n-1\} \to \{\mathrm{true}, \mathrm{false}\}$, a positive literal evaluates to $\sigma(\mathrm{idx}(\ell))$ and a negative literal to $\lnot\sigma(\mathrm{idx}(\ell))$; write $\ell(\sigma)$ for this value.

Left side of the iff ("$f$ is satisfiable").

Consequently: if $m = 0$ this holds (vacuously; when $n = 0$ the unique empty assignment witnesses it); if some clause is empty it fails.

The constructed OV instance $\mathrm{toOV}(f)$. Let

Variables with index $i < h$ are called left variables, and those with $i \ge h$ are right variables (there are $n - h = \lfloor n/2 \rfloor$ of them). The instance has $N = 2^h$ left vectors $L_0, \dots, L_{N-1}$ and $N = 2^h$ right vectors $R_0, \dots, R_{N-1}$, each a Boolean vector of dimension $m$ (one coordinate per clause, in list order). For a natural number $a$ write $\mathrm{bit}_k(a) = \lfloor a / 2^k \rfloor \bmod 2$ (least-significant bit is $k = 0$). For $a, b \in \{0,\dots,2^h-1\}$ define assignments

where $i \mathbin{\dot{-}} h$ is truncated natural subtraction ($= 0$ when $i < h$). (Formally $\alpha_a(i)$ reads bit $i$ of $a$ viewed as an $h$-bit word, returning $\mathrm{false}$ if $i \ge h$; this agrees with $\mathrm{bit}_i(a)$ since $a < 2^h$. The junk values $\alpha_a(i)$ for $i \ge h$ and $\beta_b(i) = \mathrm{bit}_0(b)$ for $i < h$ are never consulted below.) The coordinates are

That is, coordinate $j$ is $1$ exactly when no literal of $C_j$ on that side is made true by that side's half-assignment. In particular, an empty clause gives coordinate $1$ in every left and every right vector. For right variables $i \ge h$ the bit read is $i - h \le n - 1 - h$; when $n$ is even all $h$ bits of $b$ are used, and when $n$ is odd bit $h-1$ of $b$ is never read, so $R_b = R_{b'}$ whenever $b, b'$ differ only in that bit (duplicate right vectors).

Right side of the iff ("$\mathrm{toOV}(f)$ has an orthogonal pair").

Unfolded, this says: there exist $a, b < 2^h$ such that every clause $C_j$ contains either a literal with index $< h$ made true by $\alpha_a$, or a literal with index $\ge h$ made true by $\beta_b$. The pair consists of one left and one right vector (the same index $a = b$ is allowed).

Edge cases. If $n = 0$: $h = 0$, $N = 1$, there are no literals (no valid indices), so every clause is empty and every coordinate of the single left and single right vector is $1$; the right side then holds iff $m = 0$. If $m = 0$ (any $n$): the dimension is $0$ and the right side holds trivially (orthogonality over zero coordinates). If $n = 1$: $h = 1$, $N = 2$, the sole variable is a left variable, and right vectors do not depend on $b$.