1-in-SAT: the problem, and its membership in NP

EXACTLY-ONE SATISFIABILITY: is there a truth assignment giving every clause exactly one true literal? Like NAE-SAT, it lives on the vocabulary FirstOrder.Language.sat unchanged and only its notion of satisfaction differs (DescriptiveComplexity.OneInProper), so this adds a problem rather than a language. It is the second Schaefer-style variant of satisfiability (Schaefer 1978) in the catalog.

Its value is as a reduction source, and specifically for Exact Cover: a 1-in-SAT instance becomes an exact cover with no counting and no gadget at all, one set per literal (x, s) gathering x itself and the clauses where (x, s) occurs. Covering the element x exactly once picks exactly one of the two literals of x – an assignment – and covering a clause exactly once is exactly-one satisfaction. That works at any clause width, which is why the catalog wants unrestricted 1-in-SAT rather than a width-three restriction.

Membership reuses SAT's kernel (DescriptiveComplexity.realize_satKernel, “every clause has a true literal”) and adds uniqueness, as three clauses – one per pattern of signs, the mixed pattern being simply forbidden.

The problem

def DescriptiveComplexity.OneInProper {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) : Prop

An assignment is exactly-one proper when every clause has exactly one true literal occurrence.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.OneInSatisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

A Language.sat-structure is exactly-one satisfiable if some assignment gives every clause exactly one true literal.

Equations

• DescriptiveComplexity.OneInSatisfiable A = ∃ (ν : A → Prop), DescriptiveComplexity.OneInProper ν

theorem DescriptiveComplexity.occIn_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) {c x : A} {s : Bool} : SatOcc.OccIn c x s ↔ SatOcc.OccIn (e c) (e x) s

Isomorphisms preserve literal occurrences.

theorem DescriptiveComplexity.oneInSatisfiable_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) : OneInSatisfiable A ↔ OneInSatisfiable B

Exactly-one satisfiability is isomorphism-invariant.

def DescriptiveComplexity.OneInSAT : DecisionProblem FirstOrder.Language.sat

1-in-SAT, as a problem on CNF instances: is there an assignment giving every clause exactly one true literal?

Equations

• DescriptiveComplexity.OneInSAT = { Holds := fun (A : Type) (inst : FirstOrder.Language.sat.Structure A) => DescriptiveComplexity.OneInSatisfiable A, iso_invariant := ⋯ }

Membership

noncomputable def DescriptiveComplexity.oneInKernel : satSOLang.Sentence

The first-order kernel of the Σ₁ definition of 1-in-SAT: SAT's kernel together with the three uniqueness clauses.

Equations

• DescriptiveComplexity.oneInKernel = DescriptiveComplexity.satKernel ⊓ (DescriptiveComplexity.oiPPClause✝ ⊓ (DescriptiveComplexity.oiNNClause✝ ⊓ DescriptiveComplexity.oiPNClause✝))

theorem DescriptiveComplexity.oneInSat_sigmaSODefinable : SigmaSODefinable 1 OneInSAT

1-in-SAT is Σ₁-definable: guess the assignment, then check first-order that every clause has a true literal – SAT's kernel – and that it has no second one.