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 (Cslib.Complexity.TQBF), which is proved PSPACE-complete in Complexity.Computability.Complexity.Classes.Space.TQBF (Cslib.Complexity.TQBF_pspaceComplete) Arora and Barak, Section 4.2.

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. QBF V instantiates cslib's logical operator typeclasses (Top, Bot, Cslib.Logic.HasNot, Cslib.Logic.HasAnd, Cslib.Logic.HasOr, Cslib.Logic.HasImp, Cslib.Logic.HasIff), so that ⊤, ⊥, ¬, ∧, ∨, →, ↔, and ⋀ are available on QBF V when Cslib.Logic is open.

Main definitions

• Cslib.Logic.PL.QBF: the formulas, with Top, Bot, HasNot, HasAnd, HasOr, HasImp, and HasIff instances.
• 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 (QBF.conj_eq_finiteAnd).
• 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

Evaluating a variable var v under σ yields σ v.

@[simp]

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

The constant top evaluates to true.

@[simp]

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

The constant bot evaluates to false.

@[simp]

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

Evaluating φ.not negates the truth value of φ.

@[simp]

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

Evaluating φ.and ψ takes the Boolean conjunction of φ.eval σ and ψ.eval σ.

@[simp]

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

Evaluating φ.or ψ takes the Boolean disjunction of φ.eval σ and ψ.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) φ)

Evaluating ex v φ takes the disjunction of φ with v set to false and to 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) φ)

Evaluating all v φ takes the conjunction of φ with v set to false and to 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}

The free variables of var v are {v}.

@[simp]

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

The constant top has no free variables.

@[simp]

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

The constant bot has no free variables.

@[simp]

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

Negation preserves the set of free variables.

@[simp]

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

The free variables of φ.and ψ are the union of those of φ and ψ.

@[simp]

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

The free variables of φ.or ψ are the union of those of φ and ψ.

@[simp]

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

Existential quantification over v removes v from the free variables of φ.

@[simp]

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

Universal quantification over v removes v from the free variables of φ.

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

Every formula has size at least 1.

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

The number of variable occurrences in φ is at most φ.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

Being closed is decidable when variable equality is decidable.

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

A negated formula φ.not is closed if and only if φ is closed.

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

A conjunction φ.and ψ is closed if and only if both φ and ψ are closed.

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

A disjunction φ.or ψ is closed if and only if both φ and ψ are 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.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instTop {V : Type u_1} : Top (QBF V)

⊤ on QBF V is QBF.top.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instBot {V : Type u_1} : Bot (QBF V)

⊥ on QBF V is QBF.bot.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instHasNot {V : Type u_1} : HasNot (QBF V)

¬ on QBF V is QBF.not.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instHasAnd {V : Type u_1} : HasAnd (QBF V)

∧ on QBF V is QBF.and.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instHasOr {V : Type u_1} : HasOr (QBF V)

∨ on QBF V is QBF.or.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instHasImp {V : Type u_1} : HasImp (QBF V)

→ on QBF V is QBF.imp.

@[instance_reducible]

instance Cslib.Logic.PL.QBF.instHasIff {V : Type u_1} : HasIff (QBF V)

↔ on QBF V is QBF.iff.

theorem Cslib.Logic.PL.QBF.conj_eq_finiteAnd {V : Type u_1} (φs : List (QBF V)) : conj φs = finiteAnd φs

QBF.conj agrees with Cslib.Logic.finiteAnd (⋀).

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 φ)

Existential quantification over vs ++ ws is existential quantification over vs followed by 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 φ)

Universal quantification over vs ++ ws is universal quantification over vs followed by 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

The conjunction of a list l evaluates to true iff every formula in l evaluates to true.

@[simp]

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

Evaluating imp φ ψ computes Boolean implication !φ.eval σ || ψ.eval σ.

@[simp]

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

Evaluating iff φ ψ computes Boolean equivalence φ.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)

A literal lit v b evaluates to true iff σ v equals 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

Embedding a clause via ofClause preserves its truth value under σ.

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

Quantifying existentially over vs removes vs.toFinset from the free variables of φ.

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

Quantifying universally over vs removes vs.toFinset from the free variables of φ.

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

A variable is free in conj l if and only if it is free in some formula of l.

@[simp]

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

The free variables of imp φ ψ are the union of those of φ and ψ.

@[simp]

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

The free variables of iff φ ψ are the union of those of φ and ψ.

@[simp]

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

The only free variable of lit v b is v.

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

The free variables of ofCNF φ are the variables occurring in φ.