The number written by unit propagation: definition

The function counterpart of HORN-SAT (DescriptiveComplexity.HORNSAT): some variables of a Horn formula are marked as outputs and compared by significance, and the problem is to compute the number whose binary digits say which of them unit propagation forces to be true (DescriptiveComplexity.Forced), i.e., which are true in the least model.

• The vocabulary is the one of CNF instances (FirstOrder.Language.sat) with two more symbols (FirstOrder.Language.digitOrder): out marks the output variables and below compares them.
• DescriptiveComplexity.hornNumber: a forced output variable contributes 2 ^ r, where r is the number of output variables strictly below it, when below linearly orders the output variables (DescriptiveComplexity.VarOrder). An instance that is not a satisfiable Horn formula, or whose below is not such an order, writes 0.

This is the problem through which the number written by a machine (DescriptiveComplexity.DTMNumber) is shown hard for FP: the least fixed point of a system of rules is the least model of a Horn formula, and the unit-propagation machine leaves that model on its tape.

def FirstOrder.Language.digitOrder : Language

The symbols reading a number off a set of marked elements.

Equations

• FirstOrder.Language.digitOrder = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.digitOrderRel }

@[reducible, inline]

abbrev FirstOrder.Language.dgoBelow : Language.digitOrder.Relations 2

below y x: the digit of y is at most as significant as the one of x.

Equations

• FirstOrder.Language.dgoBelow = FirstOrder.Language.digitOrderRel.below

inductive FirstOrder.Language.digitOrderRel : ℕ → Type

The relation symbols of the language.

• out : digitOrderRel 1

  out x: the element x holds one digit.

• below : digitOrderRel 2

  below y x: the digit of y is at most as significant as the one of x.

instance FirstOrder.Language.instIsRelationalDigitOrder : Language.digitOrder.IsRelational

def FirstOrder.Language.instDecidableEqDigitOrderRel.decEq {a✝ : ℕ} (x✝ x✝¹ : digitOrderRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqDigitOrderRel {a✝ : ℕ} : DecidableEq (digitOrderRel a✝)

Equations

• FirstOrder.Language.instDecidableEqDigitOrderRel = FirstOrder.Language.instDecidableEqDigitOrderRel.decEq

@[reducible, inline]

abbrev FirstOrder.Language.dgoOut : Language.digitOrder.Relations 1

out x: the element x holds one digit.

Equations

• FirstOrder.Language.dgoOut = FirstOrder.Language.digitOrderRel.out

@[reducible, inline]

abbrev FirstOrder.Language.satOut : Language

The relational language of Horn formulas writing a number.

Equations

• FirstOrder.Language.satOut = FirstOrder.Language.sat.sum FirstOrder.Language.digitOrder

@[reducible, inline]

abbrev DescriptiveComplexity.hnOut : FirstOrder.Language.satOut.Relations 1

“Is an output variable”.

Equations

• DescriptiveComplexity.hnOut = Sum.inr FirstOrder.Language.dgoOut

@[reducible, inline]

abbrev DescriptiveComplexity.hnBelow : FirstOrder.Language.satOut.Relations 2

The comparison of the output variables.

Equations

• DescriptiveComplexity.hnBelow = Sum.inr FirstOrder.Language.dgoBelow

@[instance_reducible]

instance DescriptiveComplexity.satOutStructure (A : Type) [FirstOrder.Language.satOut.Structure A] : FirstOrder.Language.sat.Structure A

A Horn formula writing a number is a CNF instance.

Equations

• DescriptiveComplexity.satOutStructure A = FirstOrder.Language.LHom.sumInl.reduct A

The propagation closure is isomorphism-invariant

The number

def DescriptiveComplexity.ForcedDigit {A : Type} [FirstOrder.Language.satOut.Structure A] (x : A) : Prop

The output variable x is forced.

Equations

• DescriptiveComplexity.ForcedDigit x = (FirstOrder.Language.Structure.RelMap DescriptiveComplexity.hnOut ![x] ∧ DescriptiveComplexity.Forced x)

def DescriptiveComplexity.LowerVar {A : Type} [FirstOrder.Language.satOut.Structure A] (x y : A) : Prop

y is an output variable strictly below x.

Equations

• DescriptiveComplexity.LowerVar x y = (FirstOrder.Language.Structure.RelMap DescriptiveComplexity.hnOut ![y] ∧ y ≠ x ∧ FirstOrder.Language.Structure.RelMap DescriptiveComplexity.hnBelow ![y, x])

noncomputable def DescriptiveComplexity.varRank {A : Type} [FirstOrder.Language.satOut.Structure A] (x : A) : ℕ

The rank of a variable among the outputs: the number of output variables strictly below it.

Equations

• DescriptiveComplexity.varRank x = Nat.card { y : A // DescriptiveComplexity.LowerVar x y }

def DescriptiveComplexity.VarOrder (A : Type) [FirstOrder.Language.satOut.Structure A] : Prop

The comparison of the outputs is a linear order on them: reflexive, transitive, antisymmetric and total among the output variables.

Equations

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

noncomputable def DescriptiveComplexity.hornNumber (A : Type) [FirstOrder.Language.satOut.Structure A] : ℕ

The number written by unit propagation: each forced output variable contributes two to the power of its rank among the outputs. Instances that are not satisfiable Horn formulas, or whose outputs are not linearly ordered, write 0.

Equations

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

theorem DescriptiveComplexity.hornNumber_iso {A B : Type} [FirstOrder.Language.satOut.Structure A] [FirstOrder.Language.satOut.Structure B] (e : FirstOrder.Language.satOut.Equiv A B) : hornNumber A = hornNumber B

The number written is isomorphism-invariant.

noncomputable def DescriptiveComplexity.HornNumber : CountingProblem FirstOrder.Language.satOut

The number written by unit propagation, as a counting problem on Language.satOut-structures: the function counterpart of DescriptiveComplexity.HORNSAT.

Equations

• DescriptiveComplexity.HornNumber = { Count := fun (A : Type) (inst : FirstOrder.Language.satOut.Structure A) => DescriptiveComplexity.hornNumber A, iso_invariant := ⋯ }