Occurrence splitting for not-all-equal clauses

The ordinary occurrence splitter also preserves not-all-equal satisfiability. Its binary implication cycles become equality constraints under NAE semantics. The existing width, occurrence and polynomial-time bounds apply unchanged. Binary clauses are essential here.

Main results

• CNF.naeSatisfiable_toThreeOccurrence: NAE satisfiability is preserved.

theorem Cslib.Logic.PL.CNF.naeSatisfiable_toThreeOccurrence {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.toThreeOccurrence.NAESatisfiable ↔ φ.NAESatisfiable

The existing occurrence splitter preserves not-all-equal satisfiability.