Quantified Boolean Formulas (QBF)

Author

Your Name

Published

February 5, 2025

Introduction

This lecture introduces Quantified Boolean Formulas (QBF), a generalization of propositional logic that incorporates quantifiers, similar to how first-order logic is a generalization of propositional logic. We will explore the syntax and semantics of QBF, and discuss the complexity of model checking and satisfiability problems. The main objectives are to understand how quantifiers affect the interpretation of formulas, to learn the difference between free and bound variables, and to analyze the algorithmic implications of this extended formalism. We will see that adding quantifiers does not increase the expressiveness of the logic, but it does allow for more succinct formulas. This succinctness comes at a cost, as the complexity of model checking and satisfiability will increase from linear time and $NP$-complete to $PSPACE$-complete, respectively.

Vocabulary, Syntax, and Semantics of QBF

Vocabulary

The vocabulary of QBF extends that of propositional logic by including:

Boolean connectives: $\land, \lor, \neg, \rightarrow, \leftrightarrow$
Boolean variables: $P, Q, R, \dots$ (We will use capital letters to denote variables)
Quantifiers: $\exists$ (existential) and $\forall$ (universal)

Syntax

The syntax of QBF is defined recursively as follows:

A Boolean variable $P$ is a QBF.
If $\phi_1$ and $\phi_2$ are QBFs, then $\neg \phi_1$, $\phi_1 \land \phi_2$, $\phi_1 \lor \phi_2$, $\phi_1 \rightarrow \phi_2$, and $\phi_1 \leftrightarrow \phi_2$ are QBFs.
If $\phi$ is a QBF and $P$ is a Boolean variable, then $\exists P \phi$ and $\forall P \phi$ are QBFs.

An example of a QBF is: \[\exists P \forall Q (P \lor \neg Q) \land (\neg R \lor \neg P)\] Here, $P$ and $Q$ are bound variables, while $R$ is a free variable.

Semantics

The semantics of QBF are defined with respect to a structure $S$, which is a function mapping Boolean variables to truth values (true or false).

An interpretation (or structure) $S$ for a QBF $\phi$ is a function that maps the free variables of $\phi$ to either true or false.

It is important to note that we only need to define the interpretation for the free variables. The bound variables will be assigned values by the quantifiers.

The semantics are defined recursively:

$S \models P$ if and only if $S(P) = \text{true}$.
$S \models \neg \phi$ if and only if $S \not\models \phi$.
$S \models \phi_1 \lor \phi_2$ if and only if $S \models \phi_1$ or $S \models \phi_2$.
$S \models \phi_1 \land \phi_2$ if and only if $S \models \phi_1$ and $S \models \phi_2$.
$S \models \exists P \phi$ if and only if there exists a structure $S'$ such that $S'[P \mapsto \text{true}] \models \phi$ or $S'[P \mapsto \text{false}] \models \phi$, where $S'[P \mapsto v]$ is the structure obtained from $S$ by setting the value of $P$ to $v$ or adding an interpretation for $P$ if $P$ was not in the domain of $S$. We denote this operation as $S \cup \{P=v\}$.
$S \models \forall P \phi$ if and only if for both structures $S'[P \mapsto \text{true}] \models \phi$ and $S'[P \mapsto \text{false}] \models \phi$, where $S'[P \mapsto v]$ is defined as above.

Consider the QBF $\phi = \exists Q (P \lor Q)$. Let $S$ be a structure such that $S(P) = \text{true}$. To evaluate $S \models \phi$, we need to check if there exists a structure $S'$ such that $S' \models P \lor Q$, where $S'$ is obtained from $S$ by either setting $Q$ to true or false. Let $S_1 = S \cup \{Q = \text{true}\}$ and $S_2 = S \cup \{Q = \text{false}\}$. Since $S(P) = \text{true}$, we have $S_1 \models P \lor Q$ and $S_2 \models P \lor Q$. Thus, $S \models \exists Q (P \lor Q)$.

The universal quantifier can be expressed using the existential quantifier and negation: $\forall P \phi \equiv \neg \exists P \neg \phi$.

Free and Bound Variables

In a QBF, a variable is bound if it is under the scope of a quantifier. Otherwise, it is free.

In the formula $\exists P (P \land \forall Q (Q \lor R))$, $P$ and $Q$ are bound, while $R$ is free.

It is generally preferred to avoid using the same variable both free and bound in a formula to prevent confusion. For instance, in the formula $P \land \forall Q \exists P (Q \lor P)$, the variable $P$ is used both free and bound. It is better to rename the bound variable to avoid clashes. For example, the formula can be rewritten as $P \land \forall Q \exists P' (Q \lor P')$.

When we write a formula as $\phi(P_1, \dots, P_n)$, we mean that the free variables of $\phi$ are among $P_1, \dots, P_n$. It is important to specify the free variables of a formula because the truth value of the formula depends on the interpretation of these variables.

Example 1. Consider the formula $\phi(P) = \exists Q (P \lor Q)$ from Example [ex:qbf_semantics]. The only free variable is $P$, so we write it as $\phi(P)$.

Substitution

Let $\phi$ be a QBF with a free variable $P$. We denote by $\phi[P/\alpha]$ the QBF obtained by replacing every free occurrence of $P$ in $\phi$ with the formula $\alpha$.

Let $\phi(P) = \neg P \lor \exists Q \forall P (P \lor \neg Q)$. Then:

$\phi[P/\text{true}] = \neg \text{true} \lor \exists Q \forall P (P \lor \neg Q)$
$\phi[P/(\neg R \lor T)] = \neg (\neg R \lor T) \lor \exists Q \forall P (P \lor \neg Q)$

The substitution only affects the free occurrences of the variable. The bound occurrences are not changed. This is analogous to how substitution works in programming languages when dealing with local and global variables.

Renaming Bound Variables

Let $\phi$ be a QBF and $\exists P \psi$ be a subformula of $\phi$. Let $Q$ be a variable that does not occur free in $\psi$ and does not occur in $\phi$ as a bound variable. Then $\exists P \psi$ is logically equivalent to $\exists Q \psi[P/Q]$.

Proof. Proof. The proof is by induction on the structure of the formula $\psi$. The base case is when $\psi$ is a single variable. In this case, the lemma holds trivially. The inductive step is to assume that the lemma holds for $\psi_1$ and $\psi_2$ and show that it holds for $\neg \psi_1$, $\psi_1 \land \psi_2$, $\psi_1 \lor \psi_2$, $\exists R \psi_1$, and $\forall R \psi_1$. We will omit the details of the proof here, but it follows directly from the semantics of QBF. ◻

The QBF $\exists P (\neg P \land R)$ is equivalent to $\exists Q (\neg Q \land R)$.

It is important that the new variable $Q$ does not already occur as a free variable in $\psi$, and does not occur in $\phi$ as a bound variable. Otherwise, the renaming might change the meaning of the formula. For example, $\exists P (P \land R)$ is not equivalent to $\exists R (R \land R)$.

The same lemma holds for the universal quantifier:

Let $\phi$ be a QBF and $\forall P \psi$ be a subformula of $\phi$. Let $Q$ be a variable that does not occur free in $\psi$ and does not occur in $\phi$ as a bound variable. Then $\forall P \psi$ is logically equivalent to $\forall Q \psi[P/Q]$.

Proof. Proof. Similar to the proof of Lemma [lem:renaming]. ◻

Model Checking

Given a QBF $\phi$ and a structure $S$, the model checking problem asks whether $S \models \phi$.

Algorithm for Model Checking

The model checking problem can be solved recursively using the following algorithm:

A QBF formula $\phi$ and a structure $S$ Returns true if $S \models \phi$, false otherwise $S(P)$ $\neg$ ModelCheck($\phi_1$, $S$) ModelCheck($\phi_1$, $S$) $\lor$ ModelCheck($\phi_2$, $S$) ModelCheck($\phi_1$, $S$) $\land$ ModelCheck($\phi_2$, $S$) $S_1 \gets S \cup \{P = \text{true}\}$ $S_2 \gets S \cup \{P = \text{false}\}$ ModelCheck($\phi_1$, $S_1$) $\lor$ ModelCheck($\phi_1$, $S_2$) $S_1 \gets S \cup \{P = \text{true}\}$ $S_2 \gets S \cup \{P = \text{false}\}$ ModelCheck($\phi_1$, $S_1$) $\land$ ModelCheck($\phi_1$, $S_2$)

Complexity Analysis

Time Complexity: The model checking algorithm for QBF has a time complexity that is exponential in the size of the formula. This is because, in the worst case, we may need to explore all possible assignments to the quantified variables. In particular, if the formula has $n$ quantifiers, we might have to make $2^n$ recursive calls in the worst case.
Space Complexity: The space complexity is polynomial in the size of the formula. This is because the depth of the recursion is at most the number of variables (or quantifiers) in the formula, and each recursive call requires space proportional to the size of the formula and the structure. The size of the structure is at most linear in the number of variables in the formula, as we add at most one new assignment for each variable. Thus the space complexity is $O(n^2)$, where $n$ is the size of the formula. We say that the model checking problem for QBF is in PSPACE. In fact, it is PSPACE-complete.

The model checking problem for propositional logic is in linear time. The addition of quantifiers increases the complexity to PSPACE. This is a significant increase in complexity, and it is a consequence of the increased succinctness of QBF compared to propositional logic.

Satisfiability

Given a QBF $\phi$, the satisfiability problem asks whether there exists a structure $S$ such that $S \models \phi$.

Reduction to Model Checking

The satisfiability problem for QBF can be reduced to the model checking problem by considering the existential closure of the formula.

Let $\phi$ be a QBF with free variables $P_1, P_2, \dots, P_n$. The existential closure of $\phi$ is the QBF $\exists P_1 \exists P_2 \dots \exists P_n \phi$.

A QBF with no free variables is called a sentence.

A QBF $\phi$ with free variables $P_1, \dots, P_n$ is satisfiable if and only if the model checking problem for the existential closure $\exists P_1 \dots \exists P_n \phi$ with the empty structure returns true.

Proof. Proof. If $\phi$ is satisfiable, there exists a structure $S$ such that $S \models \phi$. This structure $S$ provides an interpretation for the free variables $P_1, \dots, P_n$. By the semantics of the existential quantifier, the existential closure $\exists P_1 \dots \exists P_n \phi$ is true under the empty structure. Conversely, if the existential closure is true under the empty structure, then there exists an interpretation for $P_1, \dots, P_n$ that makes $\phi$ true, which means that $\phi$ is satisfiable. ◻

The empty structure is the structure with an empty domain, i.e., it does not assign any value to any variable. It is denoted by $\emptyset$.

Complexity

The complexity of the satisfiability problem for QBF is the same as the complexity of the model checking problem, which is PSPACE-complete.

The satisfiability problem for propositional logic is NP-complete. The addition of quantifiers increases the complexity to PSPACE-complete.

Expressiveness and Succinctness

QBF has the same expressive power as propositional logic, meaning that any property expressible in QBF can also be expressed in propositional logic. Formally, for every QBF formula $\phi$, there exists a propositional logic formula $\phi'$ such that $\phi$ and $\phi'$ have the same models when restricted to the free variables of $\phi$. However, QBF can be exponentially more succinct, meaning that the equivalent propositional logic formula may be exponentially larger than the QBF formula.

A property in this context is a set of interpretations over a set of variables. For example, the property "P implies Q" is the set of interpretations $\{ \{P=T, Q=T\}, \{P=F, Q=T\}, \{P=F, Q=F\} \}$.

Consider the QBF $\exists P \forall Q \exists R (P \lor \neg Q) \land (Q \lor \neg R) \land (\neg P \lor R)$. Translating this to propositional logic may result in an exponential blow-up in the size of the formula. We can eliminate the quantifiers one by one. First, we eliminate $\exists R$: \[\exists P \forall Q (\text{true} \land (Q \lor \neg \text{false}) \land (\neg P \lor \text{false})) \lor (\text{false} \land (Q \lor \neg \text{true}) \land (\neg P \lor \text{true}))\] Simplifying, we get: \[\exists P \forall Q (Q \land \neg P) \lor (\text{false})\] \[\exists P \forall Q (Q \land \neg P)\] Now we eliminate $\forall Q$: \[\exists P (\text{true} \land \neg P) \land (\text{false} \land \neg P)\] \[\exists P (\neg P \land \text{false})\] Finally, we eliminate $\exists P$: \[(\neg \text{true} \land \text{false}) \lor (\neg \text{false} \land \text{false})\] \[\text{false} \lor \text{false}\] \[\text{false}\] In this particular case the formula simplifies to false. However, if we had free variables, we would have to keep track of them during the translation.

We can also see the exponential blow-up more clearly with the following example:

Example 2. Consider the QBF $\phi = \exists P_1 \forall P_2 \exists P_3 \forall P_4 ... \exists P_{n-1} \forall P_n (P_1 \lor \neg P_2) \land (\neg P_2 \lor P_3) \land ...$ If we translate this to propositional logic by eliminating the quantifiers one by one, we will have to double the size of the formula for each quantifier. This will result in a formula of size $2^n$.

The increased succinctness of QBF comes at the cost of increased complexity for model checking and satisfiability. This is a common trade-off in logic and computer science.

Conclusion

In this lecture, we introduced Quantified Boolean Formulas (QBF) as an extension of propositional logic. We explored the syntax and semantics of QBF, highlighting the roles of free and bound variables, and the importance of renaming bound variables to avoid clashes. We discussed the model checking and satisfiability problems for QBF and analyzed their complexities. We found that while QBF has the same expressive power as propositional logic, it can be exponentially more succinct. This succinctness leads to higher algorithmic complexity for model checking and satisfiability, specifically PSPACE-completeness, compared to the linear time and NP-completeness of propositional logic, respectively.

Follow-up Questions:

Can you provide an example of a QBF formula that, when translated to propositional logic, results in an exponential increase in size? (See Example in the previous section)
How might we modify the model checking algorithm to improve its efficiency for certain classes of QBF formulas? (Hint: Consider restrictions on the quantifier structure or the propositional part of the formula.)
What are the implications of QBF’s PSPACE-completeness for practical applications? (Hint: Think about the types of problems that can be modeled using QBF and the feasibility of solving them.)
Explore the relationship between QBF and other logical formalisms, such as first-order logic. What are the trade-offs in terms of expressiveness and complexity? (Hint: Consider the ability to quantify over predicates and functions in first-order logic.)

--- title: "Quantified Boolean Formulas (QBF)" author: "Your Name" date: "2025-02-05" format: html: toc: true # Table of Contents toc-depth: 2 code-tools: true theme: cosmo # Or "journal" for Distill-like minimalism --- # Introduction This lecture introduces **Quantified Boolean Formulas (QBF)**, a generalization of propositional logic that incorporates quantifiers, similar to how first-order logic is a generalization of propositional logic. We will explore the syntax and semantics of QBF, and discuss the complexity of model checking and satisfiability problems. The main objectives are to understand how quantifiers affect the interpretation of formulas, to learn the difference between free and bound variables, and to analyze the algorithmic implications of this extended formalism. We will see that adding quantifiers does not increase the expressiveness of the logic, but it does allow for more succinct formulas. This succinctness comes at a cost, as the complexity of model checking and satisfiability will increase from linear time and $NP$-complete to $PSPACE$-complete, respectively. # Vocabulary, Syntax, and Semantics of QBF ## Vocabulary The vocabulary of QBF extends that of propositional logic by including: - Boolean connectives: $\land, \lor, \neg, \rightarrow, \leftrightarrow$ - Boolean variables: $P, Q, R, \dots$ (We will use capital letters to denote variables) - Quantifiers: $\exists$ (existential) and $\forall$ (universal) ## Syntax The syntax of QBF is defined recursively as follows: - A Boolean variable $P$ is a QBF. - If $\phi_1$ and $\phi_2$ are QBFs, then $\neg \phi_1$, $\phi_1 \land \phi_2$, $\phi_1 \lor \phi_2$, $\phi_1 \rightarrow \phi_2$, and $\phi_1 \leftrightarrow \phi_2$ are QBFs. - If $\phi$ is a QBF and $P$ is a Boolean variable, then $\exists P \phi$ and $\forall P \phi$ are QBFs. ::: tcolorbox []{#ex:qbf_example label="ex:qbf_example"} An example of a QBF is: $$\exists P \forall Q (P \lor \neg Q) \land (\neg R \lor \neg P)$$ Here, $P$ and $Q$ are bound variables, while $R$ is a free variable. ::: ## Semantics The semantics of QBF are defined with respect to a structure $S$, which is a function mapping Boolean variables to truth values (true or false). ::: tcolorbox []{#def:interpretation label="def:interpretation"} An interpretation (or structure) $S$ for a QBF $\phi$ is a function that maps the free variables of $\phi$ to either true or false. ::: ::: tcolorbox It is important to note that we only need to define the interpretation for the free variables. The bound variables will be assigned values by the quantifiers. ::: The semantics are defined recursively: - $S \models P$ if and only if $S(P) = \text{true}$. - $S \models \neg \phi$ if and only if $S \not\models \phi$. - $S \models \phi_1 \lor \phi_2$ if and only if $S \models \phi_1$ or $S \models \phi_2$. - $S \models \phi_1 \land \phi_2$ if and only if $S \models \phi_1$ and $S \models \phi_2$. - $S \models \exists P \phi$ if and only if there exists a structure $S'$ such that $S'[P \mapsto \text{true}] \models \phi$ or $S'[P \mapsto \text{false}] \models \phi$, where $S'[P \mapsto v]$ is the structure obtained from $S$ by setting the value of $P$ to $v$ or adding an interpretation for $P$ if $P$ was not in the domain of $S$. We denote this operation as $S \cup \{P=v\}$. - $S \models \forall P \phi$ if and only if for both structures $S'[P \mapsto \text{true}] \models \phi$ and $S'[P \mapsto \text{false}] \models \phi$, where $S'[P \mapsto v]$ is defined as above. ::: tcolorbox []{#ex:qbf_semantics label="ex:qbf_semantics"} Consider the QBF $\phi = \exists Q (P \lor Q)$. Let $S$ be a structure such that $S(P) = \text{true}$. To evaluate $S \models \phi$, we need to check if there exists a structure $S'$ such that $S' \models P \lor Q$, where $S'$ is obtained from $S$ by either setting $Q$ to true or false. Let $S_1 = S \cup \{Q = \text{true}\}$ and $S_2 = S \cup \{Q = \text{false}\}$. Since $S(P) = \text{true}$, we have $S_1 \models P \lor Q$ and $S_2 \models P \lor Q$. Thus, $S \models \exists Q (P \lor Q)$. ::: ::: tcolorbox The universal quantifier can be expressed using the existential quantifier and negation: $\forall P \phi \equiv \neg \exists P \neg \phi$. ::: # Free and Bound Variables ::: tcolorbox []{#def:free_bound label="def:free_bound"} In a QBF, a variable is **bound** if it is under the scope of a quantifier. Otherwise, it is **free**. ::: ::: tcolorbox []{#ex:free_bound label="ex:free_bound"} In the formula $\exists P (P \land \forall Q (Q \lor R))$, $P$ and $Q$ are bound, while $R$ is free. ::: ::: tcolorbox []{#note:avoid_clashes label="note:avoid_clashes"} It is generally preferred to avoid using the same variable both free and bound in a formula to prevent confusion. For instance, in the formula $P \land \forall Q \exists P (Q \lor P)$, the variable $P$ is used both free and bound. It is better to rename the bound variable to avoid clashes. For example, the formula can be rewritten as $P \land \forall Q \exists P' (Q \lor P')$. ::: When we write a formula as $\phi(P_1, \dots, P_n)$, we mean that the free variables of $\phi$ are among $P_1, \dots, P_n$. It is important to specify the free variables of a formula because the truth value of the formula depends on the interpretation of these variables. ::: example **Example 1**. *Consider the formula $\phi(P) = \exists Q (P \lor Q)$ from Example [\[ex:qbf_semantics\]](#ex:qbf_semantics){reference-type="ref" reference="ex:qbf_semantics"}. The only free variable is $P$, so we write it as $\phi(P)$.* ::: # Substitution ::: tcolorbox []{#def:substitution label="def:substitution"} Let $\phi$ be a QBF with a free variable $P$. We denote by $\phi[P/\alpha]$ the QBF obtained by replacing every **free** occurrence of $P$ in $\phi$ with the formula $\alpha$. ::: ::: tcolorbox []{#ex:substitution label="ex:substitution"} Let $\phi(P) = \neg P \lor \exists Q \forall P (P \lor \neg Q)$. Then: - $\phi[P/\text{true}] = \neg \text{true} \lor \exists Q \forall P (P \lor \neg Q)$ - $\phi[P/(\neg R \lor T)] = \neg (\neg R \lor T) \lor \exists Q \forall P (P \lor \neg Q)$ ::: ::: tcolorbox []{#note:substitution_free label="note:substitution_free"} The substitution only affects the free occurrences of the variable. The bound occurrences are not changed. This is analogous to how substitution works in programming languages when dealing with local and global variables. ::: # Renaming Bound Variables ::: tcolorbox []{#lem:renaming label="lem:renaming"} Let $\phi$ be a QBF and $\exists P \psi$ be a subformula of $\phi$. Let $Q$ be a variable that does not occur free in $\psi$ and does not occur in $\phi$ as a bound variable. Then $\exists P \psi$ is logically equivalent to $\exists Q \psi[P/Q]$. ::: ::: proof *Proof.* The proof is by induction on the structure of the formula $\psi$. The base case is when $\psi$ is a single variable. In this case, the lemma holds trivially. The inductive step is to assume that the lemma holds for $\psi_1$ and $\psi_2$ and show that it holds for $\neg \psi_1$, $\psi_1 \land \psi_2$, $\psi_1 \lor \psi_2$, $\exists R \psi_1$, and $\forall R \psi_1$. We will omit the details of the proof here, but it follows directly from the semantics of QBF. ◻ ::: ::: tcolorbox []{#ex:renaming label="ex:renaming"} The QBF $\exists P (\neg P \land R)$ is equivalent to $\exists Q (\neg Q \land R)$. ::: ::: tcolorbox []{#note:renaming_restriction label="note:renaming_restriction"} It is important that the new variable $Q$ does not already occur as a free variable in $\psi$, and does not occur in $\phi$ as a bound variable. Otherwise, the renaming might change the meaning of the formula. For example, $\exists P (P \land R)$ is not equivalent to $\exists R (R \land R)$. ::: The same lemma holds for the universal quantifier: ::: tcolorbox []{#lem:renaming_universal label="lem:renaming_universal"} Let $\phi$ be a QBF and $\forall P \psi$ be a subformula of $\phi$. Let $Q$ be a variable that does not occur free in $\psi$ and does not occur in $\phi$ as a bound variable. Then $\forall P \psi$ is logically equivalent to $\forall Q \psi[P/Q]$. ::: ::: proof *Proof.* Similar to the proof of Lemma [\[lem:renaming\]](#lem:renaming){reference-type="ref" reference="lem:renaming"}. ◻ ::: # Model Checking ::: tcolorbox []{#def:model_checking label="def:model_checking"} Given a QBF $\phi$ and a structure $S$, the model checking problem asks whether $S \models \phi$. ::: ## Algorithm for Model Checking The model checking problem can be solved recursively using the following algorithm: :::: algorithm ::: algorithmic A QBF formula $\phi$ and a structure $S$ Returns true if $S \models \phi$, false otherwise $S(P)$ $\neg$ ModelCheck($\phi_1$, $S$) ModelCheck($\phi_1$, $S$) $\lor$ ModelCheck($\phi_2$, $S$) ModelCheck($\phi_1$, $S$) $\land$ ModelCheck($\phi_2$, $S$) $S_1 \gets S \cup \{P = \text{true}\}$ $S_2 \gets S \cup \{P = \text{false}\}$ ModelCheck($\phi_1$, $S_1$) $\lor$ ModelCheck($\phi_1$, $S_2$) $S_1 \gets S \cup \{P = \text{true}\}$ $S_2 \gets S \cup \{P = \text{false}\}$ ModelCheck($\phi_1$, $S_1$) $\land$ ModelCheck($\phi_1$, $S_2$) ::: :::: ## Complexity Analysis - **Time Complexity**: The model checking algorithm for QBF has a time complexity that is exponential in the size of the formula. This is because, in the worst case, we may need to explore all possible assignments to the quantified variables. In particular, if the formula has $n$ quantifiers, we might have to make $2^n$ recursive calls in the worst case. - **Space Complexity**: The space complexity is polynomial in the size of the formula. This is because the depth of the recursion is at most the number of variables (or quantifiers) in the formula, and each recursive call requires space proportional to the size of the formula and the structure. The size of the structure is at most linear in the number of variables in the formula, as we add at most one new assignment for each variable. Thus the space complexity is $O(n^2)$, where $n$ is the size of the formula. We say that the model checking problem for QBF is in **PSPACE**. In fact, it is **PSPACE-complete**. ::: tcolorbox []{#note:complexity_increase label="note:complexity_increase"} The model checking problem for propositional logic is in linear time. The addition of quantifiers increases the complexity to PSPACE. This is a significant increase in complexity, and it is a consequence of the increased succinctness of QBF compared to propositional logic. ::: # Satisfiability ::: tcolorbox []{#def:satisfiability label="def:satisfiability"} Given a QBF $\phi$, the satisfiability problem asks whether there exists a structure $S$ such that $S \models \phi$. ::: ## Reduction to Model Checking The satisfiability problem for QBF can be reduced to the model checking problem by considering the existential closure of the formula. ::: tcolorbox []{#def:existential_closure label="def:existential_closure"} Let $\phi$ be a QBF with free variables $P_1, P_2, \dots, P_n$. The existential closure of $\phi$ is the QBF $\exists P_1 \exists P_2 \dots \exists P_n \phi$. ::: ::: tcolorbox []{#def:sentence label="def:sentence"} A QBF with no free variables is called a **sentence**. ::: ::: tcolorbox []{#thm:satisfiability_reduction label="thm:satisfiability_reduction"} A QBF $\phi$ with free variables $P_1, \dots, P_n$ is satisfiable if and only if the model checking problem for the existential closure $\exists P_1 \dots \exists P_n \phi$ with the empty structure returns true. ::: ::: proof *Proof.* If $\phi$ is satisfiable, there exists a structure $S$ such that $S \models \phi$. This structure $S$ provides an interpretation for the free variables $P_1, \dots, P_n$. By the semantics of the existential quantifier, the existential closure $\exists P_1 \dots \exists P_n \phi$ is true under the empty structure. Conversely, if the existential closure is true under the empty structure, then there exists an interpretation for $P_1, \dots, P_n$ that makes $\phi$ true, which means that $\phi$ is satisfiable. ◻ ::: ::: tcolorbox []{#note:empty_structure label="note:empty_structure"} The empty structure is the structure with an empty domain, i.e., it does not assign any value to any variable. It is denoted by $\emptyset$. ::: ## Complexity The complexity of the satisfiability problem for QBF is the same as the complexity of the model checking problem, which is **PSPACE-complete**. ::: tcolorbox []{#note:sat_complexity_increase label="note:sat_complexity_increase"} The satisfiability problem for propositional logic is NP-complete. The addition of quantifiers increases the complexity to PSPACE-complete. ::: # Expressiveness and Succinctness QBF has the same expressive power as propositional logic, meaning that any property expressible in QBF can also be expressed in propositional logic. Formally, for every QBF formula $\phi$, there exists a propositional logic formula $\phi'$ such that $\phi$ and $\phi'$ have the same models when restricted to the free variables of $\phi$. However, QBF can be exponentially more succinct, meaning that the equivalent propositional logic formula may be exponentially larger than the QBF formula. ::: tcolorbox []{#note:property label="note:property"} A property in this context is a set of interpretations over a set of variables. For example, the property \"P implies Q\" is the set of interpretations $\{ \{P=T, Q=T\}, \{P=F, Q=T\}, \{P=F, Q=F\} \}$. ::: ::: tcolorbox []{#ex:succinctness label="ex:succinctness"} Consider the QBF $\exists P \forall Q \exists R (P \lor \neg Q) \land (Q \lor \neg R) \land (\neg P \lor R)$. Translating this to propositional logic may result in an exponential blow-up in the size of the formula. We can eliminate the quantifiers one by one. First, we eliminate $\exists R$: $$\exists P \forall Q (\text{true} \land (Q \lor \neg \text{false}) \land (\neg P \lor \text{false})) \lor (\text{false} \land (Q \lor \neg \text{true}) \land (\neg P \lor \text{true}))$$ Simplifying, we get: $$\exists P \forall Q (Q \land \neg P) \lor (\text{false})$$ $$\exists P \forall Q (Q \land \neg P)$$ Now we eliminate $\forall Q$: $$\exists P (\text{true} \land \neg P) \land (\text{false} \land \neg P)$$ $$\exists P (\neg P \land \text{false})$$ Finally, we eliminate $\exists P$: $$(\neg \text{true} \land \text{false}) \lor (\neg \text{false} \land \text{false})$$ $$\text{false} \lor \text{false}$$ $$\text{false}$$ In this particular case the formula simplifies to false. However, if we had free variables, we would have to keep track of them during the translation. ::: We can also see the exponential blow-up more clearly with the following example: ::: example **Example 2**. *Consider the QBF $\phi = \exists P_1 \forall P_2 \exists P_3 \forall P_4 ... \exists P_{n-1} \forall P_n (P_1 \lor \neg P_2) \land (\neg P_2 \lor P_3) \land ...$ If we translate this to propositional logic by eliminating the quantifiers one by one, we will have to double the size of the formula for each quantifier. This will result in a formula of size $2^n$.* ::: ::: tcolorbox []{#note:succinctness_cost label="note:succinctness_cost"} The increased succinctness of QBF comes at the cost of increased complexity for model checking and satisfiability. This is a common trade-off in logic and computer science. ::: # Conclusion In this lecture, we introduced Quantified Boolean Formulas (QBF) as an extension of propositional logic. We explored the syntax and semantics of QBF, highlighting the roles of free and bound variables, and the importance of renaming bound variables to avoid clashes. We discussed the model checking and satisfiability problems for QBF and analyzed their complexities. We found that while QBF has the same expressive power as propositional logic, it can be exponentially more succinct. This succinctness leads to higher algorithmic complexity for model checking and satisfiability, specifically PSPACE-completeness, compared to the linear time and NP-completeness of propositional logic, respectively. **Follow-up Questions:** 1. Can you provide an example of a QBF formula that, when translated to propositional logic, results in an exponential increase in size? (See Example in the previous section) 2. How might we modify the model checking algorithm to improve its efficiency for certain classes of QBF formulas? (Hint: Consider restrictions on the quantifier structure or the propositional part of the formula.) 3. What are the implications of QBF's PSPACE-completeness for practical applications? (Hint: Think about the types of problems that can be modeled using QBF and the feasibility of solving them.) 4. Explore the relationship between QBF and other logical formalisms, such as first-order logic. What are the trade-offs in terms of expressiveness and complexity? (Hint: Consider the ability to quantify over predicates and functions in first-order logic.)