Enumeration of k-SAT functions

DefinitionSatisfied clause#✓fully proved

Let \(n \in \mathbb{N}\). A clause on \(n\) variables is a finite set \(C\) of literals \((i, b)\), where \(i \in \{0, \dots, n - 1\}\) is a variable and \(b \in \{\mathrm{true}, \mathrm{false}\}\). An assignment \(x : \{0, \dots, n - 1\} \to \{\mathrm{true}, \mathrm{false}\}\) satisfies \(C\) if \(x_i = b\) for some literal \((i, b) \in C\).

def ClauseSatisfied {n : ℕ} (x : Fin n → Bool)
    (C : Finset (Fin n × Bool)) : Prop :=
  ∃ l ∈ C, x l.1 = l.2

Sources

• [OWR-10252930-018], k-SAT clause semantics.

Used by 1

Used by\(k\)-SAT function

Definition\(k\)-SAT function#✓fully proved

Let \(k, n \in \mathbb{N}\). A Boolean function \(f : \{\mathrm{true}, \mathrm{false}\}^n \to \{\mathrm{true}, \mathrm{false}\}\) is a \(k\)-SAT function on \(n\) variables if there is a finite set \(S\) of clauses on \(n\) variables such that each clause in \(S\) has at most \(k\) literals, no two of them on the same variable, and for every assignment \(x\), \(f(x) = \mathrm{true}\) if and only if \(x\) satisfies every clause in \(S\).

def IsKSATFunction (k n : ℕ) (f : (Fin n → Bool) → Bool) : Prop :=
  ∃ S : Finset (Finset (Fin n × Bool)),
    (∀ C ∈ S, C.card ≤ k ∧ ∀ l₁ ∈ C, ∀ l₂ ∈ C, l₁.1 = l₂.1 → l₁ = l₂) ∧
    ∀ x : Fin n → Bool, (f x = true ↔ ∀ C ∈ S, ClauseSatisfied x C)

Sources

• [OWR-10252930-018], k-SAT functions.

Uses 1 · Used by 2

Statement usesSatisfied clause

Used byNumber of \(k\)-SAT functions · Number of unate \(k\)-SAT functions

DefinitionPositively unate variable#✓fully proved

Let \(f : \{\mathrm{true}, \mathrm{false}\}^n \to \{\mathrm{true}, \mathrm{false}\}\) be a Boolean function and \(i\) one of its \(n\) variables. Then \(f\) is positively unate in \(i\) if for all assignments \(x\) and \(y\) that agree at every variable other than \(i\) and have \(x_i = \mathrm{false}\) and \(y_i = \mathrm{true}\), \(f(x) = \mathrm{true}\) implies \(f(y) = \mathrm{true}\). Equivalently, switching \(i\) from false to true never switches the value of \(f\) from true to false.

def IsPositiveUnateIn {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) : Prop :=
  ∀ x y : Fin n → Bool, x i = false → y i = true →
    (∀ j : Fin n, j ≠ i → x j = y j) → f x = true → f y = true

Sources

• [OWR-10252930-018], unate.

Used by 1

Used byUnate Boolean function

DefinitionNegatively unate variable#✓fully proved

Let \(f : \{\mathrm{true}, \mathrm{false}\}^n \to \{\mathrm{true}, \mathrm{false}\}\) be a Boolean function and \(i\) one of its \(n\) variables. Then \(f\) is negatively unate in \(i\) if for all assignments \(x\) and \(y\) that agree at every variable other than \(i\) and have \(x_i = \mathrm{false}\) and \(y_i = \mathrm{true}\), \(f(y) = \mathrm{true}\) implies \(f(x) = \mathrm{true}\). Equivalently, switching \(i\) from false to true never switches the value of \(f\) from false to true.

def IsNegativeUnateIn {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) : Prop :=
  ∀ x y : Fin n → Bool, x i = false → y i = true →
    (∀ j : Fin n, j ≠ i → x j = y j) → f y = true → f x = true

Sources

• [OWR-10252930-018], unate.

Used by 1

Used byUnate Boolean function

DefinitionUnate Boolean function#✓fully proved

A Boolean function \(f : \{\mathrm{true}, \mathrm{false}\}^n \to \{\mathrm{true}, \mathrm{false}\}\) is unate if, for every variable \(i\), \(f\) is positively unate in \(i\) or negatively unate in \(i\).

def IsUnate {n : ℕ} (f : (Fin n → Bool) → Bool) : Prop :=
  ∀ i : Fin n, IsPositiveUnateIn f i ∨ IsNegativeUnateIn f i

Sources

• [OWR-10252930-018], unate.

Uses 2 · Used by 1

Statement usesNegatively unate variable · Positively unate variable

Used byNumber of unate \(k\)-SAT functions

DefinitionNumber of \(k\)-SAT functions#✓fully proved

For natural numbers \(k\) and \(n\), the number of Boolean functions \(f : \{\mathrm{true}, \mathrm{false}\}^n \to \{\mathrm{true}, \mathrm{false}\}\) that are \(k\)-SAT functions on \(n\) variables.

noncomputable def countKSATFunctions (k n : ℕ) : ℕ :=
  Nat.card { f : (Fin n → Bool) → Bool // IsKSATFunction k n f }

Sources

• [OWR-10252930-018], enumeration of k-SAT functions.

Uses 1 · Used by 1

Statement uses\(k\)-SAT function

Used byBollobás–Brightwell–Leader conjecture for \(k\)

DefinitionNumber of unate \(k\)-SAT functions#✓fully proved

For natural numbers \(k\) and \(n\), the number of Boolean functions \(f : \{\mathrm{true}, \mathrm{false}\}^n \to \{\mathrm{true}, \mathrm{false}\}\) that are \(k\)-SAT functions on \(n\) variables and are unate.

noncomputable def countUnateKSATFunctions (k n : ℕ) : ℕ :=
  Nat.card { f : (Fin n → Bool) → Bool // IsKSATFunction k n f ∧ IsUnate f }

Sources

• [OWR-10252930-018], typical structure (unate).

Uses 2 · Used by 1

Statement uses\(k\)-SAT function · Unate Boolean function

Used byBollobás–Brightwell–Leader conjecture for \(k\)

DefinitionBollobás–Brightwell–Leader conjecture for \(k\)#✓fully proved

For a natural number \(k\), the proposition that if \(k \ge 2\), then the number of unate \(k\)-SAT functions on \(n\) Boolean variables divided by the number of \(k\)-SAT functions on \(n\) Boolean variables tends to \(1\) as \(n \to \infty\); that is, a \(1 - o(1)\) fraction of the \(k\)-SAT functions on \(n\) variables is unate.

noncomputable def conjecture (k : ℕ) : Prop :=
  2 ≤ k →
    Filter.Tendsto
      (fun n : ℕ =>
        (countUnateKSATFunctions k n : ℝ) / (countKSATFunctions k n : ℝ))
      Filter.atTop (nhds 1)

Sources

• [OWR-10252930-018], DOI 10.4171/owr/2022/22, arXiv:2107.09233.

Uses 2 · Used by 1

Statement usesNumber of \(k\)-SAT functions · Number of unate \(k\)-SAT functions

Used byBollobás–Brightwell–Leader conjecture for all \(k\)

DefinitionBollobás–Brightwell–Leader conjecture for all \(k\)#✓fully proved

The proposition that for every natural number \(k \ge 2\), the number of unate \(k\)-SAT functions on \(n\) Boolean variables divided by the number of \(k\)-SAT functions on \(n\) Boolean variables tends to \(1\) as \(n \to \infty\).

def conjectureAllK : Prop :=
  ∀ k : ℕ, conjecture k

Uses 1 · Used by 1

Statement usesBollobás–Brightwell–Leader conjecture for \(k\)

Used byNearly all \(k\)-SAT functions are unate

TheoremNearly all \(k\)-SAT functions are unate#●ready to prove

For every natural number \(k \ge 2\), the number of unate \(k\)-SAT functions on \(n\) Boolean variables divided by the number of \(k\)-SAT functions on \(n\) Boolean variables tends to \(1\) as \(n \to \infty\); that is, the Bollobás–Brightwell–Leader conjecture holds for every \(k\).

Balogh, Dong, Lidický, Mani and Zhao prove this as Theorem 1.1 of arXiv:2209.04894. They use a DNF convention with exactly \(k\) distinct variables per clause, which gives the same counts as the CNF, at-most-\(k\) convention here for \(n \ge k\) (negation preserves unateness).

public theorem_wanted conjectureAllK_holds : conjectureAllK

Sources

• J. Balogh, D. Dong, B. Lidický, N. Mani, Y. Zhao, Nearly all k-SAT functions are unate, STOC 2023; J. Eur. Math. Soc. (2026), arXiv:2209.04894, https://arxiv.org/abs/2209.04894.

Uses 1

Statement usesBollobás–Brightwell–Leader conjecture for all \(k\)

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.