Exact-one semantics for clauses

Clause.evalOne counts true literal occurrences, including repeated occurrences of the same variable. CNF.evalOne requires exactly one true literal in every clause. This reuses the existing signed CNF representation; positivity and clause-size restrictions are separate.

CNF.oneEncoding expresses these semantics with ordinary CNF clauses and no new variables. Unlike CNF.exactlyOne, which constrains distinct variables, this encoding counts positions.

Main definitions

• Clause.evalOne, CNF.evalOne, CNF.OneSatisfiable: exact-one semantics.
• Clause.oneEncoding, CNF.oneEncoding: the ordinary CNF encoding.

Main results

• CNF.eval_oneEncoding: correctness of the encoding under the same assignment.
• CNF.mem_vars_oneEncoding: the encoding has exactly the source variables.

References

• Hunt, Marathe, Radhakrishnan and Stearns, Definition 2.9.

def Cslib.Logic.PL.Clause.evalOne {V : Type u_1} (σ : V → Bool) (c : Clause V) : Bool

Exactly one literal occurrence of the clause is true.

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

Every clause has exactly one true literal occurrence.

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

Some assignment gives exactly one true literal occurrence in every clause.

@[simp]

theorem Cslib.Logic.PL.Clause.evalOne_nil {V : Type u_1} (σ : V → Bool) : evalOne σ [] = false

The empty clause cannot have exactly one true literal.

@[simp]

theorem Cslib.Logic.PL.Clause.evalOne_singleton {V : Type u_1} (σ : V → Bool) (l : Literal V) : evalOne σ [l] = Literal.eval σ l

A singleton exact-one clause has the same semantics as its literal.

theorem Cslib.Logic.PL.Clause.evalOne_eq_true_iff {V : Type u_1} (σ : V → Bool) (c : Clause V) : evalOne σ c = true ↔ List.countP (Literal.eval σ) c = 1

Exact-one satisfaction is the occurrence-count equation.

theorem Cslib.Logic.PL.CNF.evalOne_eq_true_iff {V : Type u_1} (σ : V → Bool) (φ : CNF V) : evalOne σ φ = true ↔ ∀ (c : Clause V), c ∈ φ → Clause.evalOne σ c = true

An assignment satisfies the exact-one formula when it satisfies every exact-one clause.

@[simp]

theorem Cslib.Logic.PL.CNF.evalOne_nil {V : Type u_1} (σ : V → Bool) : evalOne σ [] = true

The empty exact-one formula is true.

@[simp]

theorem Cslib.Logic.PL.CNF.evalOne_cons {V : Type u_1} (σ : V → Bool) (c : Clause V) (φ : CNF V) : evalOne σ (c :: φ) = (Clause.evalOne σ c && evalOne σ φ)

A cons of exact-one clauses evaluates conjunctively.

@[simp]

theorem Cslib.Logic.PL.CNF.evalOne_append {V : Type u_1} (σ : V → Bool) (φ ψ : CNF V) : evalOne σ (φ ++ ψ) = (evalOne σ φ && evalOne σ ψ)

Appending exact-one formulas conjoins their values.

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

A blockwise exact-one formula holds when every block does.

theorem Cslib.Logic.PL.Clause.evalOne_congr {V : Type u_1} {σ τ : V → Bool} {c : Clause V} (h : ∀ (l : Literal V), l ∈ c → σ l.fst = τ l.fst) : evalOne σ c = evalOne τ c

Clause exact-one evaluation depends only on the variables occurring in it.

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

Formula exact-one evaluation depends only on its variables.

@[simp]

theorem Cslib.Logic.PL.Clause.evalOne_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (σ : W → Bool) (c : Clause V) : evalOne σ (relabel f c) = evalOne (σ ∘ f) c

Exact-one clause evaluation commutes with relabelling.

@[simp]

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

Exact-one formula evaluation commutes with relabelling.

def Cslib.Logic.PL.Clause.atMostOneOccurrences {V : Type u_1} : Clause V → CNF V

Clauses forbidding simultaneous truth of each pair of literal positions.

def Cslib.Logic.PL.Clause.oneEncoding {V : Type u_1} (c : Clause V) : CNF V

Express exact-one clause semantics with ordinary clauses and no new variables.

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

Express exact-one formula semantics with ordinary clauses and no new variables.

theorem Cslib.Logic.PL.Clause.eval_atMostOneOccurrences {V : Type u_1} (σ : V → Bool) (c : Clause V) : CNF.eval σ c.atMostOneOccurrences = true ↔ List.countP (Literal.eval σ) c ≤ 1

The pair clauses constrain the true occurrence count to be at most one.

@[simp]

theorem Cslib.Logic.PL.Clause.eval_oneEncoding {V : Type u_1} (σ : V → Bool) (c : Clause V) : CNF.eval σ c.oneEncoding = evalOne σ c

Exact-one clause encoding preserves evaluation under the same assignment.

@[simp]

theorem Cslib.Logic.PL.CNF.eval_oneEncoding {V : Type u_1} (σ : V → Bool) (φ : CNF V) : eval σ φ.oneEncoding = evalOne σ φ

Exact-one formula encoding preserves evaluation under the same assignment.

theorem Cslib.Logic.PL.CNF.satisfiable_oneEncoding {V : Type u_1} (φ : CNF V) : φ.oneEncoding.Satisfiable ↔ φ.OneSatisfiable

The ordinary encoding is satisfiable exactly when the exact-one source is.

theorem Cslib.Logic.PL.Clause.fst_mem_of_mem_atMostOneOccurrences {V : Type u_1} {c d : Clause V} (hd : d ∈ c.atMostOneOccurrences) {l : Literal V} (hl : l ∈ d) : ∃ (k : Literal V), k ∈ c ∧ l.fst = k.fst

A variable in a pair clause already occurs in the source clause.

theorem Cslib.Logic.PL.CNF.mem_vars_oneEncoding {V : Type u_1} {φ : CNF V} {v : V} : v ∈ φ.oneEncoding.vars ↔ v ∈ φ.vars

The encoding has exactly the variables of the source, irrespective of repetitions.

theorem Cslib.Logic.PL.Clause.atMostOneOccurrences_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) : (relabel f c).atMostOneOccurrences = CNF.relabel f c.atMostOneOccurrences

The pair encoding commutes with renaming variables.

theorem Cslib.Logic.PL.Clause.oneEncoding_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (c : Clause V) : (relabel f c).oneEncoding = CNF.relabel f c.oneEncoding

The clause encoding commutes with renaming variables.

theorem Cslib.Logic.PL.CNF.oneEncoding_relabel {V : Type u_1} {W : Type u_2} (f : V → W) (φ : CNF V) : (relabel f φ).oneEncoding = relabel f φ.oneEncoding

The formula encoding commutes with renaming variables.