Split-and-list SAT-to-OV instance and sparse $k$-SAT time bounds

Reduction.half

For a natural number $n$, $\mathrm{half}(n)$ is the natural number

$$\mathrm{half}(n) = \left\lfloor \frac{n+1}{2} \right\rfloor = \left\lceil \frac{n}{2} \right\rceil .$$

Edge values: $\mathrm{half}(0) = 0$, $\mathrm{half}(1) = 1$, $\mathrm{half}(2) = 1$, $\mathrm{half}(3) = 2$. For even $n$ it equals $n/2$; for odd $n$ it equals $(n+1)/2$, one more than $\lfloor n/2 \rfloor$.

Reduction.onLeft

For a natural number $n$ and a variable index $i \in \{0, \dots, n-1\}$, $\mathrm{onLeft}_n(i)$ is the Boolean value

$$\mathrm{onLeft}_n(i) = \mathsf{true} \iff i < \lceil n/2 \rceil .$$

So the indices $0, \dots, \lceil n/2\rceil - 1$ are "left" and the indices $\lceil n/2 \rceil, \dots, n-1$ (there are $\lfloor n/2 \rfloor$ of them) are "right". For $n = 0$ there are no indices; for $n = 1$ the single index $0$ is left and no index is right.

Reduction.fails

Here a literal over $n$ variables is a pair $\ell = (\iota(\ell), \pi(\ell))$ with variable index $\iota(\ell) \in \{0,\dots,n-1\}$ and polarity $\pi(\ell) \in \{\mathsf{true}, \mathsf{false}\}$; under an assignment $\alpha : \{0,\dots,n-1\} \to \{\mathsf{true},\mathsf{false}\}$ its value is $\alpha(\iota(\ell))$ if $\pi(\ell) = \mathsf{true}$ and $\neg\alpha(\iota(\ell))$ otherwise. A clause is a finite list of such literals (possibly empty, possibly with repeated literals). The number of variables $n$ is an implicit argument. Given a "side" predicate $\sigma : \{0,\dots,n-1\} \to \{\mathsf{true},\mathsf{false}\}$, an assignment $\alpha$, and a clause $c$, $\mathrm{fails}(\sigma, \alpha, c)$ is the Boolean

$$\mathrm{fails}(\sigma,\alpha,c) = \mathsf{true} \iff \text{there is no literal } \ell \in c \text{ with } \sigma(\iota(\ell)) = \mathsf{true} \text{ and } \ell \text{ true under } \alpha .$$

Literals whose variable is not on the side $\sigma$ are ignored entirely, regardless of $\alpha$. If $c$ is the empty clause, or if no literal of $c$ has its variable on side $\sigma$, then $\mathrm{fails}(\sigma,\alpha,c) = \mathsf{true}$ for every $\alpha$.

Reduction.leftAssignment

For $n \in \mathbb{N}$ and $a \in \{0, \dots, 2^{\lceil n/2 \rceil} - 1\}$, $\mathrm{leftAssignment}_n(a)$ is the assignment $\{0,\dots,n-1\} \to \{\mathsf{true},\mathsf{false}\}$ that sends variable $i$ to the $i$-th binary digit of $a$ (least significant digit is digit $0$), obtained by viewing $a$ as a bit string of length $\lceil n/2 \rceil$ and reading bit $i$, with the convention that a position $i \ge \lceil n/2 \rceil$ (outside that bit string) reads as $\mathsf{false}$:

$$\mathrm{leftAssignment}_n(a)(i) = \begin{cases} \text{bit}_i(a) & i < \lceil n/2\rceil,\\ \mathsf{false} & i \ge \lceil n/2 \rceil.\end{cases}$$

Since $a < 2^{\lceil n/2\rceil}$, this equals $\text{bit}_i(a)$ for every $i$. Every left variable $i < \lceil n/2 \rceil$ is driven by a distinct bit of $a$, and all $\lceil n/2 \rceil$ bits of $a$ are used, so distinct $a$ give distinct restrictions to the left variables. For $n = 0$, $a$ ranges over the single value $0$ and the assignment has empty domain.

Reduction.rightAssignment

For $n \in \mathbb{N}$ and $b \in \{0, \dots, 2^{\lceil n/2 \rceil} - 1\}$, $\mathrm{rightAssignment}_n(b)$ is the assignment $\{0,\dots,n-1\} \to \{\mathsf{true},\mathsf{false}\}$ given by

$$\mathrm{rightAssignment}_n(b)(i) = \text{bit}_{\,i \,\dot-\, \lceil n/2 \rceil}(b),$$

where $\dot-$ is truncated natural-number subtraction ($x \dot- y = \max(x-y,0)$) and $b$ is read as a bit string of length $\lceil n/2\rceil$ (positions at or beyond that length read as $\mathsf{false}$, though that never happens here, see below). Consequences of the arithmetic:

• For a left index $i < \lceil n/2 \rceil$, the subtraction truncates to $0$, so every left variable receives the same value, namely bit $0$ of $b$ (not $\mathsf{false}$).
• For a right index $i \ge \lceil n/2 \rceil$, variable $i$ receives bit $i - \lceil n/2 \rceil$ of $b$; these positions range over $0, \dots, \lfloor n/2 \rfloor - 1$, which are all inside the bit string.
• For even $n$, all $n/2$ bits of $b$ drive right variables. For odd $n$, the top bit of $b$ (position $\lceil n/2 \rceil - 1 = \lfloor n/2 \rfloor$) drives no right variable, so $b$ and $b + 2^{\lfloor n/2 \rfloor}$ (for $b < 2^{\lfloor n/2\rfloor}$) induce the same values on the right variables. For $n = 1$ there are no right variables and both $b \in \{0,1\}$ only affect variable $0$ (a left variable) through bit $0$.

Reduction.toOV

Given a SAT instance $f$, consisting of a number of variables $n$ and a list of clauses $c_0, \dots, c_{m-1}$ (each clause a finite, possibly empty, list of literals over the $n$ variables, as described for fails), $\mathrm{toOV}(f)$ is the following orthogonal-vectors instance: two lists, "left" and "right", each of exactly

$$N = 2^{\lceil n/2 \rceil}$$

Boolean vectors (indexed by $a, b \in \{0,\dots,N-1\}$), all of dimension $m$ (one coordinate per clause, in the clause order of $f$). Writing $L = \{\, i : i < \lceil n/2\rceil \,\}$ for the left variables and $R = \{\, i : \lceil n/2 \rceil \le i < n \,\}$ for the right ones, the coordinates are

$$\mathrm{left}_a[j] = \mathsf{true} \iff \text{no literal } \ell \in c_j \text{ has } \iota(\ell) \in L \text{ and is true under } \mathrm{leftAssignment}_n(a),$$ $$\mathrm{right}_b[j] = \mathsf{true} \iff \text{no literal } \ell \in c_j \text{ has } \iota(\ell) \in R \text{ and is true under } \mathrm{rightAssignment}_n(b),$$

where $\mathrm{leftAssignment}_n(a)$ sets variable $i$ to bit $i$ of $a$, and $\mathrm{rightAssignment}_n(b)$ sets variable $i \in R$ to bit $i - \lceil n/2\rceil$ of $b$ (its values on $L$, which equal bit $0$ of $b$, are never consulted here because left-side literals are filtered out of the right vectors). Clause indexing is always in range. Edge cases: both lists have the same length $2^{\lceil n/2 \rceil}$ even though there are only $\lfloor n/2 \rfloor$ right variables, so for odd $n$ each right vector appears (at least) twice; for $n = 1$ every right vector is the all-$\mathsf{true}$ vector. For $n = 0$, $N = 1$ and every clause is necessarily empty, so the single left and single right vector are both all-$\mathsf{true}$ of dimension $m$. An empty clause $c_j$ gives coordinate $j$ equal to $\mathsf{true}$ in every left and every right vector. A clause containing only left variables gives coordinate $j$ equal to $\mathsf{true}$ in every right vector (and symmetrically). If $m = 0$ the vectors are all the empty vector. The construction is a direct function of $f$; nothing in it refers to satisfiability. (An OV instance in the dependencies also has a notion "there exist $a, b$ with no coordinate $j$ where both $\mathrm{left}_a[j]$ and $\mathrm{right}_b[j]$ are $\mathsf{true}$"; toOV itself does not state any relation between that notion and satisfiability of $f$.)

HasFastSparseSAT

For natural numbers $k$, $d$ ("density") and $q$, $\mathrm{HasFastSparseSAT}(k, d, q)$ is the proposition:

There exist an algorithm $A$ and natural numbers $C, p, n_0$ with $C > 0$ such that for every SAT instance $f$ with $n$ variables and clause list $c_0,\dots,c_{m-1}$ satisfying

1. every clause has at most $k$ literals ($|c_j| \le k$ for all $j$), and
2. $m \le d \cdot n$,

there exists $t \in \mathbb{N}$ such that $A$ decides the satisfiability of $f$ in exactly $t$ steps on input $\mathrm{enc}(f)$ with extra-bits parameter $n$ (defined below), and if $n \ge n_0$ then

$$t^{q} \le C \cdot 2^{(q \,\dot-\, 1)\, n} \cdot \bigl(|\mathrm{enc}(f)| + 1\bigr)^{p}.$$

The quantifier order is: $A, C, p, n_0$ are chosen once (depending only on $k, d, q$), then $f$ is arbitrary, then $t$ may depend on $f$. The decision requirement holds for all admissible $f$, including $n < n_0$; only the time inequality is restricted to $n \ge n_0$.

Instances, satisfiability, encoding. A literal is a variable index in $\{0,\dots,n-1\}$ with a polarity; clauses may be empty or contain repeated literals. $f$ is satisfiable iff there is an assignment $\alpha : \{0,\dots,n-1\} \to \{\mathsf{true},\mathsf{false}\}$ such that every clause contains at least one literal true under $\alpha$; so an empty clause makes $f$ unsatisfiable and an empty clause list makes $f$ satisfiable (also when $n = 0$). The encoding $\mathrm{enc}(f)$ is the list of natural numbers $[n, m]$ followed, for each clause in order, by its length $|c_j|$ and then, for each literal in order, the pair (variable index, $1$ if positive else $0$). Hence $|\mathrm{enc}(f)| = 2 + \sum_j (1 + 2|c_j|)$.

Algorithms and the machine. An algorithm $A$ consists of a finite list of source instructions and a positive natural number $\phi$ ("word factor"). Given an input list $x$ of naturals and an extra-bits parameter $e$, the word width is

$$w = \phi \cdot \bigl(e + \lfloor \log_2 M(x) \rfloor + 1\bigr), \qquad M(x) = \max\bigl(|x|, \max_i x_i\bigr) + 1,$$

(with $\lfloor\log_2\rfloor$ the floor binary logarithm); here $x = \mathrm{enc}(f)$ and $e = n$. The source code is compiled to a word RAM program over $w$-bit words (values in $\{0,\dots,2^w-1\}$) in the "multiplication" model: instructions are copy, binary operation (addition, subtraction, multiplication all mod $2^w$; left/right shift by the unsigned value of the second operand with zero fill; bitwise AND, OR), bitwise NOT, "store the word width" (writes $w \bmod 2^w$ into a cell; this is the only native constant), unconditional jump to a fixed instruction index, conditional branch on an unsigned comparison ($=$, $<$, $\le$) to a fixed index, and halt. Operands are immediates (fixed natural-number literals reduced mod $2^w$) or memory reads; destination and source addresses are direct (a fixed cell number) or indirect (the unsigned value stored in a fixed cell). Each executed instruction advances the program counter by one (unless it jumps/branches), and halt sets a halted flag. A step is defined only when the machine is not halted and the program counter indexes an existing instruction; otherwise no step exists (in particular, falling off the end of the program is a stuck state, not a halt).

Deciding in exactly $t$ steps. "$A$ decides $P$ in $t$ steps on input $x$ with extra bits $e$" means: with $w$ as above, starting from the initial state in which cell $0$ holds $0$, cell $a \ge 1$ holds $x_{a-1} \bmod 2^w$ for $a \le |x|$ and $0$ for $a > |x|$, program counter $0$, not halted, there is a sequence of exactly $t$ successive successful steps ending in a state $s$ with

• $s$ halted,
• the word in cell $0$ of $s$ equal to $0$ or to $1$, and
• (cell $0$ of $s$ equals $1$) $\iff P$, here $P$ = "$f$ is satisfiable".

Because the initial state is not halted and only the halt instruction sets the flag, $t \ge 1$ and $t$ counts every executed instruction including the final halt. Since each step is a function of the state, at most one such $t$ exists for given $A$ and $f$. Input loading costs nothing.

Edge cases of the parameters.

• $q = 0$: $q \dot- 1 = 0$ and $t^0 = 1$, so the time inequality reads $1 \le C\,(|\mathrm{enc}(f)|+1)^p$, which holds automatically since $C \ge 1$; only correctness/halting remains.
• $q = 1$: the inequality is $t \le C\,(|\mathrm{enc}(f)|+1)^p$ (no exponential factor).
• $q \ge 2$: $t \le \bigl(C\, 2^{(q-1)n} (|\mathrm{enc}(f)|+1)^p\bigr)^{1/q}$.
• $d = 0$, or $n = 0$: only instances with no clauses at all are quantified over.
• $k = 0$: only instances whose clauses are all empty are quantified over.
• The polynomial exponent $p$ is unrestricted, and $C$, $p$, $n_0$ may not depend on $f$.