Algorithmic sparsification: fast sparse $k$-SAT gives fast $k$-SAT on the word RAM

Read-back of WordRAM.Conjectures.sparsification_transfer.

The statement. Let $r$ and $k$ be natural numbers with $r \ge 2$ and $k \ge 3$. Suppose that for every natural number $d \ge 1$ (the "density") the property $\mathrm{FastSparseSAT}(k, d, r)$ holds. The theorem concludes that $\mathrm{FastSAT}(k, 2r)$ holds. The order of quantifiers in the hypothesis matters: the hypothesis is $\forall d \ge 1,\ \exists$ (algorithm, constants). So the algorithm and all of its constants may be different for each density $d$. Nothing in the hypothesis provides one algorithm that works for all densities. In the conclusion, a single algorithm with a single set of constants has to handle every formula whose clauses have width at most $k$, with no bound on the number of clauses. The integer parameter of the time bound changes from $r$ in the hypothesis to $2r$ in the conclusion. Both predicates are spelled out below.

Formulas. A SAT instance $f$ is made of:

• a number of variables $n = n(f) \in \mathbb{N}$, where $n = 0$ is allowed;
• a finite list of clauses, where each clause is a finite list of literals.

A literal is a pair (index $i \in \{0,\dots,n-1\}$, polarity $\in \{\text{true},\text{false}\}$). Under an assignment $\alpha : \{0,\dots,n-1\} \to \{\text{true},\text{false}\}$, a literal evaluates to $\alpha(i)$ when its polarity is true and to $\neg\alpha(i)$ when its polarity is false.

• $f$ is satisfiable when some $\alpha$ makes every clause in the list contain at least one literal that evaluates to true. So an empty clause makes $f$ unsatisfiable, and a formula with an empty clause list is satisfiable (for $n = 0$, by the empty assignment).
• $f$ is $k$-CNF when every clause has length (number of list entries) at most $k$. Empty clauses, repeated literals, a variable and its negation in the same clause, and repeated clauses are all allowed. The value of $k$ only caps clause length, and the hypothesis $k \ge 3$ is its only other constraint.

Encoding. The encoding $\mathrm{enc}(f)$ is the list of natural numbers

$$\mathrm{enc}(f) = [\,n,\ m\,] \;{+\!\!+}\; \big[\,\ell_1, i_{1,1}, s_{1,1}, \dots, i_{1,\ell_1}, s_{1,\ell_1}\,\big] \;{+\!\!+}\; \cdots \;{+\!\!+}\; \big[\,\ell_m, \dots\,\big].$$

Here $m$ is the number of clauses, $\ell_j$ is the length of clause $j$, $i_{j,t}$ is the variable index of its $t$-th literal, and $s_{j,t}$ is $1$ for positive polarity and $0$ for negative. Its length is $L(f) = 2 + \sum_j (1 + 2\ell_j)$.

Machine model (algorithms). An algorithm $a$ consists of:

• a fixed finite list of source instructions;
• a fixed natural number $c_a \ge 1$, the "word factor".

The source instructions are:

• copy to an address;
• a binary operation $\in \{+, -, \text{shift-left}, \text{shift-right}, \text{AND}, \text{OR}, \times\}$, stored to an address;
• bitwise NOT;
• "load word width" into an address;
• unconditional jump to a fixed program position;
• conditional branch on an unsigned comparison $=$, $<$ or $\le$ of two operands, to a fixed program position;
• halt.

An operand is either a fixed natural-number literal (an immediate) or a memory cell. A cell is named either directly, by a fixed natural number, or indirectly, through the number stored in a fixed pointer cell. For a word width $w$, the program is compiled as follows:

• immediates are reduced mod $2^w$;
• "load word width" writes the word $w \bmod 2^w$, which equals $w$;
• arithmetic is mod $2^w$, and in particular subtraction wraps around;
• shifts move by the operand's value with zero fill, so a shift by $\ge w$ gives $0$.

Memory is an infinite array of $w$-bit words indexed by $\mathbb{N}$.

Word width. On input list $x$ with "extra bits" $e$, the width is

$$w = c_a\cdot\big(e + \lfloor \log_2 (M(x)) \rfloor + 1\big), \qquad M(x) = \max\big(|x|, \max_j x_j\big) + 1.$$

Here $|x|$ is the length of the list (and $\max_j x_j$ is taken as nothing when the list is empty). For SAT the extra bits are $e = n(f)$, so the width grows linearly in the number of variables, and it is chosen per input.

Initial state. Cell $0$ holds $0$, and cell $j \ge 1$ holds $x_{j-1} \bmod 2^w$, or $0$ if $j > |x|$. Every other cell is $0$. The program counter is $0$ and the machine is not halted. Loading the input costs nothing.

One step. If the machine is halted, or the program counter is outside the program, no step is possible. In the second case the machine is stuck, which does not count as halting. Otherwise the instruction at the program counter is executed, and this costs exactly one step:

• jumps and taken branches set the program counter;
• every other instruction advances the program counter by $1$;
• the halt instruction marks the machine halted and also counts as one step.

Exact-step decision $\mathrm{Dec}(a, x, e, t, P)$. For $w$ as above, starting from the initial state, there is a sequence of exactly $t$ successful steps that reaches a state $S$ such that:

• $S$ is halted;
• cell $0$ of $S$ holds the word $0$ or the word $1$;
• cell $0$ of $S$ holds $1$ iff the proposition $P$ holds.

The initial state is not halted, and only the halt instruction sets the halted flag. So in a run that satisfies this, $t \ge 1$ and the $t$-th step is a halt instruction. The machine is deterministic, so $t$ is the unique halting time.

$\mathrm{FastSAT}(k,q)$ (the conclusion, with $q = 2r$). There exist an algorithm $a$ and natural numbers $C, p, n_0$ with $C > 0$ such that, for every $k$-CNF instance $f$ (with $n = n(f)$, $L = L(f)$), there is a $t$ with $\mathrm{Dec}(a, \mathrm{enc}(f), n, t, f \text{ satisfiable})$ and

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

Correctness and halting are therefore required for every $k$-CNF instance, while the time bound is required only when $n \ge n_0$. The constants $C, p, n_0$ are chosen after $a$ and before $f$. The exponent $p$ is unrestricted. For $q = 2r$ the bound reads $t^{2r} \le C\cdot 2^{(2r-1)n}(L+1)^p$. Since $r \ge 2$, the factor $2r-1 \ge 3$ involves no truncated subtraction.

$\mathrm{FastSparseSAT}(k,d,q)$ (the hypothesis, with $q = r$). This is word-for-word the same as $\mathrm{FastSAT}(k,q)$, with one change: the universal quantifier over $f$ is restricted to $k$-CNF instances that also have at most $d\cdot n(f)$ clauses. The required bound is $t^{r} \le C\cdot 2^{(r-1)n}(L+1)^p$. Since $r \ge 2$, $r - 1 \ge 1$ is ordinary subtraction. Edge cases:

• When $n = 0$ the clause bound forces the clause list to be empty, whatever $d$ is.
• Every $k$-CNF formula with $m$ clauses and $n \ge 1$ falls under some density, for example $d = \max(1, m)$. A formula with $n = 0$ and $m \ge 1$ clauses (each of which must be empty) falls under no density.
• The algorithm $a$, its word factor, and the constants $C, p, n_0$ all depend on $(k, d, r)$.

Not used. The imported split-and-list SAT-to-OV construction (Reduction.toOV, half, etc.) and the OV and SETH predicates are not mentioned by this statement.