Exact-three distinct-variable formulas with three occurrences are satisfiable

Hall's theorem chooses a different representative variable for every clause. Setting each representative to satisfy its clause is consistent even with arbitrary literal signs.

This is Tovey's tractable boundary, recalled in Berman, Karpinski and Scott, §1, pp. 1–2 of the linked preprint. The Lean version uses lists, counts repeated clauses separately, permits unused variables, and assumes at most three occurrences per variable. Each clause has exactly three distinct variables. No computational bound for constructing the matching or satisfying assignment is asserted here.

Main results

• CNF.satisfiable_of_exactThreeDistinct_of_count_le_three.

theorem Cslib.Logic.PL.CNF.satisfiable_of_exactThreeDistinct_of_count_le_three {V : Type u_1} [DecidableEq V] {φ : CNF V} (hw : φ.IsExactThreeDistinct) (ho : ∀ (v : V), List.count v φ.vars ≤ 3) : φ.Satisfiable

Exact-three clauses on distinct variables with at most three occurrences per variable are always satisfiable. Binary clauses are excluded from this statement.