Understanding terms related to 2SAT algorithm Recently I am learning about solution of the 2-satiability problem using strongly connected components. There is a theorem related to this problem given below:
Let $F = Q_lx_1 Q_2x_2\ldots Q_nx_n C$ be a quantified Boolean formula with no free variables, where each $Q_i$ is either universal or existential, and $C$ is in conjunctive normal form. That is, $C$ is a conjunction of clauses, each clause is a disjunction of literals, and each literal is either a variable, $x_i$, or the negation of a variable, $x_i$ ($1 \leq i \leq n$).

Theorem 2: The formula $F$ is true if and only if none of the following three conditions holds:
3(i) An existential vertex $u$ is in the same strong component as its complement $u’$.
3(ii) A universal vertex $u_i$ is in the same strong component as an existential vertex $u_j$ such that $j &lt; i$ (i.e., $x_i$ is not quantified within the scope of $Q_i$).
3(iii) There is a path from a universal vertex $u$ to another universal vertex $v$. (This condition includes the case that $v = u$.)

In the proof they use this definition:
We call a vertex universal if the corresponding variable is universally quantified and existential otherwise.
But I am not familiar with the terms universal vertex and existential vertex. Can any one please explain these terms to me?
The terms universal vertex and existential vertex are not universal, but rather specific to this specific theorem. The context is a graph on the set of literals (variables and their complements). Presumably for every clause $\ell_1 \lor \ell_2$ in $C$, there is an arrow from $\bar{\ell}_1$ to $\ell_2$.

A vertex is called universal if its corresponding variable is universally quantified, that is, quantified as $\forall x_i$. In other words, if $Q_i x_i = \forall x_i$ then the vertices $x_i$ and $\bar{x}_i$ are universal.

Similarly, a vertex is called existential if its corresponding variable is existentially quantified, that is, quantified as $\exists x_i$.