Fast Orthogonal Vectors gives fast sparse $k$-SAT on the word RAM

Statement. For all natural numbers $q, k, \delta$ (the code calls $\delta$ density) with

$$q \ge 2, \qquad k \ge 3, \qquad \delta \ge 1,$$

if $\mathrm{FastOV}(2\delta,\, q)$ holds, then $\mathrm{FastSparseSAT}(k,\, \delta,\, 4q)$ holds. Neither $k$ nor anything else about SAT appears in the hypothesis: the same OV hypothesis (with dimension factor $2\delta$ and improvement parameter $q$) is assumed for every $k \ge 3$. The theorem is a pure implication between these two existence statements. It says nothing if no algorithm satisfies $\mathrm{FastOV}(2\delta, q)$. Nothing in the statement links the SAT algorithm it concludes exists to the OV algorithm it assumes. The imported file also defines a split-and-list SAT-to-OV construction (half, toOV, and related functions), but the statement does not refer to any of it.

---

The machine (multiplication word RAM). A word width $w$ is a positive integer, and a word is a $w$-bit vector, i.e. an integer in $\{0,\dots,2^w-1\}$. Memory is an infinite array $\mathrm{mem}:\mathbb{N}\to\{0,\dots,2^w-1\}$. A machine state consists of the memory, a program counter $\mathrm{pc}\in\mathbb{N}$, a flag $\mathrm{halted}$ and a tick counter (the tick counter plays no role here).

An algorithm $a$ consists of two parts:

• a finite list of source instructions, the same list for every input and every width;
• a constant $\mathrm{wordFactor}_a \ge 1$.

At width $w$, each source instruction compiles to one machine instruction. Immediate literals $n\in\mathbb{N}$ become $n \bmod 2^w$. Addresses are either direct (cell $c$) or indirect (the cell whose index is the numeric value stored in cell $c$). The instructions are:

• copy a source operand into a destination cell;
• binary operations, all taken mod $2^w$: $x+y$, $x-y$ (wrapping), $x\cdot y$, left shift $x\cdot 2^{y}$, right shift $\lfloor x/2^{y}\rfloor$ (zero fill), bitwise AND and bitwise OR;
• bitwise NOT;
• load word width, which writes the word $w \bmod 2^w$ (which equals $w$) into a cell. This is the only "native constant".
• unconditional jump to an absolute instruction index;
• conditional branch on unsigned $=$, $<$ or $\le$ between two operands; it goes to the target if the test holds and to $\mathrm{pc}+1$ otherwise;
• halt.

Every executed instruction other than a jump or a taken branch increments $\mathrm{pc}$. Halt sets $\mathrm{halted}$ to true. A single step behaves as follows:

• It is undefined if the state is already halted.
• It is undefined if $\mathrm{pc}$ is not a valid index into the program; this is a stuck state, not a halt.
• Otherwise it executes the instruction at index $\mathrm{pc}$.

$\mathrm{Runs}(t, s, u)$ means that exactly $t$ consecutive defined steps lead from $s$ to $u$.

Word width used. For an input list $x$ of naturals and a parameter $e$ ("extra bits"), let

$$M(x) = \max\bigl(|x|,\ \max_i x_i\bigr) + 1,$$

where $|x|$ is the length of the list. The width is

$$w_a(x,e) = \mathrm{wordFactor}_a\cdot\bigl(e + \lfloor \log_2 M(x)\rfloor + 1\bigr).$$

Initial state. Cell $0$ holds $0$. For $1\le i\le |x|$, cell $i$ holds $x_{i-1} \bmod 2^w$ (every entry is $< M(x)$, so it fits without truncation). All other cells hold $0$. Also $\mathrm{pc}=0$ and the machine is not halted. Loading the input is free; only executed instructions are counted.

$\mathrm{DecidesIn}(a, x, e, t, P)$. Let $w = w_a(x,e)$. There must be a state $u$ such that all of the following hold:

• the program of $a$ compiled at width $w$ performs exactly $t$ defined steps from the initial state on $x$ and ends in $u$;
• $u$ is halted;
• cell $0$ of $u$ holds $0$ or $1$;
• cell $0$ of $u$ holds $1$ if and only if the proposition $P$ is true.

A step from a halted state is undefined, so in such a run the $t$-th step is the halt instruction itself and no earlier step halts. Hence $t\ge 1$, and $t$ is exactly the number of instructions executed, counting the final halt. The run is deterministic, so $t$ is determined by $a$ and $x$.

---

OV instances and the hypothesis $\mathrm{FastOV}(c, q)$, with $c = 2\delta$. An OV instance consists of a count $N$, a dimension $d$, and two families $L_0,\dots,L_{N-1}$ and $R_0,\dots,R_{N-1}$ of vectors in $\{0,1\}^d$. Duplicates are allowed. Two vectors are orthogonal if no coordinate is $1$ in both. The instance "has an orthogonal pair" if some $L_i$ is orthogonal to some $R_j$ with $i, j < N$.

Its encoding is the list

$$[N, d] \;\text{++}\; (\text{all bits of } L_0,\dots,L_{N-1} \text{ in row order}) \;\text{++}\; (\text{all bits of } R_0,\dots,R_{N-1}).$$

Each bit is one entry, $0$ or $1$, so the list has length $2+2Nd$.

Let $\lceil\log_2\rceil^*(N) := \lfloor\log_2(N-1)\rfloor+1$, which equals $\lceil\log_2 N\rceil$ for $N\ge 2$. $\mathrm{FastOV}(c,q)$ states the following. There exist an algorithm $a$ and naturals $C\ge 1$ and $n_0$ such that, for every OV instance $v$ with

$$N \ge 2 \quad\text{and}\quad d \le c\cdot\lceil\log_2\rceil^*(N),$$

there is a $t$ with both of the following:

• \mathrm{DecidesIn}(a, \mathrm{enc}(v), 0, t, \text{"v has an orthogonal pair"}), so the extra bits are $0$ and $w = \mathrm{wordFactor}_a(\lfloor\log_2 M\rfloor+1)$;
• if $N \ge n_0$ then

$$t^{q} \le C\cdot N^{2q-1}.$$

There is no truncated subtraction here because $q\ge2$; over the reals the bound is equivalent to $t\le C^{1/q}N^{2-1/q}$. The bound is required for every valid instance with $N\ge n_0$. Correct halting is required for every valid instance, including those with $N < n_0$. Dimension $d=0$ is allowed. Instances with $N<2$, or with dimension above the bound, are not constrained. In the theorem, $c = 2\delta$.

---

SAT instances and the conclusion $\mathrm{FastSparseSAT}(k, \delta, Q)$, with $Q = 4q$. A SAT instance consists of a number of variables $n$ and a list of clauses. Each clause is a list of literals, and a literal is a pair (index $i\in\{0,\dots,n-1\}$, polarity). Under an assignment $\alpha:\{0,\dots,n-1\}\to\{\text{true},\text{false}\}$, a positive literal evaluates to $\alpha(i)$ and a negative one to $\neg\alpha(i)$.

• Satisfiable means that some $\alpha$ makes every clause in the list contain a literal that evaluates to true. An empty clause makes the instance unsatisfiable. An empty clause list is satisfiable, even when $n=0$.
• $k$-CNF means that every clause has at most $k$ literals. Empty clauses, repeated literals, repeated clauses, and complementary literals within a clause are all allowed.
• Sparsity: the number of clauses $m$ (the length of the list, repetitions counted) satisfies $m \le \delta\cdot n$. When $n=0$ this forces $m=0$.

The encoding is

$$[n, m] \;\text{++}\; \bigl[\ell_1, i_{1,1}, \sigma_{1,1}, \dots\bigr] \;\text{++} \cdots$$

For each clause in order, the list contains its length $\ell_j$ followed by the pair (variable index, polarity bit) for each of its literals, with polarity $1$ for positive and $0$ for negative. The encoded length is $L = 2 + m + 2\sum_j \ell_j$.

$\mathrm{FastSparseSAT}(k,\delta,Q)$ states the following. There exist an algorithm $a$ and naturals $C\ge1$, $p$ and $n_0$ (chosen after $k,\delta,Q$ and before the instance) such that, for every SAT instance $f$ that is $k$-CNF and has $m\le\delta n$, there is a $t$ with both of the following:

• \mathrm{DecidesIn}(a, \mathrm{enc}(f), n, t, \text{"f is satisfiable"}). The extra bits equal the number of variables, so the word width is

$$w = \mathrm{wordFactor}_a\bigl(n + \lfloor\log_2 M(\mathrm{enc}(f))\rfloor + 1\bigr) \ \ge\ n+1.$$

• if $n\ge n_0$ then

$$t^{Q} \le C\cdot 2^{(Q-1)\,n}\cdot (L+1)^{p}.$$

The exponent $p$ is unrestricted. Correct halting is required for all such $f$, including those with $n<n_0$.

With $Q=4q\ge 8$, the subtraction $Q-1=4q-1$ is not truncated. The concluded bound reads

$$t^{4q} \le C\cdot 2^{(4q-1)n}\cdot(L+1)^p,$$

which over the reals is equivalent to $t\le C^{1/(4q)}\,2^{(1-\frac{1}{4q})n}\,(L+1)^{p/(4q)}$.