Directed implication cycles

A binary implication cycle forces all its variables to have the same Boolean value. Each listed variable contributes exactly two literal occurrences, including the two occurrences in a singleton cycle. Repeated variables are counted with multiplicity. These are the implication cycles used in Papadimitriou, Proposition 9.3.

Adapted from the cycle construction in lean-trominoes, revision 6d5b36c15cec6cb18d30137b7f1c7fb92ea24332, PeriodicThreeSATThree.lean, PeriodicThreeSATThreeCorrectness.lean, and PeriodicThreeSATThreeExactSize.lean. No periodic semantics is used here.

Main definitions

• Cslib.Logic.PL.CNF.implicationCycle: binary implications around a list.

Main results

• Cslib.Logic.PL.CNF.eval_implicationCycle: a cycle holds exactly when all listed values agree.
• Cslib.Logic.PL.CNF.length_implicationCycle: one clause per listed variable.
• Cslib.Logic.PL.CNF.count_vars_implicationCycle: two occurrences per listed variable.

References

• C. H. Papadimitriou, Computational Complexity, Proposition 9.3

def Cslib.Logic.PL.CNF.implicationPath {V : Type u_1} (first : V) : V → List V → CNF V

An implication path from current through rest, closed back to first.

def Cslib.Logic.PL.CNF.implicationCycle {V : Type u_1} : List V → CNF V

Binary implications around a list, including a tautological clause for a singleton.

theorem Cslib.Logic.PL.CNF.eval_implicationCycle {V : Type u_1} (σ : V → Bool) (vs : List V) : eval σ (implicationCycle vs) = true ↔ ∀ (x : V), x ∈ vs → ∀ (y : V), y ∈ vs → σ x = σ y

A cycle holds exactly when all variables listed in it have the same value.

@[simp]

theorem Cslib.Logic.PL.CNF.length_implicationCycle {V : Type u_1} (vs : List V) : List.length (implicationCycle vs) = vs.length

There is one binary clause per element of the cycle list.

theorem Cslib.Logic.PL.CNF.length_of_mem_implicationCycle {V : Type u_1} (vs : List V) {c : Clause V} (hc : c ∈ implicationCycle vs) : List.length c = 2

Every implication-cycle clause has exactly two literals.

theorem Cslib.Logic.PL.CNF.count_vars_implicationCycle {V : Type u_1} [DecidableEq V] (vs : List V) (v : V) : List.count v (implicationCycle vs).vars = 2 * List.count v vs

A variable occurs twice per appearance in the cycle list, including repeated entries.