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

@[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

@[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

@[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

inductive DescriptiveComplexity.GameHard.GTag : Type

The two sorts of node the interpretation draws.

• var : GTag

  A propositional variable.

• cl : GTag

  A clause.

@[instance_reducible]

instance DescriptiveComplexity.GameHard.instDecidableEqGTag : DecidableEq GTag

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.GameHard.instFintypeGTag : Fintype GTag

Equations

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

instance DescriptiveComplexity.GameHard.instNonemptyGTag : Nonempty GTag

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)

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)

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)

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.

@[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]

@[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]

@[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]

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.

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)

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)

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]

@[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]

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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

@[simp]

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

@[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

Winning is being forced

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

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

Equations

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

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

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

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)

The game is won exactly on the no-instances

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.

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. Registered in the Lax archive as Lax535992.GamePTIMEComplete.game_PTIME_complete.