Not-all-equal semantics

CNF.evalNAE requires a true and a false literal in every clause, using the existing signed CNF representation. Empty and singleton clauses are false; the empty formula is true.

Main definitions

• CNF.evalNAE, CNF.NAESatisfiable: not-all-equal evaluation and satisfiability.

Main results

• CNF.evalNAE_complement: complementing all variables preserves evaluation.
• CNF.naeSatisfiable_relabel: injective variable renaming preserves satisfiability.

@[simp]

theorem Cslib.Logic.PL.Literal.eval_complement {V : Type u_1} (σ : V → Bool) (l : Literal V) : eval (fun (v : V) => !σ v) l = !eval σ l

Complementing every variable negates each literal's value.

def Cslib.Logic.PL.CNF.evalNAE {V : Type u_1} (σ : V → Bool) (φ : CNF V) : Bool

Each clause has both a true and a false literal.

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

Some assignment makes every clause not all equal.

@[simp]

theorem Cslib.Logic.PL.CNF.evalNAE_complement {V : Type u_1} (σ : V → Bool) (φ : CNF V) : evalNAE (fun (v : V) => !σ v) φ = evalNAE σ φ

Global complementation preserves not-all-equal evaluation.

theorem Cslib.Logic.PL.CNF.evalNAE_congr {V : Type u_1} {σ τ : V → Bool} {φ : CNF V} (h : ∀ (v : V), v ∈ φ.vars → σ v = τ v) : evalNAE σ φ = evalNAE τ φ

Not-all-equal evaluation depends only on the occurring variables.

theorem Cslib.Logic.PL.CNF.evalNAE_flatMap_eq_true_iff {V : Type u_1} {ι : Type u_3} (σ : V → Bool) (l : List ι) (f : ι → CNF V) : evalNAE σ (List.flatMap f l) = true ↔ ∀ (i : ι), i ∈ l → evalNAE σ (f i) = true

NAE satisfaction of a blockwise formula is satisfaction of every block.

@[simp]

theorem Cslib.Logic.PL.CNF.evalNAE_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (σ : W → Bool) (φ : CNF V) : evalNAE σ (relabel f φ) = evalNAE (σ ∘ f) φ

Relabelling evaluates the composite assignment.

theorem Cslib.Logic.PL.CNF.naeSatisfiable_relabel {V : Type u_1} {W : Type u_2} {f : V → W} (hf : Function.Injective f) (φ : CNF V) : (relabel f φ).NAESatisfiable ↔ φ.NAESatisfiable

Injective renaming preserves not-all-equal satisfiability.

def Cslib.Logic.PL.Clause.oneNAEEncoding {V : Type u_1} (t a b c : Literal V) : CNF V

An exact-one triple is encoded by four not-all-equal triples and a true reference literal.

theorem Cslib.Logic.PL.Clause.eval_oneNAEEncoding {V : Type u_1} (σ : V → Bool) (t a b c : Literal V) (ht : Literal.eval σ t = true) : CNF.evalNAE σ (oneNAEEncoding t a b c) = evalOne σ [a, b, c]

With a true reference literal, the four NAE clauses express exactly one true position.