Quantified Boolean formulas

Quantified Boolean formulas over an arbitrary type V of variables: variables, the two constants, negation, conjunction, disjunction, and quantifiers ∃ v and ∀ v over the truth value of a variable Stockmeyer and Meyer. QBF.eval σ φ is the truth value of φ under the assignment σ; a quantifier over v evaluates its body with v set to each of the two truth values (Function.update).

The value of a formula depends only on its free variables (QBF.eval_congr), so a closed formula, one without free variables, has the same value under every assignment (QBF.eval_eq_of_closed). The true closed formulas form the problem TQBF, which is PSPACE-complete Arora and Barak, Section 4.2 (Cslib.Complexity.TQBF_pspaceComplete).

cslib's Cslib.Logic.PL.Proposition has no quantifiers and is a syntax for proof systems rather than an evaluated one, so it is not reused.

Main definitions

• Cslib.Logic.PL.QBF: the formulas.
• Cslib.Logic.PL.QBF.eval: the value of a formula under an assignment.
• Cslib.Logic.PL.QBF.freeVars, Cslib.Logic.PL.QBF.Closed.
• Cslib.Logic.PL.QBF.vars, Cslib.Logic.PL.QBF.size: the variables, free or bound, and the number of nodes.
• Cslib.Logic.PL.QBF.exs, Cslib.Logic.PL.QBF.alls, Cslib.Logic.PL.QBF.conj, Cslib.Logic.PL.QBF.imp, Cslib.Logic.PL.QBF.iff, Cslib.Logic.PL.QBF.lit: derived connectives, blocks of quantifiers and conjunctions of lists.
• Cslib.Logic.PL.QBF.ofClause, Cslib.Logic.PL.QBF.ofCNF: clauses and formulas in conjunctive normal form as quantified Boolean formulas.

Main results

• Cslib.Logic.PL.QBF.eval_ex_eq_true_iff, Cslib.Logic.PL.QBF.eval_all_eq_true_iff: the quantifiers as ∃ and ∀ over a truth value.
• Cslib.Logic.PL.QBF.eval_congr: the value depends only on the free variables.
• Cslib.Logic.PL.QBF.eval_eq_of_closed: a closed formula has the same value under every assignment.
• Cslib.Logic.PL.QBF.eval_not_ex, Cslib.Logic.PL.QBF.eval_not_all: De Morgan's laws for the quantifiers.
• Cslib.Logic.PL.QBF.eval_exs_eq_true_iff, Cslib.Logic.PL.QBF.eval_alls_eq_true_iff: blocks of quantifiers range over the assignments that agree outside the block.
• Cslib.Logic.PL.QBF.eval_ofCNF, Cslib.Logic.PL.QBF.mem_freeVars_ofCNF: formulas in conjunctive normal form keep their value and their variables.

References

• L. Stockmeyer, A. Meyer, Word problems requiring exponential time
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

inductive Cslib.Logic.PL.QBF (V : Type u_1) : Type u_1

Quantified Boolean formulas over variables of type V.

• var {V : Type u_1} (v : V) : QBF V

  The variable v.

• top {V : Type u_1} : QBF V

  The constant true.

• bot {V : Type u_1} : QBF V

  The constant false.

• not {V : Type u_1} (φ : QBF V) : QBF V

  Negation.

• and {V : Type u_1} (φ ψ : QBF V) : QBF V

  Conjunction.

• or {V : Type u_1} (φ ψ : QBF V) : QBF V

  Disjunction.

• ex {V : Type u_1} (v : V) (φ : QBF V) : QBF V

  Existential quantification ∃ v, φ over the truth value of v.

• all {V : Type u_1} (v : V) (φ : QBF V) : QBF V

  Universal quantification ∀ v, φ over the truth value of v.

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableEqQBF {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (QBF V✝)

def Cslib.Logic.PL.instDecidableEqQBF.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : QBF V✝) : Decidable (x✝ = x✝¹)

Evaluation

def Cslib.Logic.PL.QBF.eval {V : Type u_1} [DecidableEq V] (σ : V → Bool) : QBF V → Bool

The value of a formula under the assignment σ. A quantifier over v evaluates its body with v set to false and to true, and takes the disjunction (ex) or the conjunction (all) of the two values.

@[simp]

theorem Cslib.Logic.PL.QBF.eval_var {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) : eval σ (var v) = σ v

@[simp]

theorem Cslib.Logic.PL.QBF.eval_top {V : Type u_1} [DecidableEq V] (σ : V → Bool) : eval σ top = true

@[simp]

theorem Cslib.Logic.PL.QBF.eval_bot {V : Type u_1} [DecidableEq V] (σ : V → Bool) : eval σ bot = false

@[simp]

theorem Cslib.Logic.PL.QBF.eval_not {V : Type u_1} [DecidableEq V] (σ : V → Bool) (φ : QBF V) : eval σ φ.not = !eval σ φ

@[simp]

theorem Cslib.Logic.PL.QBF.eval_and {V : Type u_1} [DecidableEq V] (σ : V → Bool) (φ ψ : QBF V) : eval σ (φ.and ψ) = (eval σ φ && eval σ ψ)

@[simp]

theorem Cslib.Logic.PL.QBF.eval_or {V : Type u_1} [DecidableEq V] (σ : V → Bool) (φ ψ : QBF V) : eval σ (φ.or ψ) = (eval σ φ || eval σ ψ)

@[simp]

theorem Cslib.Logic.PL.QBF.eval_ex {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (φ : QBF V) : eval σ (ex v φ) = (eval (Function.update σ v false) φ || eval (Function.update σ v true) φ)

@[simp]

theorem Cslib.Logic.PL.QBF.eval_all {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (φ : QBF V) : eval σ (all v φ) = (eval (Function.update σ v false) φ && eval (Function.update σ v true) φ)

theorem Cslib.Logic.PL.QBF.eval_ex_eq_true_iff {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (φ : QBF V) : eval σ (ex v φ) = true ↔ ∃ (b : Bool), eval (Function.update σ v b) φ = true

∃ v, φ is true when φ is true for some value of v.

theorem Cslib.Logic.PL.QBF.eval_all_eq_true_iff {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (φ : QBF V) : eval σ (all v φ) = true ↔ ∀ (b : Bool), eval (Function.update σ v b) φ = true

∀ v, φ is true when φ is true for every value of v.

theorem Cslib.Logic.PL.QBF.eval_not_ex {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (φ : QBF V) : eval σ (ex v φ).not = eval σ (all v φ.not)

De Morgan's law for ∃: ¬∃ v, φ and ∀ v, ¬φ have the same value.

theorem Cslib.Logic.PL.QBF.eval_not_all {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (φ : QBF V) : eval σ (all v φ).not = eval σ (ex v φ.not)

De Morgan's law for ∀: ¬∀ v, φ and ∃ v, ¬φ have the same value.

Free variables

def Cslib.Logic.PL.QBF.freeVars {V : Type u_1} [DecidableEq V] : QBF V → Finset V

The free variables of a formula: the variables with an occurrence outside the scope of every quantifier over them.

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_var {V : Type u_1} [DecidableEq V] (v : V) : (var v).freeVars = {v}

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_top {V : Type u_1} [DecidableEq V] : top.freeVars = ∅

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_bot {V : Type u_1} [DecidableEq V] : bot.freeVars = ∅

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_not {V : Type u_1} [DecidableEq V] (φ : QBF V) : φ.not.freeVars = φ.freeVars

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_and {V : Type u_1} [DecidableEq V] (φ ψ : QBF V) : (φ.and ψ).freeVars = φ.freeVars ∪ ψ.freeVars

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_or {V : Type u_1} [DecidableEq V] (φ ψ : QBF V) : (φ.or ψ).freeVars = φ.freeVars ∪ ψ.freeVars

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_ex {V : Type u_1} [DecidableEq V] (v : V) (φ : QBF V) : (ex v φ).freeVars = φ.freeVars.erase v

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_all {V : Type u_1} [DecidableEq V] (v : V) (φ : QBF V) : (all v φ).freeVars = φ.freeVars.erase v

theorem Cslib.Logic.PL.QBF.eval_congr {V : Type u_1} [DecidableEq V] {σ : V → Bool} {φ : QBF V} {τ : V → Bool} (h : ∀ w ∈ φ.freeVars, σ w = τ w) : eval σ φ = eval τ φ

Agreement on free variables. The value of a formula depends only on the values of its free variables.

theorem Cslib.Logic.PL.QBF.eval_update_of_notMem_freeVars {V : Type u_1} [DecidableEq V] {v : V} {φ : QBF V} (hv : v ∉ φ.freeVars) (σ : V → Bool) (b : Bool) : eval (Function.update σ v b) φ = eval σ φ

Updating a variable that is not free does not change the value of a formula.

theorem Cslib.Logic.PL.QBF.eval_ex_of_notMem_freeVars {V : Type u_1} [DecidableEq V] {v : V} {φ : QBF V} (hv : v ∉ φ.freeVars) (σ : V → Bool) : eval σ (ex v φ) = eval σ φ

A quantifier ∃ v over a variable that is not free in its body can be dropped.

theorem Cslib.Logic.PL.QBF.eval_all_of_notMem_freeVars {V : Type u_1} [DecidableEq V] {v : V} {φ : QBF V} (hv : v ∉ φ.freeVars) (σ : V → Bool) : eval σ (all v φ) = eval σ φ

A quantifier ∀ v over a variable that is not free in its body can be dropped.

Variables and size

def Cslib.Logic.PL.QBF.vars {V : Type u_1} : QBF V → List V

The variables of a formula, free or bound, with multiplicity, in prefix order.

def Cslib.Logic.PL.QBF.size {V : Type u_1} : QBF V → ℕ

The number of nodes of a formula.

theorem Cslib.Logic.PL.QBF.one_le_size {V : Type u_1} (φ : QBF V) : 1 ≤ φ.size

theorem Cslib.Logic.PL.QBF.length_vars_le_size {V : Type u_1} (φ : QBF V) : φ.vars.length ≤ φ.size

Closed formulas

def Cslib.Logic.PL.QBF.Closed {V : Type u_1} [DecidableEq V] (φ : QBF V) : Prop

A formula is closed when it has no free variables.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instDecidablePredClosed {V : Type u_1} [DecidableEq V] : DecidablePred Closed

theorem Cslib.Logic.PL.QBF.eval_eq_of_closed {V : Type u_1} [DecidableEq V] {φ : QBF V} (hφ : φ.Closed) (σ τ : V → Bool) : eval σ φ = eval τ φ

A closed formula has the same value under every assignment.

theorem Cslib.Logic.PL.QBF.closed_not {V : Type u_1} [DecidableEq V] {φ : QBF V} : φ.not.Closed ↔ φ.Closed

theorem Cslib.Logic.PL.QBF.closed_and {V : Type u_1} [DecidableEq V] {φ : QBF V} (ψ : QBF V) : (φ.and ψ).Closed ↔ φ.Closed ∧ ψ.Closed

theorem Cslib.Logic.PL.QBF.closed_or {V : Type u_1} [DecidableEq V] {φ : QBF V} (ψ : QBF V) : (φ.or ψ).Closed ↔ φ.Closed ∧ ψ.Closed

Derived connectives

def Cslib.Logic.PL.QBF.exs {V : Type u_1} (vs : List V) (φ : QBF V) : QBF V

Existential quantification over each variable of a list, the first one outermost.

def Cslib.Logic.PL.QBF.alls {V : Type u_1} (vs : List V) (φ : QBF V) : QBF V

Universal quantification over each variable of a list, the first one outermost.

def Cslib.Logic.PL.QBF.conj {V : Type u_1} (l : List (QBF V)) : QBF V

The conjunction of a list of formulas, top for the empty list.

def Cslib.Logic.PL.QBF.imp {V : Type u_1} (φ ψ : QBF V) : QBF V

Implication.

def Cslib.Logic.PL.QBF.iff {V : Type u_1} (φ ψ : QBF V) : QBF V

Equivalence.

def Cslib.Logic.PL.QBF.lit {V : Type u_1} (v : V) (b : Bool) : QBF V

The literal of v with sign b: v itself for true, its negation for false.

def Cslib.Logic.PL.QBF.ofClause {V : Type u_1} (c : Clause V) : QBF V

A clause as the disjunction of its literals, bot for the empty clause.

def Cslib.Logic.PL.QBF.ofCNF {V : Type u_1} (φ : CNF V) : QBF V

A formula in conjunctive normal form as the conjunction of its clauses, top for the empty formula.

theorem Cslib.Logic.PL.QBF.exs_append {V : Type u_1} (vs ws : List V) (φ : QBF V) : exs (vs ++ ws) φ = exs vs (exs ws φ)

theorem Cslib.Logic.PL.QBF.alls_append {V : Type u_1} (vs ws : List V) (φ : QBF V) : alls (vs ++ ws) φ = alls vs (alls ws φ)

theorem Cslib.Logic.PL.QBF.eval_exs_eq_true_iff {V : Type u_1} [DecidableEq V] (σ : V → Bool) (vs : List V) (φ : QBF V) : eval σ (exs vs φ) = true ↔ ∃ (τ : V → Bool), (∀ x ∉ vs, τ x = σ x) ∧ eval τ φ = true

A block of existential quantifiers ranges over the assignments that agree with the given one outside the block.

theorem Cslib.Logic.PL.QBF.eval_alls_eq_true_iff {V : Type u_1} [DecidableEq V] (σ : V → Bool) (vs : List V) (φ : QBF V) : eval σ (alls vs φ) = true ↔ ∀ (τ : V → Bool), (∀ x ∉ vs, τ x = σ x) → eval τ φ = true

A block of universal quantifiers ranges over the assignments that agree with the given one outside the block.

@[simp]

theorem Cslib.Logic.PL.QBF.eval_conj {V : Type u_1} [DecidableEq V] (σ : V → Bool) (l : List (QBF V)) : eval σ (conj l) = l.all fun (x : QBF V) => eval σ x

@[simp]

theorem Cslib.Logic.PL.QBF.eval_imp {V : Type u_1} [DecidableEq V] (σ : V → Bool) (φ ψ : QBF V) : eval σ (φ.imp ψ) = (!eval σ φ || eval σ ψ)

@[simp]

theorem Cslib.Logic.PL.QBF.eval_iff {V : Type u_1} [DecidableEq V] (σ : V → Bool) (φ ψ : QBF V) : eval σ (φ.iff ψ) = (eval σ φ == eval σ ψ)

@[simp]

theorem Cslib.Logic.PL.QBF.eval_lit {V : Type u_1} [DecidableEq V] (σ : V → Bool) (v : V) (b : Bool) : eval σ (lit v b) = (σ v == b)

@[simp]

theorem Cslib.Logic.PL.QBF.eval_ofClause {V : Type u_1} [DecidableEq V] (σ : V → Bool) (c : Clause V) : eval σ (ofClause c) = Clause.eval σ c

@[simp]

theorem Cslib.Logic.PL.QBF.eval_ofCNF {V : Type u_1} [DecidableEq V] (σ : V → Bool) (φ : CNF V) : eval σ (ofCNF φ) = CNF.eval σ φ

A formula in conjunctive normal form keeps its value.

Free variables of the derived connectives

theorem Cslib.Logic.PL.QBF.freeVars_exs {V : Type u_1} [DecidableEq V] (vs : List V) (φ : QBF V) : (exs vs φ).freeVars = φ.freeVars \ vs.toFinset

theorem Cslib.Logic.PL.QBF.freeVars_alls {V : Type u_1} [DecidableEq V] (vs : List V) (φ : QBF V) : (alls vs φ).freeVars = φ.freeVars \ vs.toFinset

theorem Cslib.Logic.PL.QBF.mem_freeVars_conj {V : Type u_1} [DecidableEq V] {l : List (QBF V)} {x : V} : x ∈ (conj l).freeVars ↔ ∃ φ ∈ l, x ∈ φ.freeVars

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_imp {V : Type u_1} [DecidableEq V] (φ ψ : QBF V) : (φ.imp ψ).freeVars = φ.freeVars ∪ ψ.freeVars

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_iff {V : Type u_1} [DecidableEq V] (φ ψ : QBF V) : (φ.iff ψ).freeVars = φ.freeVars ∪ ψ.freeVars

@[simp]

theorem Cslib.Logic.PL.QBF.freeVars_lit {V : Type u_1} [DecidableEq V] (v : V) (b : Bool) : (lit v b).freeVars = {v}

theorem Cslib.Logic.PL.QBF.mem_freeVars_ofCNF {V : Type u_1} [DecidableEq V] {x : V} {φ : CNF V} : x ∈ (ofCNF φ).freeVars ↔ x ∈ φ.vars