ETH Hardness of Partial-Function MCSP (PartialMCSP)

This module formalizes Rahul Ilango's ETH lower bound for partial-function Minimum Circuit Size Problem (MCSP* / PartialMCSP) [Ilango2020FOCS, Theorem I.3, pp. 424, 427–428; ECCC TR20-183, Section 1.2.2, Theorem 3, p. 6, and Section 3, Theorem 11 (p. 20) & Lemma 12 (p. 22), construction and proof pp. 21–26]: under the Exponential Time Hypothesis (ETH), PartialMCSP on partial Boolean functions of arity $m$ (truth-table size $N = 2^m$) is not decidable in subexponential time $2^{o(m \log m)} = N^{o(\log \log N)}$ (¬DecidableInSubexpTime).

Overview of the reduction and faithfulness

1. Source problem (BipartitePermutationIndependentSet): Given an instance $G = (n, E)$ of $2n \times 2n$ Bipartite Permutation Independent Set with parameter $n$ and directed pair-edges $E \subseteq ([n] \times [n])^2$, decide whether there exist permutations $\sigma_1, \sigma_2 \in S_n$ (equivalently, a block-preserving permutation $\pi \in S_{2n}$ on $[0, n) \cup [n, 2n)$) avoiding all conflict edges in $E$. By the Lokshtanov–Marx–Saurabh theorem (ETH.not_decidableInSubexpTime_BipartitePermutationIndependentSet, [LokshtanovMarxSaurabh2018, Theorem 2.11]; [Ilango2020FOCS, Section III.B, p. 427; ECCC TR20-183, Section 3, Theorem 10, p. 20]), this problem cannot be decided in time $2^{o(n \log n)}$ under ETH.

2. Ilango's partial Boolean function $\gamma_G$ (PartialMCSP.ilangoGamma, [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, p. 21]): For $n = G.1$, $\gamma_G : \{0, 1\}^{6n} \to \mathrm{Option\ Bool}$ views a $6n$-bit input as a triple $(x, y, z) \in \{0, 1\}^{2n} \times \{0, 1\}^{2n} \times \{0, 1\}^{2n}$ and is defined by seven clauses:

   • (1) If $x = 0^{2n}$: $\bigvee_{i \in [2n]} (y_i \wedge z_i)$.
   • (2) If $x = 1^{2n}$: $\bigvee_{i \in [2n]} z_i$.
   • (3) If $z = 1^{2n}$: $\bigvee_{i \in [2n]} (x_i \vee y_i)$.
   • (4) If $z = 0^{2n}$: $0$ (false).
   • (5) If $z = 1^n 0^n$ and $y = 0^{2n}$: $\bigvee_{i < n} x_i$.
   • (6) If $z = 0^n 1^n$ and $y = 0^{2n}$: $\bigvee_{n \le i < 2n} x_i$.
   • (7) If $\exists ((j, k), (j', k')) \in E$ with $(x, y, z) = (\overline{e_k}\,\overline{e_{k'}}, 0^{2n}, e_j\,e_{j'})$: $1$ (true).
   • Otherwise: $?$ (none).

3. Rigidity of read-once formulas for Clauses 1–4 (PosFormula.exists_perm_of_agreesWith_ilango, [ECCC TR20-183, Section 3, Lemma 12, pp. 22, 24–26]): Any read-once positive formula $F$ on $6n$ variables ($n \ge 1$) of leaf size $6n$ (i.e., binary gate size $6n - 1$) that agrees with Clauses (1)–(4) computes $(x, y, z) \mapsto \bigvee_{i \in [2n]} ((x_{\pi(i)} \vee y_i) \wedge z_i)$ for some permutation $\pi \in S_{2n}$.

4. Equivalence across circuit and formula models ([ECCC TR20-183, Section 3, Theorem 11, p. 20, construction and proof pp. 21–24]): For $n \ge 2$, the instance ilangoInstance G of arity $6n$ and threshold $s = 6n - 1$ has all $6n$ variables positively essential (ilangoInstance_posEssential). By Circuit.exists_posFormula_of_cost_binaryCost_le, any circuit $c$ with at most $6n - 1$ binary (AND/OR) gates agreeing with $\gamma_G$ unfolds into a read-once positive formula of size $6n - 1$. Conversely, any satisfying permutation $\pi \in S_{2n}$ yields an explicit read-once positive formula $\bigvee_{i \in [2n]} ((x_{\pi(i)} \vee y_i) \wedge z_i)$ of gate size $6n - 1$ whose compiled circuit has all-gates size $6n - 1$. Thus for $n \ge 2$: $$G \in \mathrm{BipartitePermutationIndependentSet} \iff \mathrm{ilangoInstance}\, G \in \mathrm{PartialMCSP} \iff \mathrm{ilangoInstance}\, G \in \mathrm{PartialMCSP.BinaryGate} \iff \mathrm{ilangoInstance}\, G \in \mathrm{PartialMCSP.MonotoneReadOnce}.$$

Main definitions

• Cslib.PartialMCSP.MonotoneReadOnce: partial-function MCSP restricted to read-once positive formulas.
• Cslib.PartialMCSP.ilangoGamma, Cslib.PartialMCSP.ilangoInstance: Ilango's partial Boolean function $\gamma_G$ on $6n$ bits and the PartialMCSP instance $(\gamma_G, 6n - 1)$.
• Cslib.PartialMCSP.ilangoReduction: total reduction from BipartitePermutationGraph to PartialMCSP running in time $2^{O(n)} \cdot \mathrm{poly}(|G|)$.

Main results

• Cslib.Circuits.Boolean.PosFormula.exists_perm_of_agreesWith_ilango: Ilango's Lemma 12 [ECCC TR20-183, Section 3, Lemma 12, pp. 22, 24–26].
• Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoInstance_mem: correctness of ilangoInstance for $2 \le G.1$ across PartialMCSP, PartialMCSP.BinaryGate, and PartialMCSP.MonotoneReadOnce [ECCC TR20-183, Section 3, Theorem 11, p. 20, proof pp. 21–24].
• Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_encBinary, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_binaryGate, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_binaryGate_encBinary, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_monotoneReadOnce, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_monotoneReadOnce_encBinary, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_tableSize, Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_tableSize_encBinary: Ilango's FOCS 2020 Theorem I.3 / ECCC TR20-183 Section 1.2.2 Theorem 3 (under ETH, PartialMCSP and its binary-gate and monotone-read-once variants reject the subexponential decider family DecidableInSubexpTime at $m \log_2 m = \log_2 N \cdot \log_2 \log_2 N$, i.e., are not decidable in time $2^{o(m \log m)} = N^{o(\log \log N)}$).

References

• R. Ilango, Constant Depth Formula and Partial Function Versions of MCSP are Hard
• D. Lokshtanov, D. Marx, S. Saurabh, Slightly Superexponential Parameterized Problems

Read-once monotone formula variant of PartialMCSP

def Cslib.PartialMCSP.MonotoneReadOnce : Set Instance

Read-once positive formula variant of PartialMCSP [Ilango2020FOCS, Section III.B; ECCC TR20-183, Section 3, Theorem 11, p. 20]: instances x : PartialMCSP.Instance that agree with some read-once positive Boolean formula F : PosFormula x.arity with at most x.threshold binary gates.

theorem Cslib.PartialMCSP.mem_monotoneReadOnce_iff {x : Instance} : x ∈ MonotoneReadOnce ↔ ∃ (F : Circuits.Boolean.PosFormula x.arity), F.IsReadOnce ∧ F.size ≤ x.threshold ∧ x.AgreesWith F.eval

theorem Cslib.PartialMCSP.mem_of_mem_monotoneReadOnce {x : Instance} (h : x ∈ MonotoneReadOnce) : x ∈ PartialMCSP

Every yes-instance of PartialMCSP.MonotoneReadOnce is a yes-instance of all-gates PartialMCSP, since F.toCircuit has F.toCircuit.size = F.size.

theorem Cslib.PartialMCSP.monotoneReadOnce_subset : MonotoneReadOnce ⊆ PartialMCSP

theorem Cslib.PartialMCSP.monotoneReadOnce_subset_binaryGate : MonotoneReadOnce ⊆ BinaryGate

Block-of-three-$2n$ coordinates (x, y, z) on Fin (6 * n)

def Cslib.PartialMCSP.xVar {n : ℕ} (i : Fin (2 * n)) : Fin (6 * n)

Coordinate i : Fin (2 * n) of the first block x in Fin (6 * n).

def Cslib.PartialMCSP.yVar {n : ℕ} (i : Fin (2 * n)) : Fin (6 * n)

Coordinate i : Fin (2 * n) of the second block y in Fin (6 * n).

def Cslib.PartialMCSP.zVar {n : ℕ} (i : Fin (2 * n)) : Fin (6 * n)

Coordinate i : Fin (2 * n) of the third block z in Fin (6 * n).

def Cslib.PartialMCSP.unpackX {n : ℕ} (w : BitString (6 * n)) : BitString (2 * n)

Extract the x-block of a $6n$-bit string.

def Cslib.PartialMCSP.unpackY {n : ℕ} (w : BitString (6 * n)) : BitString (2 * n)

Extract the y-block of a $6n$-bit string.

def Cslib.PartialMCSP.unpackZ {n : ℕ} (w : BitString (6 * n)) : BitString (2 * n)

Extract the z-block of a $6n$-bit string.

def Cslib.PartialMCSP.packXYZ {n : ℕ} (x y z : BitString (2 * n)) (v : Fin (6 * n)) : Bool

Pack three $2n$-bit strings (x, y, z) into a single $6n$-bit string.

Special $2n$-bit vectors and Ilango's partial function $\gamma_G$

def Cslib.PartialMCSP.zeros2n {n : ℕ} : BitString (2 * n)

All-zeros vector $0^{2n}$.

def Cslib.PartialMCSP.ones2n {n : ℕ} : BitString (2 * n)

All-ones vector $1^{2n}$.

def Cslib.PartialMCSP.leftHalfOnes {n : ℕ} : BitString (2 * n)

Left-half indicator $1^n 0^n$.

def Cslib.PartialMCSP.rightHalfOnes {n : ℕ} : BitString (2 * n)

Right-half indicator $0^n 1^n$.

def Cslib.PartialMCSP.unitPair {n : ℕ} (j j' : Fin n) : BitString (2 * n)

Pair-of-units vector $e_j e_{j'} \in \{0, 1\}^{2n}$ with ones at $j$ and $n + j'$.

def Cslib.PartialMCSP.antiUnitPair {n : ℕ} (k k' : Fin n) : BitString (2 * n)

Complemented pair-of-units vector $\overline{e_k}\,\overline{e_{k'}} \in \{0, 1\}^{2n}$ with zeros at $k$ and $n + k'$ and ones elsewhere.

def Cslib.PartialMCSP.ilangoGamma (G : Complexity.BipartitePermutationGraph) (w : BitString (6 * G.1)) : Option Bool

Ilango's partial Boolean function $\gamma_G$ [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, p. 21] on $6n$ variables for a BipartitePermutationGraph $G = (n, E)$.

def Cslib.PartialMCSP.ilangoInstance (G : Complexity.BipartitePermutationGraph) : Instance

Ilango's PartialMCSP instance [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21]: partial truth table $\gamma_G$ on $6n$ variables with size threshold $s = 6n - 1$.

@[simp]

theorem Cslib.PartialMCSP.ilangoInstance_arity (G : Complexity.BipartitePermutationGraph) : (ilangoInstance G).arity = 6 * G.1

@[simp]

theorem Cslib.PartialMCSP.ilangoInstance_threshold (G : Complexity.BipartitePermutationGraph) : (ilangoInstance G).threshold = 6 * G.1 - 1

@[simp]

theorem Cslib.PartialMCSP.ilangoInstance_partialFunction (G : Complexity.BipartitePermutationGraph) : (ilangoInstance G).partialFunction = ilangoGamma G

Evaluation of ilangoGamma on each of the seven clauses

Positive essentiality of all $6n$ variables (Claim 13)

Ilango's Lemma 12: Structural characterization of read-once formulas for Clauses 1–4

theorem Cslib.Circuits.Boolean.PosFormula.exists_perm_of_agreesWith_ilango {n : ℕ} {F : PosFormula (6 * n)} (hro : F.IsReadOnce) (hleaf : F.leafSize = 6 * n) (hC1 : ∀ (y z : BitString (2 * n)), F.eval (PartialMCSP.packXYZ PartialMCSP.zeros2n y z) = decide (∃ (i : Fin (2 * n)), y i = true ∧ z i = true)) (hC2 : ∀ (y z : BitString (2 * n)), F.eval (PartialMCSP.packXYZ PartialMCSP.ones2n y z) = decide (∃ (i : Fin (2 * n)), z i = true)) (hC3 : ∀ (x y : BitString (2 * n)), F.eval (PartialMCSP.packXYZ x y PartialMCSP.ones2n) = decide (∃ (i : Fin (2 * n)), x i = true ∨ y i = true)) (hC4 : ∀ (x y : BitString (2 * n)), F.eval (PartialMCSP.packXYZ x y PartialMCSP.zeros2n) = false) : ∃ (π : Equiv.Perm (Fin (2 * n))), ∀ (x y z : BitString (2 * n)), F.eval (PartialMCSP.packXYZ x y z) = decide (∃ (i : Fin (2 * n)), ((x (π i) || y i) && z i) = true)

Ilango's Lemma 12 [ECCC TR20-183, Section 3, Lemma 12, pp. 22, 24–26]: if F : PosFormula (6 * n) is a read-once positive formula of leaf size $6n$ that agrees with Clauses (1)–(4) of $\gamma_G$, then there exists a permutation $\pi \in S_{2n}$ such that for all $x, y, z \in \{0, 1\}^{2n}$, $$F.\mathrm{eval}(\mathrm{packXYZ}\, x\, y\, z) = \mathrm{decide}(\exists i \in \mathrm{Fin}\,(2n),\; (x(\pi(i)) \vee y(i)) \wedge z(i)).$$

Section 5: Ilango's Theorem 11 (Exact Equivalence for $n \ge 2$)

def Cslib.PartialMCSP.ilangoPosFormula {n : ℕ} (hn : 0 < n) (π : Equiv.Perm (Fin (2 * n))) : Circuits.Boolean.PosFormula (6 * n)

The read-once positive formula $\bigvee_{i=1}^{2n} ((x_{\pi(i)} \vee y_i) \wedge z_i)$ of gate size $6n - 1$ corresponding to a permutation $\pi \in S_{2n}$ [ECCC TR20-183, Section 3, p. 22].

theorem Cslib.PartialMCSP.agreesWith_ilangoPosFormula_of_satisfiesUndirected {G : Complexity.BipartitePermutationGraph} (hn : 0 < G.1) {π : Equiv.Perm (Fin (2 * G.1))} (hπ : G.SatisfiesUndirected π) : (ilangoInstance G).AgreesWith (ilangoPosFormula hn π).eval

If $\pi \in S_{2n}$ satisfies G.SatisfiesUndirected π, then the read-once positive formula ilangoPosFormula hn π agrees with ilangoInstance G on every defined entry [ECCC TR20-183, Section 3, Theorem 11 (easy direction), pp. 23–24].

theorem Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoInstance_mem_monotoneReadOnce {G : Complexity.BipartitePermutationGraph} (hG : 2 ≤ G.1) : G ∈ Complexity.BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ MonotoneReadOnce

Ilango's Theorem 11 (monotone read-once equivalence for $n \ge 2$) [ECCC TR20-183, Section 3, Theorem 11, p. 20, proof pp. 21–24]: for $2 \le G.1$, G ∈ BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ PartialMCSP.MonotoneReadOnce.

theorem Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoInstance_mem_binaryGate {G : Complexity.BipartitePermutationGraph} (hG : 2 ≤ G.1) : G ∈ Complexity.BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ BinaryGate

Ilango's Theorem 11 (binary-gate equivalence for $n \ge 2$) [ECCC TR20-183, Section 3, Theorem 11, p. 20, proof pp. 21–24]: for $2 \le G.1$, G ∈ BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ PartialMCSP.BinaryGate.

theorem Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoInstance_mem {G : Complexity.BipartitePermutationGraph} (hG : 2 ≤ G.1) : G ∈ Complexity.BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ PartialMCSP

Ilango's Theorem 11 (all-gates equivalence for $n \ge 2$) [ECCC TR20-183, Section 3, Theorem 11, p. 20, proof pp. 21–24]: for $2 \le G.1$, G ∈ BipartitePermutationIndependentSet ↔ ilangoInstance G ∈ PartialMCSP.

Section 6: Total Reduction ilangoReduction and $2^{O(n)}$-Time Computability

def Cslib.PartialMCSP.ilangoReduction (G : Complexity.BipartitePermutationGraph) : Instance

Total reduction from BipartitePermutationIndependentSet to PartialMCSP [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21]: maps $G$ to ilangoInstance G when $2 \le G.1$, and to trivialYesInstance / trivialNoInstance when $G.1 < 2$.

theorem Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoReduction_mem_monotoneReadOnce (G : Complexity.BipartitePermutationGraph) : G ∈ Complexity.BipartitePermutationIndependentSet ↔ ilangoReduction G ∈ MonotoneReadOnce

theorem Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoReduction_mem_binaryGate (G : Complexity.BipartitePermutationGraph) : G ∈ Complexity.BipartitePermutationIndependentSet ↔ ilangoReduction G ∈ BinaryGate

theorem Cslib.PartialMCSP.mem_BipartitePermutationIndependentSet_iff_ilangoReduction_mem (G : Complexity.BipartitePermutationGraph) : G ∈ Complexity.BipartitePermutationIndependentSet ↔ ilangoReduction G ∈ PartialMCSP

Bitwise list evaluator and $2^{O(n)}$-time computability of ilangoReduction

theorem Cslib.PartialMCSP.exists_computableInO_ilangoReduction : ∃ (C : ℕ) (D : ℕ), Turing.MultiTapeTM.ComputableInO ilangoReduction Complexity.encBipartitePermutationGraph enc (fun (G : Complexity.BipartitePermutationGraph) => 2 ^ (C * G.1) * ((Complexity.encBipartitePermutationGraph G).length + 1) ^ D) fun (G : Complexity.BipartitePermutationGraph) => 2 ^ (C * G.1) * ((Complexity.encBipartitePermutationGraph G).length + 1) ^ D

Plain $2^{O(n)}$-time computability of Ilango's reduction under unary threshold encoding (PartialMCSP.enc) [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21].

Section 7: Subexponential-Time Transfer and Ilango's ETH Lower Bounds

def Cslib.PartialMCSP.Instance.tableSize (x : Instance) : ℕ

The truth-table size $N = 2^m$ of a PartialMCSP.Instance of arity $m$ [Ilango2020FOCS, Theorem I.3, p. 424; ECCC TR20-183, Section 1.2.2, Theorem 3, p. 6].

@[simp]

theorem Cslib.PartialMCSP.Instance.log_tableSize (x : Instance) : Nat.log 2 x.tableSize = x.arity

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP (h : ETH) : ¬DecidableInSubexpTime PartialMCSP PartialMCSP.enc fun (I : PartialMCSP.Instance) => I.arity * Nat.log 2 I.arity

Ilango's ETH Lower Bound for PartialMCSP (unary threshold encoding) [Ilango2020FOCS, Theorem I.3, pp. 424, 427–428; ECCC TR20-183, Section 1.2.2, Theorem 3, p. 6, and Section 3, Theorem 11, pp. 20–21]: under ETH, PartialMCSP on $m$-variable partial Boolean functions cannot be decided in time $2^{o(m \log m)} = N^{o(\log \log N)}$ (where $N = 2^m$ is the truth-table size).

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_encBinary (h : ETH) : ¬DecidableInSubexpTime PartialMCSP PartialMCSP.encBinary fun (I : PartialMCSP.Instance) => I.arity * Nat.log 2 I.arity

Ilango's ETH Lower Bound for PartialMCSP (binary threshold encoding) [Ilango2020FOCS, Theorem I.3, pp. 424, 427–428; ECCC TR20-183, Section 1.2.2, Theorem 3, p. 6, and Section 3, Theorem 11, pp. 20–21]: under ETH, PartialMCSP on $m$-variable partial Boolean functions cannot be decided in time $2^{o(m \log m)} = N^{o(\log \log N)}$ under binary threshold encoding.

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_binaryGate (h : ETH) : ¬DecidableInSubexpTime PartialMCSP.BinaryGate PartialMCSP.enc fun (I : PartialMCSP.Instance) => I.arity * Nat.log 2 I.arity

Ilango's ETH Lower Bound for PartialMCSP.BinaryGate (unary threshold encoding) [Ilango2020FOCS, Section III.B, p. 427; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21]: under ETH, PartialMCSP.BinaryGate (circuit size measured by binary AND/OR gates) cannot be decided in time $2^{o(m \log m)} = N^{o(\log \log N)}$.

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_binaryGate_encBinary (h : ETH) : ¬DecidableInSubexpTime PartialMCSP.BinaryGate PartialMCSP.encBinary fun (I : PartialMCSP.Instance) => I.arity * Nat.log 2 I.arity

Ilango's ETH Lower Bound for PartialMCSP.BinaryGate (binary threshold encoding) [Ilango2020FOCS, Section III.B, p. 427; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21]: under ETH, PartialMCSP.BinaryGate cannot be decided in time $2^{o(m \log m)} = N^{o(\log \log N)}$ under binary threshold encoding.

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_monotoneReadOnce (h : ETH) : ¬DecidableInSubexpTime PartialMCSP.MonotoneReadOnce PartialMCSP.enc fun (I : PartialMCSP.Instance) => I.arity * Nat.log 2 I.arity

Ilango's ETH Lower Bound for PartialMCSP.MonotoneReadOnce (unary threshold encoding) [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21]: under ETH, even deciding whether a partial Boolean function has a monotone read-once formula of size at most threshold cannot be done in time $2^{o(m \log m)} = N^{o(\log \log N)}$.

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_monotoneReadOnce_encBinary (h : ETH) : ¬DecidableInSubexpTime PartialMCSP.MonotoneReadOnce PartialMCSP.encBinary fun (I : PartialMCSP.Instance) => I.arity * Nat.log 2 I.arity

Ilango's ETH Lower Bound for PartialMCSP.MonotoneReadOnce (binary threshold encoding) [Ilango2020FOCS, Section III.B, p. 428; ECCC TR20-183, Section 3, Theorem 11, pp. 20–21]: under ETH, PartialMCSP.MonotoneReadOnce cannot be decided in time $2^{o(m \log m)} = N^{o(\log \log N)}$ under binary threshold encoding.

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_tableSize (h : ETH) : ¬DecidableInSubexpTime PartialMCSP PartialMCSP.enc fun (I : PartialMCSP.Instance) => Nat.log 2 I.tableSize * Nat.log 2 (Nat.log 2 I.tableSize)

Truth-table-size ($N = 2^m$) formulation of Ilango's ETH Lower Bound for PartialMCSP [Ilango2020FOCS, Theorem I.3, p. 424; ECCC TR20-183, Section 1.2.2, Theorem 3, p. 6]: under ETH, PartialMCSP on partial truth tables of size $N = I.\text{tableSize} = 2^m$ is not decidable in time $N^{o(\log \log N)} = 2^{o(\log_2 N \cdot \log_2 \log_2 N)}$.

theorem Cslib.Complexity.ETH.not_decidableInSubexpTime_PartialMCSP_tableSize_encBinary (h : ETH) : ¬DecidableInSubexpTime PartialMCSP PartialMCSP.encBinary fun (I : PartialMCSP.Instance) => Nat.log 2 I.tableSize * Nat.log 2 (Nat.log 2 I.tableSize)

Truth-table-size ($N = 2^m$) formulation of Ilango's ETH Lower Bound for PartialMCSP (binary threshold encoding) [Ilango2020FOCS, Theorem I.3, p. 424; ECCC TR20-183, Section 1.2.2, Theorem 3, p. 6]: under ETH, PartialMCSP on partial truth tables of size $N = I.\text{tableSize} = 2^m$ is not decidable in time $N^{o(\log \log N)} = 2^{o(\log_2 N \cdot \log_2 \log_2 N)}$ under binary threshold encoding.