Clause sets, subcubes, isolation and the PPZ decoder -- definitions

A clause set over N variables is a finite set of clauses, each a finite set of literals (ClauseSet N). It is the set-based form of Complexity.CNF, used by the satisfiability-coding lemma of Paturi, Pudlák and Zane and by the sparsification lemma of Impagliazzo, Paturi and Zane. CNF.toClauseSet converts a CNF, preserving its semantics (CNF.eval) and not increasing its width.

Main definitions

• ClauseSet.Sat, ClauseSet.solutions: satisfaction and the solution set.
• ClauseSet.toCNF, CNF.occurrences: a CNF listing the clauses of a clause set, and the number of clauses of a CNF that mention a variable.
• ClauseSet.occurrences, ClauseSet.neighbors: the number of clauses mentioning a variable, and the neighbours of a variable in the co-occurrence graph (two distinct variables are adjacent when some clause mentions both).
• BitString.flipOn x T: the point x ⊕ e_T, flipping the coordinates in T.
• ContainsSubcube S d: S contains a subcube {a ⊕ e_T : T ⊆ J} with |J| = d.
• isolatedDirections S x: the directions i with x ⊕ e_i ∉ S.
• ClauseSet.forced ψ σ x: for an order σ of the variables (a permutation: variable v is placed at position σ v), the variables at which the first rule of the PPZ decoder fires on input x: some clause has a literal on v, and all its other literals are on variables placed before v and are false under x.
• ClauseSet.decode ψ σ y: the PPZ decoder. It processes the variables in the order σ; at v, if the first rule fires on the values already decoded, it sets v to satisfy a forcing literal, and otherwise it copies y v.

def Complexity.Literal.equivProd {N : ℕ} : Literal N ≃ Fin N × Bool

Literals over N variables are pairs of a variable and a polarity.

Equations

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

@[instance_reducible]

instance Complexity.instFintypeLiteral {N : ℕ} : Fintype (Literal N)

Equations

• Complexity.instFintypeLiteral = Fintype.ofEquiv (Fin N × Bool) Complexity.Literal.equivProd.symm

theorem Complexity.Literal.card_literal {N : ℕ} : Fintype.card (Literal N) = 2 * N

There are 2 N literals over N variables.

@[reducible, inline]

abbrev Complexity.ClauseSet (N : ℕ) : Type

A clause set over N variables: a finite set of clauses, each a finite set of literals. A clause is satisfied when one of its literals is true; a clause set when all its clauses are.

Equations

• Complexity.ClauseSet N = Finset (Finset (Complexity.Literal N))

def Complexity.ClauseSet.Sat {N : ℕ} (ψ : ClauseSet N) (x : BitString N) : Prop

x satisfies every clause of ψ.

Equations

• ψ.Sat x = ∀ C ∈ ψ, ∃ l ∈ C, l.eval x = true

@[instance_reducible]

instance Complexity.ClauseSet.instDecidablePredBitStringSat {N : ℕ} (ψ : ClauseSet N) : DecidablePred ψ.Sat

Equations

• ψ.instDecidablePredBitStringSat x✝ = id inferInstance

def Complexity.ClauseSet.solutions {N : ℕ} (ψ : ClauseSet N) : Finset (BitString N)

The solution set of a clause set.

Equations

• ψ.solutions = Finset.filter ψ.Sat Finset.univ

def Complexity.ClauseSet.occurrences {N : ℕ} (ψ : ClauseSet N) (v : Fin N) : ℕ

The number of clauses of ψ that mention the variable v.

Equations

• ψ.occurrences v = {C ∈ ψ | ∃ l ∈ C, l.var = v}.card

def Complexity.ClauseSet.neighbors {N : ℕ} (ψ : ClauseSet N) (u : Fin N) : Finset (Fin N)

The neighbours of u in the co-occurrence graph of ψ: the variables w ≠ u such that some clause of ψ mentions both u and w.

Equations

• ψ.neighbors u = {w : Fin N | w ≠ u ∧ ∃ C ∈ ψ, (∃ l ∈ C, l.var = u) ∧ ∃ l ∈ C, l.var = w}

def Complexity.CNF.toClauseSet {N : ℕ} (φ : CNF N) : ClauseSet N

The clause set of a CNF: each clause becomes the set of its literals.

Equations

• φ.toClauseSet = (List.map List.toFinset φ.clauses).toFinset

noncomputable def Complexity.ClauseSet.toCNF {N : ℕ} (ψ : ClauseSet N) : CNF N

A CNF with the clauses of a clause set, listed in some order.

Equations

• ψ.toCNF = { clauses := List.map Finset.toList (Finset.toList ψ) }

def Complexity.CNF.occurrences {N : ℕ} (φ : CNF N) (v : Fin N) : ℕ

The number of clauses of a CNF (counted with multiplicity) that mention the variable v.

Equations

• φ.occurrences v = List.countP (fun (clause : List (Complexity.Literal N)) => decide (∃ l ∈ clause, l.var = v)) φ.clauses

def Complexity.BitString.flipOn {N : ℕ} (x : BitString N) (T : Finset (Fin N)) : BitString N

x ⊕ e_T: flip the coordinates of x in T.

Equations

• x.flipOn T i = if i ∈ T then !x i else x i

def Complexity.ContainsSubcube {N : ℕ} (S : Set (BitString N)) (d : ℕ) : Prop

S contains a subcube of dimension d: some base point a and some set J of d coordinates have a ⊕ e_T ∈ S for every T ⊆ J.

Equations

• Complexity.ContainsSubcube S d = ∃ (a : Complexity.BitString N) (J : Finset (Fin N)), J.card = d ∧ ∀ T ⊆ J, a.flipOn T ∈ S

def Complexity.isolatedDirections {N : ℕ} (S : Finset (BitString N)) (x : BitString N) : Finset (Fin N)

The isolated directions of x in S: the coordinates i with x ⊕ e_i ∉ S.

Equations

• Complexity.isolatedDirections S x = {i : Fin N | x.flipOn {i} ∉ S}

def Complexity.ClauseSet.forced {N : ℕ} (ψ : ClauseSet N) (σ : Equiv.Perm (Fin N)) (x : BitString N) : Finset (Fin N)

The variables forced on input x for the order σ: those at which the first rule of the decoder fires when the earlier variables carry the values of x.

Equations

• ψ.forced σ x = {v : Fin N | ∃ C ∈ ψ, ∃ l ∈ C, l.var = v ∧ ∀ l' ∈ C, l' ≠ l → σ l'.var < σ v ∧ l'.eval x = false}

def Complexity.ClauseSet.decodeValue {N : ℕ} (ψ : ClauseSet N) (σ : Equiv.Perm (Fin N)) (z : BitString N) (v : Fin N) (b : Bool) : Bool

The value the decoder gives to v on the partial assignment z with default bit b: the polarity of a forcing literal if the first rule fires (true if some forcing literal is positive), and b otherwise.

Equations

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

def Complexity.ClauseSet.decodeUpTo {N : ℕ} (ψ : ClauseSet N) (σ : Equiv.Perm (Fin N)) (y : BitString N) : ℕ → BitString N

The decoder after processing the first p positions of σ: positions < p carry decoded values and the others still carry the input y.

Equations

• One or more equations did not get rendered due to their size.
• ψ.decodeUpTo σ y 0 = y

def Complexity.ClauseSet.decode {N : ℕ} (ψ : ClauseSet N) (σ : Equiv.Perm (Fin N)) (y : BitString N) : BitString N

The PPZ decoder for the order σ, run on the input y.

Equations

• ψ.decode σ y = ψ.decodeUpTo σ y N