3SAT and decoupled 5SAT formulas

Literals, clauses and satisfaction, for the succinct Cook–Levin theorem (planning/succinct-cook-levin.md). A 3SAT formula is a set of clauses, each of exactly three literals (a clause of fewer literals repeats one: x ∨ x ∨ x), and a decoupled 5SAT formula (answer_reduction.tex, "Decoupled 5SAT and its succinct descriptions") is a set of clauses with one literal from each of five blocks of variables, evaluated on five separate assignments. The literal x^o of the paper is ⟨x, o⟩: positive when o = true.

structure MIPRE.SAT.Lit (V : Type u_1) : Type u_1

A literal: a variable and its sign (pos = true for x, false for ¬x).

• var : V
• pos : Bool

def MIPRE.SAT.instDecidableEqLit.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : Lit V✝) : Decidable (x✝ = x✝¹)

Equations

• MIPRE.SAT.instDecidableEqLit.decEq { var := a, pos := a_1 } { var := b, pos := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance MIPRE.SAT.instDecidableEqLit {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (Lit V✝)

Equations

• MIPRE.SAT.instDecidableEqLit = MIPRE.SAT.instDecidableEqLit.decEq

def MIPRE.SAT.Lit.eval {V : Type u_1} (w : V → Bool) (l : Lit V) : Bool

The value of a literal under an assignment.

Equations

• MIPRE.SAT.Lit.eval w l = if l.pos = true then w l.var else !w l.var

structure MIPRE.SAT.Clause3 (V : Type u_1) : Type u_1

A 3SAT clause.

• l₁ : Lit V
• l₂ : Lit V
• l₃ : Lit V

@[instance_reducible]

instance MIPRE.SAT.instDecidableEqClause3 {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (Clause3 V✝)

Equations

• MIPRE.SAT.instDecidableEqClause3 = MIPRE.SAT.instDecidableEqClause3.decEq

def MIPRE.SAT.instDecidableEqClause3.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : Clause3 V✝) : Decidable (x✝ = x✝¹)

Equations

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

def MIPRE.SAT.Clause3.eval {V : Type u_1} (w : V → Bool) (c : Clause3 V) : Bool

The value of a clause.

Equations

• MIPRE.SAT.Clause3.eval w c = (MIPRE.SAT.Lit.eval w c.l₁ || MIPRE.SAT.Lit.eval w c.l₂ || MIPRE.SAT.Lit.eval w c.l₃)

@[reducible, inline]

abbrev MIPRE.SAT.Cnf3 (V : Type u_1) : Type u_1

A 3SAT formula on the variables V: a set of clauses.

Equations

• MIPRE.SAT.Cnf3 V = Set (MIPRE.SAT.Clause3 V)

def MIPRE.SAT.Cnf3.Sat {V : Type u_1} (φ : Cnf3 V) (w : V → Bool) : Prop

w satisfies every clause of φ.

Equations

• φ.Sat w = ∀ c ∈ φ, MIPRE.SAT.Clause3.eval w c = true

structure MIPRE.SAT.Clause5 (V₁ : Type u_1) (V₂ : Type u_2) (V₃ : Type u_3) (V₄ : Type u_4) (V₅ : Type u_5) : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

A decoupled 5SAT clause: one literal from each of five blocks.

• l₁ : Lit V₁
• l₂ : Lit V₂
• l₃ : Lit V₃
• l₄ : Lit V₄
• l₅ : Lit V₅

def MIPRE.SAT.Clause5.eval {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} {V₅ : Type u_5} (w₁ : V₁ → Bool) (w₂ : V₂ → Bool) (w₃ : V₃ → Bool) (w₄ : V₄ → Bool) (w₅ : V₅ → Bool) (c : Clause5 V₁ V₂ V₃ V₄ V₅) : Bool

The value of a decoupled clause on five assignments.

Equations

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

@[reducible, inline]

abbrev MIPRE.SAT.Cnf5 (V₁ : Type u_1) (V₂ : Type u_2) (V₃ : Type u_3) (V₄ : Type u_4) (V₅ : Type u_5) : Type (max (max (max (max u_5 u_4) u_3) u_2) u_1)

A decoupled 5SAT formula.

Equations

• MIPRE.SAT.Cnf5 V₁ V₂ V₃ V₄ V₅ = Set (MIPRE.SAT.Clause5 V₁ V₂ V₃ V₄ V₅)

def MIPRE.SAT.Cnf5.Sat {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} {V₅ : Type u_5} (φ : Cnf5 V₁ V₂ V₃ V₄ V₅) (w₁ : V₁ → Bool) (w₂ : V₂ → Bool) (w₃ : V₃ → Bool) (w₄ : V₄ → Bool) (w₅ : V₅ → Bool) : Prop

The five assignments satisfy every clause of φ.

Equations

• φ.Sat w₁ w₂ w₃ w₄ w₅ = ∀ c ∈ φ, MIPRE.SAT.Clause5.eval w₁ w₂ w₃ w₄ w₅ c = true