Documentation

DescriptiveComplexity.Problems.ThreeSat.CountingFromSat

#SAT reduces parsimoniously to #3SAT #

The clause-splitting reduction of DescriptiveComplexity.Problems.ThreeSat.FromSat threads fresh variables along the occurrences of a clause, and leaves them free once the clause is satisfied; it preserves satisfiability, not the number of models. This file is the variant that preserves it, DescriptiveComplexity.sharpSat_ordered_parsimonious_sharpThreeSat, which makes #3SAT parsimoniously #P-complete (DescriptiveComplexity.sharpThreeSat_sharpP_parsimoniousComplete).

For each occurrence (x, s) of a clause c, the interpretation (DescriptiveComplexity.SharpSatToThreeSat.interp, dimension 2) has a variable z = (.pre s, (c, x)), forced to be the truth of the disjunction of the occurrences of c up to (x, s) by three clauses, with z' the variable of the preceding occurrence when there is one:

(.k0 s, (c, x)): ¬z ∨ ℓ ∨ z';
(.k1 s, (c, x)): z ∨ ¬ℓ;
(.k2 s, (c, x)): z ∨ ¬z';

and the last occurrence of c carries the unit clause (.top s, (c, x)): z. Empty clauses are copied as empty clauses. That such z are determined by the assignment, and exist exactly when it satisfies every clause, is the interpretation-free content of DescriptiveComplexity.OccurrencePrefix.

inductive DescriptiveComplexity.SharpSatToThreeSat.PTag :

Tags of the parsimonious clause-splitting interpretation.

var : PTag
(.var, (x, x)) is the copy of the propositional variable x.
pre (s : Bool) : PTag
(.pre s, (c, x)) is the prefix variable of the occurrence (x, s) of the clause c.
k0 (s : Bool) : PTag
The clause ¬z ∨ ℓ ∨ z' of an occurrence.
k1 (s : Bool) : PTag
The clause z ∨ ¬ℓ of an occurrence.
k2 (s : Bool) : PTag
The clause z ∨ ¬z' of an occurrence that has a predecessor.
top (s : Bool) : PTag
The unit clause z of the last occurrence of a clause.
empty : PTag
(.empty, (c, c)) is the copy of the empty clause c.

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.instDecidableEqPTag.decEq (x✝ x✝¹ : PTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToThreeSat.instDecidableEqPTag :

DecidableEq PTag

Equations

DescriptiveComplexity.SharpSatToThreeSat.instDecidableEqPTag = DescriptiveComplexity.SharpSatToThreeSat.instDecidableEqPTag.decEq

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.SharpSatToThreeSat.instFintypePTag :

Equations

DescriptiveComplexity.SharpSatToThreeSat.instFintypePTag = Fintype.ofEquiv (Unit ⊕ Bool ⊕ Bool ⊕ Bool ⊕ Bool ⊕ Bool ⊕ Unit) DescriptiveComplexity.SharpSatToThreeSat.PTag.proxyTypeEquiv

Dependency graph

instance DescriptiveComplexity.SharpSatToThreeSat.instNonemptyPTag :

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.ownVarF :

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

The second argument is the variable copy of the variable of the first.

Equations

DescriptiveComplexity.SharpSatToThreeSat.ownVarF = DescriptiveComplexity.SatOcc.eqF (1, 0) (1, 1) ⊓ DescriptiveComplexity.SatOcc.eqF (1, 0) (0, 1)

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.sameF :

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

The two arguments sit on the same pair.

Equations

DescriptiveComplexity.SharpSatToThreeSat.sameF = DescriptiveComplexity.SatOcc.eqF (0, 0) (1, 0) ⊓ DescriptiveComplexity.SatOcc.eqF (0, 1) (1, 1)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToThreeSat.predF (t s : Bool) :

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

The second argument sits on the occurrence (y, t) of the same clause immediately preceding the occurrence (x, s) of the first.

Equations

DescriptiveComplexity.SharpSatToThreeSat.predF t s = DescriptiveComplexity.SatOcc.eqF (0, 0) (1, 0) ⊓ DescriptiveComplexity.SatOcc.succOccF t s (0, 0) (1, 1) (0, 1)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToThreeSat.isClauseF :

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

Defining formula for satIsClause.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToThreeSat.posInF :

PTag → PTag → 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.SharpSatToThreeSat.posInF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToThreeSat.negInF :

PTag → PTag → 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.SharpSatToThreeSat.negInF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SharpSatToThreeSat.interp :

FOInterpretation SatOcc.satOrd FirstOrder.Language.sat PTag 2

The parsimonious clause-splitting interpretation.

Equations

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

Instances For

Dependency graph

Characterization of the interpreted relations #

def DescriptiveComplexity.SharpSatToThreeSat.OwnVar {A : Type} (w₁ w₂ : Fin 2 → A) :

The second pair is the diagonal on the variable of the first.

Equations

DescriptiveComplexity.SharpSatToThreeSat.OwnVar w₁ w₂ = (w₂ 0 = w₂ 1 ∧ w₂ 0 = w₁ 1)

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.Same {A : Type} (w₁ w₂ : Fin 2 → A) :

The two pairs are the same.

Equations

DescriptiveComplexity.SharpSatToThreeSat.Same w₁ w₂ = (w₁ 0 = w₂ 0 ∧ w₁ 1 = w₂ 1)

Instances For

Dependency graph

Assignments of the split, read as prefix valuations #

theorem DescriptiveComplexity.SharpSatToThreeSat.eta2 {A : Type} (w : Fin 2 → A) :

![w 0, w 1] = w

Dependency graph

theorem DescriptiveComplexity.SharpSatToThreeSat.ownVar_eq {A : Type} {w₁ w₂ : Fin 2 → A} (h : OwnVar w₁ w₂) :

w₂ = fun (x : Fin 2) => w₁ 1

Dependency graph

theorem DescriptiveComplexity.SharpSatToThreeSat.same_eq {A : Type} {w₁ w₂ : Fin 2 → A} (h : Same w₁ w₂) :

w₂ = w₁

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.varVal {A : Type} (ν' : interp.Map A → Prop) (x : A) :

The assignment read on the variable copies.

Equations

DescriptiveComplexity.SharpSatToThreeSat.varVal ν' x = ν' (DescriptiveComplexity.SharpSatToThreeSat.PTag.var , fun (x_1 : Fin 2) => x)

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.preVal {A : Type} (ν' : interp.Map A → Prop) (c x : A) (s : Bool) :

The assignment read on the prefix variables.

Equations

DescriptiveComplexity.SharpSatToThreeSat.preVal ν' c x s = ν' (DescriptiveComplexity.SharpSatToThreeSat.PTag.pre s, ![c, x])

Instances For

Dependency graph

def DescriptiveComplexity.SharpSatToThreeSat.HasTrue {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν' : interp.Map A → Prop) (K : interp.Map A) :

The clause K contains a literal made true by ν'.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToThreeSat.val_congr {A : Type} {ν' : interp.Map A → Prop} (t : PTag) {u u' : Fin 2 → A} (h : u = u') :

ν' (t, u) ↔ ν' (t, u')

Dependency graph

theorem DescriptiveComplexity.SharpSatToThreeSat.allTrue_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν' : interp.Map A → Prop} [Finite A] :

(∀ (K : interp.Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![K] → HasTrue ν' K) ↔ SatOcc.PrefixVal (varVal ν') (preVal ν')

Every clause of the split has a true literal exactly when the assignment is a prefix valuation, read on the variable copies and the prefix variables.

Dependency graph

The variables of the split #

theorem DescriptiveComplexity.SharpSatToThreeSat.satOccurs_iff_occIn {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :

SatOccurs A x ↔ ∃ (c : A) (s : Bool), SatOcc.OccIn c x s

Dependency graph

Models of the split are models of the input #

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

PTag × (Fin 2 → A) → Prop

The assignment of the split determined by an assignment of the input, before its restriction to the variables of the split: variable copies follow it, and a prefix variable is the truth of its prefix disjunction.

Equations

DescriptiveComplexity.SharpSatToThreeSat.canon ν (DescriptiveComplexity.SharpSatToThreeSat.PTag.var , w) = ν (w 0)
DescriptiveComplexity.SharpSatToThreeSat.canon ν (DescriptiveComplexity.SharpSatToThreeSat.PTag.pre s, w) = DescriptiveComplexity.SatOcc.PrefixOr ν (w 0) (w 1) s
DescriptiveComplexity.SharpSatToThreeSat.canon ν x✝ = False

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToThreeSat.satModel_occ {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (h : SatModel A ν) (c : A) :

SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s

Dependency graph

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

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

The models of the split are the models of the input, bijectively: a model of the input extends by the truth of its prefix disjunctions, and a model of the split is recovered from its variable copies because the prefix variables are determined.

Equations

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

Instances For

Dependency graph

The width bound #

def DescriptiveComplexity.SharpSatToThreeSat.code :

PTag → Bool → Fin 3

A code for the literals of a clause, in three values: the variable copy, the prefix variable occurring positively, the one occurring negatively.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.SharpSatToThreeSat.code_var (sg : Bool) :

code PTag.var sg = 0

Dependency graph

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

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

Correctness of the interpretation, for counting: the split has as many models as the input.

Dependency graph

noncomputable def DescriptiveComplexity.sharpSat_ordered_parsimonious_sharpThreeSat :

OrderedParsimoniousReduction SharpSAT SharpThreeSAT

#SAT reduces parsimoniously to #3SAT: the clause-splitting interpretation with determined prefix variables preserves the number of models.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.sharpThreeSat_sharpP_parsimoniousHard :

SharpP.ParsimoniousHard SharpThreeSAT

#3SAT is parsimoniously #P-hard.

Dependency graph

theorem DescriptiveComplexity.sharpThreeSat_sharpP_parsimoniousComplete :

SharpP.ParsimoniousComplete SharpThreeSAT

#3SAT is parsimoniously #P-complete. Registered in the Lax archive as Lax280166.ThreeSATComplete.sharpThreeSat_sharpP_parsimoniousComplete.

Dependency graph

theorem DescriptiveComplexity.sharpThreeSat_sharpP_complete :

SharpP.Complete SharpThreeSAT

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

Dependency graph