Random 3-SAT threshold

Definition3-clause#✓fully proved

A 3-clause on \(n\) variables is a pair \((S, p)\) of a three-element set \(S\) of variables among the \(n\) and a polarity \(p\) assigning a Boolean value to every variable, with \(p\) equal to false at every variable outside \(S\). This normalization gives each clause in the usual sense (a three-element variable set with one of \(2^3\) polarity patterns) exactly one representative.

def Clause (n : ℕ) :=
  { p : Finset (Fin n) × (Fin n → Bool) //
    p.1.card = 3 ∧ ∀ i : Fin n, i ∉ p.1 → p.2 i = false }

Used by 10

Used byClauses as variable sets with polarity patterns · 3-clauses exist on at least three variables · Satisfaction of a 3-clause · Satisfying a clause through a restricted assignment · Formulas of the random 3-SAT model · Satisfiability probability of random 3-SAT · Satisfiability probability with no clauses · Random 3-SAT satisfiability agrees with CNF satisfiability · CNF formula of a random 3-SAT formula · CNF clause of a random 3-SAT clause

AbbreviationFormulas of the random 3-SAT model#✓fully proved

A formula with \(m\) clauses on \(n\) variables is an ordered \(m\)-tuple of 3-clauses on \(n\) variables, that is, a function from \(\{0, \dots, m - 1\}\) to the set of 3-clauses on \(n\) variables.

With the uniform counting measure, this finite set of formulas is the sample space of \(m\) clauses chosen uniformly and independently, with replacement.

abbrev Formula (n m : ℕ) := Fin m → Clause n

Uses 1 · Used by 5

Statement uses3-clause

Used bySatisfiability probability of random 3-SAT · Satisfiability probability with no clauses · Satisfiable 3-SAT formulas · Random 3-SAT satisfiability agrees with CNF satisfiability · CNF formula of a random 3-SAT formula

DefinitionSatisfaction of a 3-clause#✓fully proved

An assignment \(a\) of Boolean values to \(n\) variables satisfies a 3-clause \(c\) on these variables when \(a\) gives at least one of the three variables of \(c\) the polarity that \(c\) prescribes for it.

def clauseSat {n : ℕ} (a : Fin n → Bool) (c : Clause n) : Prop :=
  ∃ i ∈ c.1.1, a i = c.1.2 i

Uses 1 · Used by 4

Statement uses3-clause

Used bySatisfying a clause through a restricted assignment · Satisfiability probability with no clauses · Satisfiable 3-SAT formulas · Random 3-SAT satisfiability agrees with CNF satisfiability

DefinitionSatisfiable 3-SAT formulas#✓fully proved

A formula \(F\) with \(m\) clauses on \(n\) variables is satisfiable when there is an assignment \(a\) of Boolean values to the \(n\) variables that satisfies every clause of \(F\), that is, \(a\) satisfies the 3-clause \(F(j)\) for every \(j \in \{0, \dots, m - 1\}\).

def Satisfiable {n m : ℕ} (F : Formula n m) : Prop :=
  ∃ a : Fin n → Bool, ∀ j : Fin m, clauseSat a (F j)

Uses 2 · Used by 3

Statement usesFormulas of the random 3-SAT model · Satisfaction of a 3-clause

Used bySatisfiability probability of random 3-SAT · Satisfiability probability with no clauses · Random 3-SAT satisfiability agrees with CNF satisfiability

DefinitionSatisfiability probability of random 3-SAT#✓fully proved

For natural numbers \(n\) and \(m\), the satisfiability probability \(p(n, m)\) is the number of satisfiable formulas with \(m\) clauses on \(n\) variables divided by the number of all such formulas, that is, the probability that a uniformly random formula with \(m\) clauses on \(n\) variables is satisfiable. When there are no such formulas, which happens exactly when \(n < 3\) and \(m > 0\), the quotient is taken to be \(0\); this affects only finitely many \(n\) in any asymptotic statement.

noncomputable def satProb (n m : ℕ) : ℝ :=
  (Fintype.card { F : Formula n m // Satisfiable F } : ℝ) /
    (Fintype.card (Formula n m) : ℝ)

Uses 3 · Used by 3

Statement uses3-clause · Formulas of the random 3-SAT model · Satisfiable 3-SAT formulas

Used byLower threshold cutoff · Upper threshold cutoff · Satisfiability probability with no clauses

Theorem3-clauses exist on at least three variables#✓fully proved

If \(n \ge 3\), then there is a 3-clause on \(n\) variables: take the first three variables, with polarity true on them and the normalized polarity false elsewhere.

theorem clause_nonempty {n : ℕ} (hn : 3 ≤ n) : Nonempty (Clause n)

Uses 1

Statement uses3-clause

TheoremSatisfiability probability with no clauses#✓fully proved

For every number \(n\) of variables, the probability that a uniformly random formula with \(0\) clauses on \(n\) variables is satisfiable is \(1\): the only such formula is the empty one, and every assignment satisfies it.

theorem satProb_zero (n : ℕ) : satProb n 0 = 1

Uses 5

Statement usesSatisfiability probability of random 3-SAT

Proof uses3-clause · Formulas of the random 3-SAT model · Satisfiable 3-SAT formulas · Satisfaction of a 3-clause

DefinitionUpper threshold cutoff#✓fully proved

A real number \(\rho\) is an upper threshold cutoff for random 3-SAT when, for every real \(r > \rho\), the probability that a uniformly random formula with \(\lfloor r n \rfloor\) clauses on \(n\) variables is satisfiable tends to \(0\) as \(n \to \infty\) (when \(r n < 0\) the formula has no clauses); equivalently, such a formula is unsatisfiable with probability tending to \(1\).

Literature upper bounds on the threshold are exactly cutoffs in this sense.

def IsUpperCutoff (ρ : ℝ) : Prop :=
  ∀ r : ℝ, ρ < r →
    Filter.Tendsto (fun n : ℕ => satProb n ⌊r * (n : ℝ)⌋₊) Filter.atTop (nhds 0)

Uses 1 · Used by 3

Statement usesSatisfiability probability of random 3-SAT

Used byDíaz–Kirousis–Mitsche–Pérez-Giménez upper bound for random 3-SAT · Random 3-SAT threshold conjecture · Upper threshold of random 3-SAT

DefinitionLower threshold cutoff#✓fully proved

A real number \(\rho\) is a lower threshold cutoff for random 3-SAT when, for every real \(r < \rho\), the probability that a uniformly random formula with \(\lfloor r n \rfloor\) clauses on \(n\) variables is satisfiable tends to \(1\) as \(n \to \infty\) (when \(r n < 0\) the formula has no clauses).

def IsLowerCutoff (ρ : ℝ) : Prop :=
  ∀ r : ℝ, r < ρ →
    Filter.Tendsto (fun n : ℕ => satProb n ⌊r * (n : ℝ)⌋₊) Filter.atTop (nhds 1)

Uses 1 · Used by 3

Statement usesSatisfiability probability of random 3-SAT

Used byHajiaghayi–Sorkin lower bound for random 3-SAT · Random 3-SAT threshold conjecture · Lower threshold of random 3-SAT

DefinitionUpper threshold of random 3-SAT#✓fully proved

The upper threshold is the infimum, in the real numbers, of the set of upper threshold cutoffs: the reals \(\rho\) such that, for every real \(r > \rho\), the probability that a uniformly random formula with \(\lfloor rn \rfloor\) clauses on \(n\) variables (no clauses when \(rn < 0\)) is satisfiable tends to \(0\) as \(n \to \infty\). The infimum is taken to be \(0\) when this set is empty or unbounded below.

Under the cutoff characterization of the source's Friedgut sequence \(r_{3,n}\), this is the limsup of that sequence.

noncomputable def upperThreshold : ℝ :=
  sInf { ρ : ℝ | IsUpperCutoff ρ }

Uses 1

Statement usesUpper threshold cutoff

DefinitionLower threshold of random 3-SAT#✓fully proved

The lower threshold is the supremum, in the real numbers, of the set of lower threshold cutoffs: the reals \(\rho\) such that, for every real \(r < \rho\), the probability that a uniformly random formula with \(\lfloor rn \rfloor\) clauses on \(n\) variables (no clauses when \(rn < 0\)) is satisfiable tends to \(1\) as \(n \to \infty\). The supremum is taken to be \(0\) when this set is empty or unbounded above.

It is the liminf counterpart of the upper threshold.

noncomputable def lowerThreshold : ℝ :=
  sSup { ρ : ℝ | IsLowerCutoff ρ }

Uses 1

Statement usesLower threshold cutoff

DefinitionRandom 3-SAT threshold conjecture#✓fully proved

There is a real number \(c\) that is both a lower and an upper threshold cutoff: for every real \(r < c\), the probability that a uniformly random formula with \(\lfloor r n \rfloor\) clauses on \(n\) variables is satisfiable tends to \(1\) as \(n \to \infty\), and for every real \(r > c\) this probability tends to \(0\) (when \(r n < 0\) the formula has no clauses).

This is stated as a proposition, not asserted: the existence of such a constant is open, whereas Friedgut's sharp-threshold theorem is proved.

def HasConstantThreshold : Prop :=
  ∃ c : ℝ, IsLowerCutoff c ∧ IsUpperCutoff c

Uses 2

Statement usesLower threshold cutoff · Upper threshold cutoff

DefinitionClauses as variable sets with polarity patterns#✓fully proved

For every \(n\), the 3-clauses on \(n\) variables correspond bijectively to the pairs \((S, q)\) of a three-element set \(S\) of variables among the \(n\) and a Boolean polarity \(q\) on the variables of \(S\): a clause is sent to its variable set together with its polarity restricted to that set.

CSLibExt.Combinatorics.RandomThreeSat.clauseEquiv · 23 lines

def clauseEquiv (n : ℕ) :
    Clause n ≃ Σ s : { s : Finset (Fin n) // s.card = 3 }, (s.1 : Type _) → Bool where
  toFun c := ⟨⟨c.1.1, c.2.1⟩, fun i => c.1.2 i.1⟩
  invFun sq :=
    ⟨(sq.1.1, fun i => if h : i ∈ sq.1.1 then sq.2 ⟨i, h⟩ else false), sq.1.2,
      fun i hi => by simp [hi]⟩
  left_inv c := by
    apply Subtype.ext
    show (c.1.1, fun i => if h : i ∈ c.1.1 then c.1.2 i else false) = c.1
    refine Prod.ext rfl ?_
    funext i
    by_cases h : i ∈ c.1.1
    · simp [h]
    · simp [h, c.2.2 i h]
  right_inv sq := by
    obtain ⟨⟨s, hs⟩, q⟩ := sq
    show (⟨⟨s, hs⟩, fun i : s => if h : i.1 ∈ s then q ⟨i.1, h⟩ else false⟩ :
        Σ s : { s : Finset (Fin n) // s.card = 3 }, (s.1 : Type _) → Bool) =
      ⟨⟨s, hs⟩, q⟩
    have hfun : (fun i : s => if h : i.1 ∈ s then q ⟨i.1, h⟩ else false) = q := by
      funext ⟨i, hi⟩
      simp [hi]
    rw [hfun]

Uses 1

Statement uses3-clause

DefinitionCNF clause of a random 3-SAT clause#✓fully proved

The CNF clause of a clause \(c\) on \(n\) variables is the list of literals \((i, b_i)\), one for each of the three variables \(i\) of \(c\) taken as a natural-number index, where \(b_i\) is the polarity that \(c\) prescribes for \(i\); the literals are listed in some fixed order.

noncomputable def toCNFClause {n : ℕ} (c : Clause n) : Cslib.Logic.PL.CNFClause :=
  c.1.1.toList.map (fun i => (i.val, c.1.2 i))

Uses 2 · Used by 3

Statement uses3-clause · CNF clause

Used bySatisfying a clause through a restricted assignment · Random 3-SAT satisfiability agrees with CNF satisfiability · CNF formula of a random 3-SAT formula

DefinitionExtension of an assignment by false#✓fully proved

An assignment \(a\) of Boolean values to the variables \(0, \dots, n - 1\) extends to all natural-number variables by giving variable \(i\) the value \(a(i)\) when \(i < n\) and the value false otherwise.

def extendAssign {n : ℕ} (a : Fin n → Bool) : ℕ → Bool :=
  fun i => if h : i < n then a ⟨i, h⟩ else false

Used by 1

Used byRandom 3-SAT satisfiability agrees with CNF satisfiability

TheoremSatisfying a clause through a restricted assignment#✓fully proved

Let \(A\) assign a Boolean value to every natural-number variable, and let \(c\) be a 3-clause on the \(n\) variables \(0, \dots, n - 1\). Then the restriction of \(A\) to these \(n\) variables satisfies \(c\) if and only if \(A\) satisfies the CNF clause of \(c\): the list with one literal \((i, p_i)\) for each of the three variables \(i\) of \(c\), where \(p_i\) is the polarity that \(c\) prescribes at \(i\). A CNF clause is satisfied when \(A\) gives the variable of at least one of its literals that literal's polarity.

theorem clauseSat_restrict_iff {n : ℕ} (A : ℕ → Bool) (c : Clause n) :
    clauseSat (fun i => A i.val) c ↔
      Cslib.Logic.PL.CNFClause.Satisfies A (toCNFClause c)

Uses 6 · Used by 1

Statement uses3-clause · Satisfaction of a 3-clause · CNF clause of a random 3-SAT clause · Satisfaction of a clause

Proof usesCNF clause · Satisfaction of a literal

Used byRandom 3-SAT satisfiability agrees with CNF satisfiability

DefinitionCNF formula of a random 3-SAT formula#✓fully proved

The CNF formula of a formula \(F\) with \(m\) clauses \(F_0, \dots, F_{m-1}\) on \(n\) variables is the list of the CNF clauses of \(F_0, \dots, F_{m-1}\), in this order.

noncomputable def toCNF {n m : ℕ} (F : Formula n m) : Cslib.Logic.PL.CNF :=
  (List.ofFn F).map toCNFClause

Uses 5 · Used by 1

Statement uses3-clause · Formulas of the random 3-SAT model · CNF clause of a random 3-SAT clause · CNF formula · CNF clause

Used byRandom 3-SAT satisfiability agrees with CNF satisfiability

TheoremRandom 3-SAT satisfiability agrees with CNF satisfiability#✓fully proved

A formula \(F\) with \(m\) clauses on \(n\) variables is satisfiable if and only if its CNF formula, which lists each clause of \(F\) as its three literals (variable index, polarity), is satisfiable as a CNF formula: some assignment of truth values to all natural-number variable indices makes at least one literal of every clause true.

theorem satisfiable_iff {n m : ℕ} (F : Formula n m) :
    Satisfiable F ↔ Cslib.Logic.PL.CNFSat (toCNF F)

Uses 15

Statement usesFormulas of the random 3-SAT model · Satisfiable 3-SAT formulas · CNF formula of a random 3-SAT formula · Satisfiability of a CNF formula

Proof uses3-clause · Satisfaction of a 3-clause · Satisfying a clause through a restricted assignment · Extension of an assignment by false · CNF clause of a random 3-SAT clause · CNF formula · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Satisfiability means having a satisfying assignment

TheoremDíaz–Kirousis–Mitsche–Pérez-Giménez upper bound for random 3-SAT#●ready to prove

The number \(4.49\) is an upper threshold cutoff for random 3-SAT: for every real \(r > 4.49\), the probability that a uniformly random formula with \(\lfloor r n \rfloor\) clauses on \(n\) variables is satisfiable tends to \(0\) as \(n \to \infty\).

theorem_wanted diazKirousisMitschePerezUpperBound_wanted :
    IsUpperCutoff (449 / 100 : ℝ)

Sources

• Díaz, Kirousis, Mitsche, and Pérez-Giménez, On the satisfiability threshold of formulas with three literals per clause (2009), catalogue upper bound 4.490.

Uses 1

Statement usesUpper threshold cutoff

TheoremHajiaghayi–Sorkin lower bound for random 3-SAT#●ready to prove

The number \(3.52\) is a lower threshold cutoff for random 3-SAT: for every real \(r < 3.52\), the probability that a uniformly random formula with \(\lfloor r n \rfloor\) clauses on \(n\) variables (no clauses when \(r < 0\)) is satisfiable tends to \(1\) as \(n \to \infty\).

theorem_wanted hajiaghayiSorkinLowerBound_wanted :
    IsLowerCutoff (352 / 100 : ℝ)

Sources

• Hajiaghayi and Sorkin, The satisfiability threshold of random 3-SAT is at least 3.52 (2003), and Kaporis, Kirousis, and Lalas (2003), catalogue lower bound 3.52.

Uses 1

Statement usesLower threshold cutoff

18 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.