Documentation

DescriptiveComplexity.Problems.Game.Hardness

HORN-SAT to GAME: unit propagation is a game #

The hardness half of DescriptiveComplexity.GAME. The AND/OR graph drawn inside a Language.sat-instance is unit propagation read as a game:

a variable x is an existential node – to win at it, name a clause that forces it;
a clause c is a universal node – the opponent challenges one of its negative literals, and the game continues there;
a clause with no negative literal wins outright, which is what the won mark of FirstOrder.Language.andOrGraph is for and why a stuck universal node had to lose (DescriptiveComplexity.Problems.Game.Defs);
the goal clauses – those with no positive literal – are the marked starts.

So the existential player wins exactly when some goal clause has all its negative literals forced, which on a Horn formula is exactly unsatisfiability (DescriptiveComplexity.exists_goalClause in one direction, DescriptiveComplexity.forced_subset_model in the other).

Reducing from the complement #

The game computes a least fixed point, so what it decides is Horn unsatisfiability; a game deciding satisfiability would have to negate the propagation. That costs nothing, since polynomial time is closed under complement (DescriptiveComplexity.piP_zero_eq), and the last step is the same one DescriptiveComplexity.Problems.Cvp.Hardness takes.

The non-Horn escape #

DescriptiveComplexity.HORNSAT folds the promise “at most one positive literal per clause” into its yes-instances, so its complement holds outright on an instance that is not Horn. The interpretation therefore marks every node both start and won when the instance fails the promise (DescriptiveComplexity.GameHard.nonHornG, a sentence, hence available to every defining formula), which makes such an instance a yes-instance of GAME with no propagation at all.

@[reducible, inline]

abbrev DescriptiveComplexity.GameHard.satOrd :

FirstOrder.Language

The ordered expansion of the vocabulary of CNF formulas.

Equations

DescriptiveComplexity.GameHard.satOrd = FirstOrder.Language.sat.sum FirstOrder.Language.order

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.GameHard.satIsClauseO :

satOrd.Relations 1

The clause symbol in the ordered expansion.

Equations

DescriptiveComplexity.GameHard.satIsClauseO = Sum.inl FirstOrder.Language.satIsClause

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.GameHard.satPosInO :

satOrd.Relations 2

The positive-occurrence symbol in the ordered expansion.

Equations

DescriptiveComplexity.GameHard.satPosInO = Sum.inl FirstOrder.Language.satPosIn

Instances For

Dependency graph

@[reducible, inline]

abbrev DescriptiveComplexity.GameHard.satNegInO :

satOrd.Relations 2

The negative-occurrence symbol in the ordered expansion.

Equations

DescriptiveComplexity.GameHard.satNegInO = Sum.inl FirstOrder.Language.satNegIn

Instances For

Dependency graph

inductive DescriptiveComplexity.GameHard.GTag :

The two sorts of node the interpretation draws.

var : GTag
A propositional variable.
cl : GTag
A clause.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.GameHard.instDecidableEqGTag :

DecidableEq GTag

Equations

DescriptiveComplexity.GameHard.instDecidableEqGTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.GameHard.instFintypeGTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.GameHard.instNonemptyGTag :

Dependency graph

The guards #

noncomputable def DescriptiveComplexity.GameHard.isClauseG {γ : Type} (x : γ) :

satOrd.Formula γ

x is a clause, as a guard.

Equations

DescriptiveComplexity.GameHard.isClauseG x = DescriptiveComplexity.GameHard.satIsClauseO.formula₁ (FirstOrder.Language.var x)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.GameHard.posInG {γ : Type} (c x : γ) :

satOrd.Formula γ

x occurs positively in the clause c, as a guard.

Equations

DescriptiveComplexity.GameHard.posInG c x = DescriptiveComplexity.GameHard.satPosInO.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.GameHard.negInG {γ : Type} (c x : γ) :

satOrd.Formula γ

x occurs negatively in the clause c, as a guard.

Equations

DescriptiveComplexity.GameHard.negInG c x = DescriptiveComplexity.GameHard.satNegInO.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.GameHard.nonHornG {γ : Type} :

satOrd.Formula γ

The instance is not Horn: some clause has two distinct positive literals. A sentence, so every defining formula may use it.

Equations

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

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.realize_isClauseG {γ A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : γ → A} (x : γ) :

(isClauseG x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![v x]

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.realize_posInG {γ A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : γ → A} (c x : γ) :

(posInG c x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![v c, v x]

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.realize_negInG {γ A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : γ → A} (c x : γ) :

(negInG c x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![v c, v x]

Dependency graph

theorem DescriptiveComplexity.GameHard.realize_nonHornG {γ A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : γ → A} :

nonHornG.Realize v ↔ ¬AtMostOnePositive A

Dependency graph

The interpretation #

noncomputable def DescriptiveComplexity.GameHard.gameInterp :

FOInterpretation satOrd FirstOrder.Language.andOrGraph GTag 1

The AND/OR graph of unit propagation: variables are existential nodes, clauses universal ones, a clause with no negative literal wins outright, and the goal clauses are the marked starts.

Equations

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

Instances For

Dependency graph

The points #

def DescriptiveComplexity.GameHard.varPt {A : Type} (x : A) :

gameInterp.Map A

The node of a propositional variable.

Equations

DescriptiveComplexity.GameHard.varPt x = (DescriptiveComplexity.GameHard.GTag.var , fun (x_1 : Fin 1) => x)

Instances For

Dependency graph

def DescriptiveComplexity.GameHard.clPt {A : Type} (c : A) :

gameInterp.Map A

The node of a clause.

Equations

DescriptiveComplexity.GameHard.clPt c = (DescriptiveComplexity.GameHard.GTag.cl , fun (x : Fin 1) => c)

Instances For

Dependency graph

theorem DescriptiveComplexity.GameHard.pt_cases {A : Type} (p : gameInterp.Map A) :

(∃ (x : A), p = varPt x) ∨ ∃ (c : A), p = clPt c

Every node is a variable node or a clause node.

Dependency graph

Reading the drawn graph #

@[simp]

theorem DescriptiveComplexity.GameHard.move_var_cl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c : A) :

AGMove (varPt x) (clPt c) ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.move_cl_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c y : A) :

AGMove (clPt c) (varPt y) ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y]

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.move_var_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x y : A) :

¬AGMove (varPt x) (varPt y)

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.move_cl_cl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c c' : A) :

¬AGMove (clPt c) (clPt c')

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.univ_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x : A) :

¬AGUniv (varPt x)

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.univ_cl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) :

AGUniv (clPt c)

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.won_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x : A) :

AGWon (varPt x) ↔ ¬AtMostOnePositive A

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.won_cl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) :

AGWon (clPt c) ↔ (FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ ∀ (y : A), ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y]) ∨ ¬AtMostOnePositive A

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.start_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x : A) :

AGStart (varPt x) ↔ ¬AtMostOnePositive A

Dependency graph

@[simp]

theorem DescriptiveComplexity.GameHard.start_cl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) :

AGStart (clPt c) ↔ (FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ ∀ (x : A), ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]) ∨ ¬AtMostOnePositive A

Dependency graph

Winning is being forced #

def DescriptiveComplexity.GameHard.Good {A : Type} [FirstOrder.Language.sat.Structure A] (p : gameInterp.Map A) :

What winning says at each of the two sorts of node.

Equations

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

Instances For

Dependency graph

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

Good (varPt x) ↔ Forced x

Dependency graph

theorem DescriptiveComplexity.GameHard.good_clPt {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) :

Good (clPt c) ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ ∀ (y : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y] → Forced y

Dependency graph

theorem DescriptiveComplexity.GameHard.good_of_winsOn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hhorn : AtMostOnePositive A) {p : gameInterp.Map A} (h : WinsOn (gameInterp.Map A) p) :

Soundness: a winning node is forced, and a winning clause node has all its negative literals forced.

Dependency graph

theorem DescriptiveComplexity.GameHard.winsOn_clPt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} (hc : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]) (hall : ∀ (y : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y] → WinsOn (gameInterp.Map A) (varPt y)) :

WinsOn (gameInterp.Map A) (clPt c)

A clause node with all its negative literals winning is winning: the opponent's every challenge is answered, and a clause with nothing to challenge wins outright.

Dependency graph

theorem DescriptiveComplexity.GameHard.winsOn_of_forcedIn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (n : ℕ) (x : A) :

ForcedIn n x → WinsOn (gameInterp.Map A) (varPt x)

Completeness: a forced variable wins.

Dependency graph

theorem DescriptiveComplexity.GameHard.winsOn_of_forced {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x : A} (h : Forced x) :

WinsOn (gameInterp.Map A) (varPt x)

Dependency graph

The game is won exactly on the no-instances #

theorem DescriptiveComplexity.GameHard.gameWon_iff_goalClause {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hhorn : AtMostOnePositive A) :

GameWon (gameInterp.Map A) ↔ ∃ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ (∀ (x : A), ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]) ∧ ∀ (y : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y] → Forced y

On a Horn instance, the game is won exactly when some goal clause has all its negative literals forced.

Dependency graph

theorem DescriptiveComplexity.GameHard.gameWon_iff_not_hornSatisfiable {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

¬HornSatisfiable A ↔ GameWon (gameInterp.Map A)

The reduction is correct: the game is won exactly on the instances that are not yes-instances of HORN-SAT.

Dependency graph

noncomputable def DescriptiveComplexity.hornSatCompl_ordered_fo_reduction_game :

OrderedFOReduction HORNSAT ᶜ GAME

The complement of HORN-SAT reduces to GAME: unit propagation, read as a game.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.game_PTIME_hard :

PTIME.Hard GAME

GAME is PTIME-hard: every SO-Horn definable problem reduces to it. The route is the Horn discharge applied to the complement of the problem, complemented back – which is available because polynomial time is closed under complement.

Dependency graph

theorem DescriptiveComplexity.game_PTIME_complete :

PTIME.Complete GAME

GAME is PTIME-complete. Membership is DescriptiveComplexity.game_mem_PTIME, the least fixed point with its scan of the order; hardness is unit propagation read as a game.

Dependency graph