Documentation

DescriptiveComplexity.Problems.OneInSat.CountingFromSat

#SAT reduces parsimoniously to #1-in-SAT #

The reduction of 3SAT to 1-in-SAT in DescriptiveComplexity.Problems.OneInSat.Reduction uses the classical gadget, which gives some satisfying assignments two extensions: it preserves satisfiability, not the number of solutions. This file reduces #SAT to #1-in-SAT directly and parsimoniously (DescriptiveComplexity.sharpSat_ordered_parsimonious_sharpOneInSat), so #1-in-SAT is parsimoniously #P-complete (DescriptiveComplexity.sharpOneInSat_sharpP_parsimoniousComplete).

As in DescriptiveComplexity.Problems.ThreeSat.CountingFromSat, each occurrence (x, s) of a clause c has a prefix variable z, the truth of the disjunction of the occurrences of c up to it (DescriptiveComplexity.OccurrencePrefix). What changes is how z ↔ z' ∨ ℓ is said with exactly-one clauses, z' being the prefix variable of the preceding occurrence and ℓ the literal: three more variables name the cases z' ∧ ℓ, z' ∧ ¬ℓ and ¬z' ∧ ℓ, and three clauses,

{¬z', g₁₁, g₁₀}, {¬ℓ, g₁₁, g₀₁} and {¬z, g₁₁, g₁₀, g₀₁},

each with exactly one true literal, force them and z. The first occurrence of a clause has the clause {¬z, ℓ}, and the last one the unit clause {z}.

inductive DescriptiveComplexity.SharpSatToOneIn.GK :

The three clauses of the gate of an occurrence.

a : GK
{¬z', g₁₁, g₁₀}.
b : GK
{¬ℓ, g₁₁, g₀₁}.
c : GK
{¬z, g₁₁, g₁₀, g₀₁}.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToOneIn.instDecidableEqGK :

Equations

DescriptiveComplexity.SharpSatToOneIn.instDecidableEqGK x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToOneIn.instFintypeGK :

Equations

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

Dependency graph

inductive DescriptiveComplexity.SharpSatToOneIn.GI :

The three case variables of the gate of an occurrence.

tt : GI
z' ∧ ℓ.
tf : GI
z' ∧ ¬ℓ.
ft : GI
¬z' ∧ ℓ.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToOneIn.instDecidableEqGI :

Equations

DescriptiveComplexity.SharpSatToOneIn.instDecidableEqGI x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToOneIn.instFintypeGI :

Equations

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

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.gateIn :

GK → GI → Bool

Which case variables a gate clause contains.

Equations

Instances For

Dependency graph

inductive DescriptiveComplexity.SharpSatToOneIn.OTag :

Tags of the interpretation.

var : OTag
(.var, (x, x)) is the copy of the propositional variable x.
pre (s : Bool) : OTag
(.pre s, (c, x)) is the prefix variable of the occurrence (x, s) of the clause c.
g (i : GI) (s : Bool) : OTag
A case variable of the gate of an occurrence.
gk (k : GK) (s : Bool) : OTag
A clause of the gate of an occurrence that has a predecessor.
kd (s : Bool) : OTag
The clause {¬z, ℓ} of the first occurrence of a clause.
top (s : Bool) : OTag
The unit clause {z} of the last occurrence of a clause.
empty : OTag
(.empty, (c, c)) is the copy of the empty clause c.

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.instDecidableEqOTag.decEq (x✝ x✝¹ : OTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToOneIn.instDecidableEqOTag :

DecidableEq OTag

Equations

DescriptiveComplexity.SharpSatToOneIn.instDecidableEqOTag = DescriptiveComplexity.SharpSatToOneIn.instDecidableEqOTag.decEq

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToOneIn.instFintypeOTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.SharpSatToOneIn.instNonemptyOTag :

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToOneIn.isClauseF :

OTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for satIsClause.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToOneIn.posInF :

OTag → OTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for satPosIn.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SharpSatToOneIn.posInF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToOneIn.negInF :

OTag → OTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for satNegIn.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SharpSatToOneIn.negInF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToOneIn.interp :

FOInterpretation SatOcc.satOrd FirstOrder.Language.sat OTag 2

The parsimonious interpretation of 1-in-SAT instances in ordered CNF instances.

Equations

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

Instances For

Dependency graph

Characterization of the interpreted relations #

The literals of each clause #

def DescriptiveComplexity.SharpSatToOneIn.varP {A : Type} (x : A) :

The copy of the variable x.

Equations

DescriptiveComplexity.SharpSatToOneIn.varP x = (DescriptiveComplexity.SharpSatToOneIn.OTag.var , fun (x_1 : Fin 2) => x)

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.preP {A : Type} (s : Bool) (c x : A) :

The prefix variable of the occurrence (x, s) of c.

Equations

DescriptiveComplexity.SharpSatToOneIn.preP s c x = (DescriptiveComplexity.SharpSatToOneIn.OTag.pre s, ![c, x])

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.gP {A : Type} (i : GI) (s : Bool) (c x : A) :

A case variable of the gate of the occurrence (x, s) of c.

Equations

DescriptiveComplexity.SharpSatToOneIn.gP i s c x = (DescriptiveComplexity.SharpSatToOneIn.OTag.g i s, ![c, x])

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.pair_eq {A : Type} {t : OTag} {we : Fin 2 → A} {c x : A} (h0 : we 0 = c) (h1 : we 1 = x) :

(t, we) = (t, ![c, x])

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.var_eq {A : Type} {w we : Fin 2 → A} (h : SharpSatToThreeSat.OwnVar w we) :

(OTag.var , we) = varP (w 1)

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.chained_of_succOcc {A : Type} [instS : FirstOrder.Language.sat.Structure A] [LinearOrder A] {c y x : A} {t s : Bool} (h : SatOcc.SuccOcc c y t x s) :

SatOcc.Chained c x s

Dependency graph

Exactly-one assignments, read as gate valuations #

structure DescriptiveComplexity.SharpSatToOneIn.GateVal {A : Type} [instS : FirstOrder.Language.sat.Structure A] [instO : LinearOrder A] (ν : A → Prop) (Z : A → A → Bool → Prop) (G : GI → A → A → Bool → Prop) :

A gate valuation of the assignment ν: prefix values Z and case values G, each forced by ν along the occurrences of every clause, with the prefix value true at the last occurrence and no empty clause.

first (c x : A) (s : Bool) : SatOcc.MinOcc c x s → (Z c x s ↔ SatOcc.LitTrue ν x s)
At a first occurrence the prefix value is the literal.
gate (c y : A) (t : Bool) (x : A) (s : Bool) : SatOcc.SuccOcc c y t x s → (G GI.tt c x s ↔ Z c y t ∧ SatOcc.LitTrue ν x s) ∧ (G GI.tf c x s ↔ Z c y t ∧ ¬SatOcc.LitTrue ν x s) ∧ (G GI.ft c x s ↔ ¬Z c y t ∧ SatOcc.LitTrue ν x s) ∧ (Z c x s ↔ Z c y t ∨ SatOcc.LitTrue ν x s)
At an occurrence with a predecessor, the case values name the cases of the previous prefix value and the literal, and the prefix value is their disjunction.
last (c x : A) (s : Bool) : SatOcc.MaxOcc c x s → Z c x s
The prefix value at the last occurrence of a clause is true.
nonempty (c : A) : ¬SatOcc.EmptyCl c
No clause is empty.

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.varVal {A : Type} (μ : interp.Map A → Prop) (x : A) :

The assignment read on the variable copies.

Equations

DescriptiveComplexity.SharpSatToOneIn.varVal μ x = μ (DescriptiveComplexity.SharpSatToOneIn.varP x)

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.preVal {A : Type} (μ : interp.Map A → Prop) (c x : A) (s : Bool) :

The assignment read on the prefix variables.

Equations

DescriptiveComplexity.SharpSatToOneIn.preVal μ c x s = μ (DescriptiveComplexity.SharpSatToOneIn.preP s c x)

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToOneIn.gVal {A : Type} (μ : interp.Map A → Prop) (i : GI) (c x : A) (s : Bool) :

The assignment read on the case variables.

Equations

DescriptiveComplexity.SharpSatToOneIn.gVal μ i c x s = μ (DescriptiveComplexity.SharpSatToOneIn.gP i s c x)

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.ne_of_tag {A : Type} {t t' : OTag} {w w' : Fin 2 → A} (h : t ≠ t') :

(t, w) ≠ (t', w')

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.oneInProper_iff_gateVal {A : Type} [instS : FirstOrder.Language.sat.Structure A] [instO : LinearOrder A] {μ : interp.Map A → Prop} [Finite A] :

OneInProper μ ↔ GateVal (varVal μ) (preVal μ) (gVal μ)

Every clause of the interpreted instance has exactly one true literal exactly when the assignment is a gate valuation, read on the variable copies, the prefix variables and the case variables.

Dependency graph

The variables of the interpreted instance #

Exactly-one models of the interpreted instance are models of the input #

def DescriptiveComplexity.SharpSatToOneIn.canon {A : Type} [instS : FirstOrder.Language.sat.Structure A] [instO : LinearOrder A] (ν : A → Prop) :

OTag × (Fin 2 → A) → Prop

The assignment of the interpreted instance determined by an assignment of the input, before its restriction to the variables of the instance.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SharpSatToOneIn.canon ν (DescriptiveComplexity.SharpSatToOneIn.OTag.var , w) = ν (w 0)
DescriptiveComplexity.SharpSatToOneIn.canon ν (DescriptiveComplexity.SharpSatToOneIn.OTag.pre s, w) = DescriptiveComplexity.SatOcc.PrefixOr ν (w 0) (w 1) s
DescriptiveComplexity.SharpSatToOneIn.canon ν x✝ = False

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.val_congr {A : Type} {μ : interp.Map A → Prop} (t : OTag) {u u' : Fin 2 → A} (h : u = u') :

μ (t, u) ↔ μ (t, u')

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.gateVal_canon {A : Type} [instS : FirstOrder.Language.sat.Structure A] [instO : LinearOrder A] [Finite A] {ν : A → Prop} (hν : ∀ (c : A), SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) :

GateVal (varVal (canon ν)) (preVal (canon ν)) (gVal (canon ν))

A satisfying assignment has a gate valuation.

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToOneIn.modelEquiv (A : Type) [instS : FirstOrder.Language.sat.Structure A] [instO : LinearOrder A] [Finite A] :

{ ν : A → Prop // SatModel A ν } ≃ { μ : interp.Map A → Prop // OneInModel (interp.Map A) μ }

The exactly-one models of the interpreted instance are the models of the input, bijectively.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToOneIn.sharpOneInSat_map (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :

SharpOneInSAT.Count (interp.Map A) = SharpSAT.Count A

Correctness of the interpretation, for counting: the interpreted instance has as many exactly-one models as the input has models.

Dependency graph

noncomputable def DescriptiveComplexity.sharpSat_ordered_parsimonious_sharpOneInSat :

OrderedParsimoniousReduction SharpSAT SharpOneInSAT

#SAT reduces parsimoniously to #1-in-SAT.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.sharpOneInSat_sharpP_parsimoniousHard :

SharpP.ParsimoniousHard SharpOneInSAT

#1-in-SAT is parsimoniously #P-hard.

Dependency graph

theorem DescriptiveComplexity.sharpOneInSat_sharpP_parsimoniousComplete :

SharpP.ParsimoniousComplete SharpOneInSAT

#1-in-SAT is parsimoniously #P-complete. Registered in the Lax archive as Lax280166.OneInSATComplete.sharpOneInSat_sharpP_parsimoniousComplete.

Dependency graph

theorem DescriptiveComplexity.sharpOneInSat_sharpP_complete :

SharpP.Complete SharpOneInSAT

SharpOneInSAT is #P-complete: parsimoniously, hence under subtractive reductions.

Dependency graph