# Understanding terms related to 2SAT algorithm [closed]

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 < 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?

• What is the source? It should define the terms it uses. To me, a universal vertex is a vertex adjacent to every other vertex. – Juho Mar 28 '15 at 8:58
• The terms universal vertex and existential vertex are specific to the theorem, and should be defined as part of the proof. – Yuval Filmus Mar 28 '15 at 15:04
• See cs.stackexchange.com/help/account if you need help with your account. – Gilles 'SO- stop being evil' Mar 31 '15 at 19:10

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$.