Unsatisfiability value of CNF formulas and the 7 / 8 random-assignment bound

The unsatisfiability value CNF.unsatVal φ of a formula in conjunctive normal form is the least proportion of its clauses, counted with multiplicity, that an assignment falsifies (CNF.countUnsat). The value vanishes on the empty formula and on satisfiable formulas (CNF.unsatVal_eq_zero_iff), and 1 - CNF.unsatVal φ is the value of φ as an instance of MAX-SAT.

When the three variables of every clause are distinct (CNF.IsExactThreeDistinct), a uniform random assignment falsifies each clause with probability 1 / 8 (Clause.IsExactThreeDistinct.expect_eval_eq_false), so some assignment falsifies at most 1 / 8 of the clauses (CNF.IsExactThreeDistinct.unsatVal_le_one_eighth). Håstad showed that this 7 / 8 threshold is optimal [Has01].

Main definitions

• Cslib.Logic.PL.CNF.unsatVal: the least proportion of falsified clauses.
• Cslib.Logic.PL.Clause.IsExactThreeDistinct, Cslib.Logic.PL.CNF.IsExactThreeDistinct: clauses and formulas with three distinct variables per clause.

Main results

• Cslib.Logic.PL.CNF.countUnsat_eq_card: the number of falsified clauses as a cardinality over clause indices.
• Cslib.Logic.PL.CNF.unsatVal_eq_zero_iff: the value vanishes exactly on satisfiable formulas.
• Cslib.Logic.PL.CNF.length_pos_of_unsatVal_pos: a formula of positive value has a clause.
• Cslib.Logic.PL.Clause.IsExactThreeDistinct.expect_eval_eq_false, Cslib.Logic.PL.Clause.IsExactThreeDistinct.expect_eval_eq_true: a uniform random assignment falsifies a clause with three distinct variables with probability 1 / 8.
• Cslib.Logic.PL.CNF.IsExactThreeDistinct.unsatVal_le_one_eighth, Cslib.Logic.PL.CNF.IsExactThreeDistinct.exists_countUnsat_le_div_eight: the 7 / 8 random-assignment bound.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 11
• J. Håstad, Some optimal inapproximability results

Counting falsified clauses

theorem Cslib.Logic.PL.CNF.countUnsat_eq_card {V : Type u_1} (σ : V → Bool) (φ : CNF V) : countUnsat σ φ = {j : Fin (List.length φ) | Clause.eval σ φ[j] = false}.card

The number of falsified clauses, counted by their positions in the formula.

theorem Cslib.Logic.PL.CNF.countUnsat_relabel {V : Type u_1} {W : Type u_2} (φ : CNF V) (f : V → W) (τ : W → Bool) : countUnsat τ (relabel f φ) = countUnsat (τ ∘ f) φ

Relabelling counts the falsified clauses of the composite assignment.

The value of a formula

noncomputable def Cslib.Logic.PL.CNF.unsatVal {V : Type u_1} (φ : CNF V) : ℝ

The unsatisfiability value of a formula: the least proportion of its clauses, counted with multiplicity, that an assignment falsifies. The formula without clauses has value zero.

theorem Cslib.Logic.PL.CNF.unsatVal_le {V : Type u_1} (φ : CNF V) (σ : V → Bool) : φ.unsatVal ≤ ↑(countUnsat σ φ) / ↑(List.length φ)

The value is at most the proportion of the clauses that any assignment falsifies.

theorem Cslib.Logic.PL.CNF.unsatVal_nonneg {V : Type u_1} (φ : CNF V) : 0 ≤ φ.unsatVal

The value is nonnegative.

theorem Cslib.Logic.PL.CNF.le_unsatVal_iff {V : Type u_1} (φ : CNF V) {c : ℝ} : c ≤ φ.unsatVal ↔ ∀ (σ : V → Bool), c ≤ ↑(countUnsat σ φ) / ↑(List.length φ)

A lower bound on the value bounds the proportion falsified by every assignment.

theorem Cslib.Logic.PL.CNF.exists_countUnsat_div_eq_unsatVal {V : Type u_1} (φ : CNF V) : ∃ (σ : V → Bool), ↑(countUnsat σ φ) / ↑(List.length φ) = φ.unsatVal

The minimum is attained: the proportions take finitely many values.

theorem Cslib.Logic.PL.CNF.unsatVal_eq_zero_iff {V : Type u_1} (φ : CNF V) : φ.unsatVal = 0 ↔ φ.Satisfiable

The value vanishes exactly on satisfiable formulas.

theorem Cslib.Logic.PL.CNF.length_pos_of_unsatVal_pos {V : Type u_1} {φ : CNF V} (h : 0 < φ.unsatVal) : 0 < List.length φ

A formula in which every assignment falsifies a positive proportion of the clauses has a clause.

Exact 3-clauses with distinct variables and the 7 / 8 random assignment bound

def Cslib.Logic.PL.Clause.IsExactThreeDistinct {V : Type u_1} (c : Clause V) : Prop

A clause has three distinct variables when it has length 3 and its variables have no duplicates.

def Cslib.Logic.PL.CNF.IsExactThreeDistinct {V : Type u_1} (φ : CNF V) : Prop

A formula is an exact 3-CNF with distinct variables per clause when every clause has three distinct variables.

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableIsExactThreeDistinctOfDecidableEq {V : Type u_1} [DecidableEq V] {c : Clause V} : Decidable c.IsExactThreeDistinct

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableIsExactThreeDistinctOfDecidableEq_1 {V : Type u_1} [DecidableEq V] {φ : CNF V} : Decidable φ.IsExactThreeDistinct

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.length_eq {V : Type u_1} {c : Clause V} (hc : c.IsExactThreeDistinct) : List.length c = 3

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.nodup_map_fst {V : Type u_1} {c : Clause V} (hc : c.IsExactThreeDistinct) : (List.map Prod.fst c).Nodup

theorem Cslib.Logic.PL.Clause.isExactThreeDistinct_iff {V : Type u_1} {c : Clause V} : c.IsExactThreeDistinct ↔ ∃ (l₁ : Literal V) (l₂ : Literal V) (l₃ : Literal V), c = [l₁, l₂, l₃] ∧ l₁.1 ≠ l₂.1 ∧ l₁.1 ≠ l₃.1 ∧ l₂.1 ≠ l₃.1

Every exact 3-clause with distinct variables is a list of three literals on pairwise distinct variables.

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.expect_eval_eq_false {ι : Type u_3} [Fintype ι] [DecidableEq ι] {c : Clause ι} (hc : c.IsExactThreeDistinct) : (Finset.univ.expect fun (σ : ι → Bool) => if eval σ c = true then 0 else 1) = 1 / 8

A uniform random assignment falsifies any 3-clause on three distinct variables with probability 1 / 8.

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.expect_eval_eq_true {ι : Type u_3} [Fintype ι] [DecidableEq ι] {c : Clause ι} (hc : c.IsExactThreeDistinct) : (Finset.univ.expect fun (σ : ι → Bool) => if eval σ c = true then 1 else 0) = 7 / 8

A uniform random assignment satisfies any 3-clause on three distinct variables with probability 7 / 8.

theorem Cslib.Logic.PL.Clause.IsExactThreeDistinct.card_eval_eq_true {c : Clause (Fin 3)} (hc : c.IsExactThreeDistinct) : {σ : Fin 3 → Bool | eval σ c = true}.card = 7

Over the 3-bit cube Fin 3 → Bool, any 3-clause on three distinct variables is satisfied by exactly 7 of the 8 truth assignments.

theorem Cslib.Logic.PL.CNF.IsExactThreeDistinct.unsatVal_le_one_eighth {V : Type u_1} {φ : CNF V} (hφ : φ.IsExactThreeDistinct) : φ.unsatVal ≤ 1 / 8

The 7 / 8 random-assignment bound: in every exact 3-CNF formula φ with three distinct variables per clause, some assignment falsifies at most 1 / 8 of the clauses (φ.unsatVal ≤ 1 / 8), hence satisfies at least 7 / 8 of the clauses.

theorem Cslib.Logic.PL.CNF.IsExactThreeDistinct.exists_countUnsat_le_div_eight {V : Type u_1} {φ : CNF V} (hφ : φ.IsExactThreeDistinct) : ∃ (σ : V → Bool), ↑(countUnsat σ φ) ≤ ↑(List.length φ) / 8

In every exact 3-CNF formula φ with three distinct variables per clause, there exists an assignment falsifying at most φ.length / 8 clauses (equivalently satisfying at least 7 / 8 * φ.length clauses).