Exact-three ordinary clauses for exact-one semantics

A triple's exact-one predicate is expressed by five ordinary clauses on its original variables: one excludes zero true literals and four exclude the assignments with at least two true literals. This original truth-table encoding preserves distinctness and introduces no new variables.

Main definitions

• Clause.oneThreeEncoding: five clauses on a given triple of literals.

Main results

• Clause.eval_oneThreeEncoding: correctness under the same assignment.
• Clause.isExactThreeDistinct_oneThreeEncoding: preservation of distinct variables.

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

A truth-table encoding of exactly one true literal among three literal positions.

theorem Cslib.Logic.PL.Clause.eval_oneThreeEncoding {V : Type u_1} (σ : V → Bool) (a b c : Literal V) : CNF.eval σ (oneThreeEncoding a b c) = evalOne σ [a, b, c]

The five ordinary clauses express positional exact-one semantics.

theorem Cslib.Logic.PL.Clause.isExactThreeDistinct_oneThreeEncoding {V : Type u_1} (a b c : Literal V) (h : IsExactThreeDistinct [a, b, c]) : (oneThreeEncoding a b c).IsExactThreeDistinct

Distinct source variables give three distinct variables in every emitted clause.